After a longer than intended gap, I return to consider Parts III and IV of Tony Roy’s freely available Symbolic Logic: An Accessible Introduction to Serious Mathematical Logic. The previous two , rather lukewarm, instalments discussing Parts I and II are here and here (but do please note Roy’s long comment in response).
Part of my beef against this very long text is indeed its length. In teaching maths, often the key task is to engender the kind of understanding that enables the student to see the wood for the trees, to see what are the Big Ideas and what is merely hack-work joining up the dots. The longer you bang on filling in every last detail of a proof, the greater the danger that you will obscure the overall contours of what’s going on (even if you scatter around an amount of signposting). We ask our students in exams to do “bookwork” questions outlining a proof of some major result, and here the name of the game is indeed to highlight the Big Ideas, the key moves, and to confidently know what can be gestured at, or when we can say “rather similarly, we can show …” etc. Where I take issue with Roy’s pedagogic style, then, is in thinking that writing at his length won’t really help foster these skills.
I mention this again because Part III on Classical Metalogic consists mostly of two very dense chapters, one of forty pages, one of fifty pages, going into rather over-the-top detail (by my lights) on relatively few results. So again I wouldn’t recommend these as primary reading for students encountering some metalogic for the first time.
However, on the positive side, the main content of Chapter 9 is unusual in one interesting respect. Roy has earlier introduced both an axiomatic and a natural deduction system for first-order logic. We can of course prove they are equivalent by going via the respective soundness/completeness proofs for the two systems. (That doesn’t really require two lots of proofs as we can point out in particular that what it takes for a Henkin completeness proof to go through is available in both cases.) But we can also give a syntactic equivalence proof for the two systems by showing how to systematically manipulate in both directions a proof of the one sort into a proof of the other. Now, this tends to be the sort of thing one armwaves about in class, perhaps sketching in a few obvious moves. But I can’t offhand recall any textbook which spells out in any detail, for particular given axiomatic and ND systems, clear routines for moving between proofs in the two systems (any offers here?). Roy however does this at (slightly numbing) length. Good: we can now usefully point any students unsatisfied by classroom armwaving who want to know how such proofs go to Roy’s very careful working-out of detailed routines.
Chapter 10 then tackles soundness and completeness. The completeness proof for the sentential fragment takes eleven pages: another thirty pages labour over the completeness of a first-order calculus with identity. This is, for example, over twice the number of pages needed by the extraordinarily lucid, gently paced, Chiswell and Hodges. I won’t quote chunks, as you can make your own judgement, since the chapter (as with the rest of the Accessible Introduction) is freely available. But I honestly can’t imagine many students finding the extra length going with a doubling in clarity and understanding. Indeed, if a student were stuck on a Henkin completeness proof in one standard text, I’d first suggest looking at another snappy presentation in a different text (before mentioning Roy’s much longer efforts): for the problem would very likely be in seeing the overall strategy, the Big Ideas — and brisker presentations are likely to make those stand out better.
Part III also contains a fragmentary Chapter 11 which belatedly talks about expressive completeness for the sentential connectives, and then says something briefly about compactness and the L-S theorems. But I won’t say anything about this.
To be concluded.