Tableaux or not tableaux, #3

The situation, perhaps we can nearly all agree, is this. In a first formal logic course for philosophers there’s a lot we’ll want/need to pack that’s independent of the nitty-gritty of a deductive apparatus of any particular formal proof system you might want to introduce. (I notice that in my  Introduction to Formal Logic elaborating my lecture course, no less than 27 of the 36 short chapters are on matters other than the actual tableaux system it uses — nearly 20 of those chapters are really on matters round and about the formal languages that would shared by different proof systems). Also, it behoves us to remember that a fair proportion of our class will find even these other parts of the logic course tough, before ever getting down to trying to manipulate our favoured proof system.

So, given the limited proportion of our time we can devote to developing a formal proof system (assuming we want to do that) and given the level of formal work we can sensibly hope to get our typical student to cope with, what to do? — assuming we aren’t just going to sail on without worrying about most of the class falling overboard at this point.

Gentzen-style deduction systems are — of course, as we all know — the Right and Proper Way of doing logic as nature intended! But by my lights, they aren’t so readily manageable by non-mathematical beginners. (Be honest: if you have to discover a rather tricky Gentzen-style proof, how do you do it? — I bet the answer, for a good number of us, is that you roughly sketch out something more Fitch-style, think “Aha, that’s the way a proof can go!”, and then massage the sketch into an official Gentzen-style tree!). So setting aside such systems for introductory purposes, and also setting aside axiomatic systems and sequent calculi (lovely though they are if our focus is on metalogical investigation), then I guess that really leaves us with Fitch-style calculi and tableaux systems. Which are indeed surely the usual options these days.

There are pros and cons on both sides, and it would be absurd to dismiss either option: indeed, it would be great to be able to look at both, but constraints of time will no doubt force a choice. (And constraints of space similarly forced a choice in my IFL where I really wanted another seven or eight short chapters on natural deduction, but CUP saw the matter differently!) As I said in the opening instalment of these posts, for a number of years, I did cast my vote for a Fitch-style natural deduction system. But I ended up teaching formal tableaux in the first year (leaving natural deduction to be covered briskly in a follow-up second-year course). Why so?

I think a major consideration was this. Tableaux for propositional logic give us mechanical procedures for demonstrating valid entailments to be so.  Moreover, when a tree stays open, we can read off a counter model demonstrating the invalidity of the argument being examined. The same goes for quantificational tableaux in simple cases; and it is only later on that you might have to use a bit of ingenuity to get a tree for a valid argument to close.

Stick to the propositional case for the moment: then the worst that go wrong for a careful student is that, by making injudicious choices of which rules to apply when, trees may sprawl more than is necessary. The student can do the logic without having to be smart at spotting proof strategies. Which is just great. For we all know that appreciating what it is to apply rules of a formally defined system (something we probably do want to get across) is one thing, and that having the ability to spot a proof strategy within that system is something else entirely — as is spectacularly illustrated in a Hilbert-style axiomatic system like Mendelson’s where it is very easy indeed to understand what constitutes a proof and can be ludicrously difficult to find a proof at least in the unaugmented system. Now, true enough, proofs in a Fitch-style system are a lot easier to find than in a Hilbert-style system: but even so, unless you mess about introducing redundant rules in inelegant ways, there will always be simple things that require somewhat tricksy proofs — and you will have to spend time drumming into your students’s heads paradigms for various cases they may encounter. And that, by my lights, is not a good use of your very limited time or of their logical efforts. If we suppose, not unreasonably, that with first year philosophers we should be more concerned to engender understanding of the principles of some formal system rather than giving a catalogue of tricks of proof-discovery, then starting with tableaux which they can at least (for quite a while) work without needing much ingenuity has its very considerable attractions. (Anecdotally, it was the most mathematically minded of the interested people on the faculty who were keenest on starting with tableaux for just these sorts of reasons.) Sure, when we get to some tableaux for arguments involving multiply-quantified propositions, the more mathematically ept students can get a chance to show off — but that comes later, as it should.

Of course we want our students to know what informal modus ponens, conditional proof, reductio, etc. are (and we’ll want to say something about how such moves can get chained together, e.g. when mathematicians build up proofs). But having a course which — when it comes to a formal system — uses tableaux doesn’t mean these things get lost (they can and should get covered in the large part of the course that isn’t specifically about your chosen formal system, and then we can return to formal natural deduction at a later stage). Of course we want our students to get clear about the difference between syntactic and semantic notions. But although there is a sense in which tableaux are semantically driven, we can reinforce the syntax/semantics distinction just as well in a tableaux-based course as in a course that focuses on natural deduction (see my book).

Having said all that, Fitch-style natural deduction is indeed lovely and, yes, natural. And if I had been teaching mathematics students who are already developing some informal notion of rigorous deduction then I’d have surely taught some form of ND (maybe indeed Gentzen-style) from the off, developing an interplay between their informal and formal understanding of rigorous proof. But it’s teaching beginning philosophers that we are talking about here, and that I think changes the calculation of pros and cons. I certainly understand the motivation for teaching a Fitch-style system to philosophers (as indeed my successor in teaching the first year Cambridge course has chosen to do). Yet I think, given my time over again, I’d still on balance go arboreal.