The other day Sara Uckelman of Durham asked on Twitter about people’s favourite textbook for 1st year intro logic using natural deduction/Fitch-style proofs. And she piqued my interest by mentioning that Lemmon’s book was currently top of her list.

Now there’s a blast from the past! Forty-five years ago — oh heavens above — when very first starting out teaching logic, I used Lemmon’s *Beginning Logic* as our textbook. For back then, at least by today’s standards, there were relatively few choices for books with a reasonably modern flavour. Lemmon’s book indeed has considerable virtues, but ease of manipulation of his deduction system by the more symbol-phobic student turned out not to be one of them. One trouble is that his formal system isn’t, of course, really a natural deduction system but is a sequent calculus (with the sequents written in a slightly non-standard way, with the wffs on the left [of the unwritten sequent arrow] being labelled by numbers rather than written out in full). So as you go along though a proof, you have to keep an explicit tally of active assumptions at each step (unlike with a Fitch-style proof, where the layout does the work for you). And strategies for finding Lemmon-style proofs aren’t that transparent to many beginners. Indeed, in tricky cases, I’d find myself thinking though a Fitch-style proof, which indeed reflects *natural *deduction* *steps, and then making the result Lemmon-flavoured. So why not do things Fitch-style from the off?

Which is indeed what I eventually started doing when after a gap of a few years (having for a while swapped courses with a colleague), I started teaching intro logic again, making my own course handouts using a Fitch-style system.

I wasn’t being at all idiosyncratic, by the way, in finding Lemmon’s book unsatisfactory (in the sense of finding that, despite its other virtues, it was too unfriendly for rather too many students). Peter Millican wrote round to UK philosophy departments — maybe about 1980, before email was common — to discover what books people used in their first-year logic courses; and the majority reply was, if I recall right, “Lemmon, but …”. Lecturers, that is to say, used Lemmon, but with significant reservations about how well the book actually worked with their students. It’s not for nothing that quite a few of us, when computers came along to make the job so much easier, produced our own handouts, a number of which indeed grew up to become books.

I found that the students seemed to cope significantly better with the business of writing correct formal proofs in the Fitch-style setting, with less messy housekeeping to keep track of, and the very nice visual display of what depends on what. It’s not called a natural deduction system for nothing! Yet, for all that, at some point in the 80s, I did switch from starting with a Fitch-style system to starting with a tableaux system (as in Hodges’s book, or Jeffrey’s, or later my own). And that’s what I continued to do for the thirteen years when I was the main lecturer for the formal part of the Cambridge first year logic paper. But why so?

My first formal logic course as an undergrad used Jeffrey (c. 1972). I was a confirmed tree-hugger already by then, due to the likes of Peirce, Lisp, Harary, and Dodgson, and I’m still quasi-arboreal after all these years.

It would also be worthwhile to reconsider “classic” logic operators because they may not be really optimal, the “ternary majority” studied long ago by Emil Post has been all but forgotten:

http://www.sciencedirect.com/science/article/pii/S0012365X06004742

However it beats the classic bunch of AND, OR, NOT, NAND etc…

http://infoscience.epfl.ch/record/204262?ln=en

But being ternary it doesn’t jibe well with the “tyranny” of binary operators. :-)

You may find some diversion in the family of

minimal negation operatorsthat arose in my study of Peirce’s amphecks and logical graphs as I evolved from trees to cacti.If logic has anything to do with deductive reasoning, then I’d have thought natural deduction is the most natural way to present logic. (Some ND formats are more natural than others. Fitch is easy for students; I find Gentzenian ND more perspicuous, and Gentzenian ND in sequent-style more perspicuous still.)

To be sure, tableaux also work well with students. But: they don’t really represent formal deductive reasoning, and their intuitive reading is semantic, which may be confusing for students (it is a syntactic method after all).

Yes! I have always found tableaux a bit too ‘semantic’ (and too different from normal reasoning). So they don’t seem ideal for making clear the significance of, and ideas behind, soundness and completeness theorems that relate syntax and semantics, or for understanding how to formalise arguments presented in natural language.

My first logic text as an undergraduate was Suppes, which I still love for reasons other than nostalgia. I’ve used occasionally in my intermediate logic course. (I like all the applied theories). It does show its (my) age.

But over forty years of teaching the baby logic course, except for a few “oh, lets try some ND for a change, because they should know *deduction*” semesters, I’ve done trees. Jeffrey, Hodges, Smith. Why?

Because for my students I set the goal of learning the (informal) semantics of FOL=, i.e., learning to symbolize. For them, the derivation system had to be easy and trees had the virtue be easily routinized and easily semantically motivated via, for example, knight-knave problems.