Time flies like an arrow.
Fruit flies like a banana.
If you’ve been following my twitter feed, you’d realise I’m still alive. You wouldn’t think that from the activity – or lack thereof – here. (Though a few papers have appeared – or changed their publication status – on my writing page.)
Here’s where we are: It’s been a busy, eventful semester, and the teaching period is almost done. I’ve had fun teaching proof theory to fourth-year students, tutoring intro philosophy to first years, and supervising graduate students (at last count, I have eight current research students in various stages of the degrees). One of the sadder things to befall us here at Melbourne is the departure of Allen Hazen, who as left our shores for the chillier climes of Edmonton. The Melbourne logic community’s loss is Canada’s gain here.
Tomorrow, I’m off on a short trip to Guangzhou, by way of St. Andrews and Bristol. It’s the long way around, but somebody has got to do it. I’m busy clearing the decks here of as much as I can before the trip. One of the decks to be cleared is this blog, so a post is in order.
Posting about not posting for a long time is so passé, so here’s a link to something you might like if you’re a logic person like me. Lately, I’ve enjoyed playing around with Wandering Mango’s program Deductions (Mac OS X only). It’s a very neat natural deduction educational tool: it helps you produce valid Fitch-style natural deduction proofs, using the format of the major texts used in intro teaching. Well, as far as I can tell, they’re the major texts ued in intro teaching in North America. In Australia, in Europe, in the UK, logic is taught in different ways: Smullyan-style tableaux, Gentzen tree-style natural deduction, Lemmon-style linear natural deduction (though see the update below) with labels, etc. There’s a lot you need to do if you’re going to cover the ground of all the ways of teaching introductory logic by way of ‘proofs’. I’ve been in touch with the developer, and he tells me this is only the beginning for Deductions. It’s built in a modular fashion, and it shouldn’t be too hard to start extending it to cover more systems.
So, if you teach logic, or if you’re learning logic and you’d like to learn it by having a proof assistant on side to keep your proofs on track take a look at Deductions.
Update on December 8, 2009: Jeff Pelletier reminds me in an email that Lemmon’s beginning logic was not the first to introduce what I called ‘Lemmon-style’ linear natural deduction. Patrick Suppes, in his Introduction to Logic. For more on ths history of natural deduction, a great place to start is Jeff’s own “A Brief History of Natural Deduction.” Thanks for that, Jeff!
