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, which then extends to more complex quanta.  Moreover, in these cases, 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 — 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 do want to get across) is one thing, and that having the ability to spot a proof strategy within the 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 our main task with first year philosophers is teaching understanding of what’s going in some formal system rather than giving a catalogue of tricks of proof-discovery, then starting with tableaux which they can work without needed 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. But having a tableaux-based course doesn’t mean these things get lost (they get covered in the large part of the course that isn’t specifically about your chosen formal system). Of course we want our students to get clear about the difference between syntactic and semantic notions. But we can reinforce that 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 I do understand the motivation for voting that way (as indeed my successor in teaching the first year Cambridge course did). Yet I think, given my time over again, I’d still on balance go arboreal.