IPT is particularly aimed at those “who have only a minimal background in mathematics and logic”. Well, philosophy students who haven’t done much logic may well not have encountered an old-school axiomatic presentation of logic before. So — perhaps reasonably enough — Chapter 2 is on Axiomatic Calculi. The chapter divides into two uneven parts, which I’ll take in turn.
In the early sections, we meet axiomatic versions of minimal, intuitionist and classical logic for propositional logic (presented using axiom schemas in the usual way). Next, after a pause to explain the idea of proofs by induction, there’s a proof of the deduction theorem, and an explanation of how to prove independence of axioms (more particularly, the independence of ex falso from minimal logic, and the independence of the double negation rule from intuitionist logic) using deviant “truth”-tables. Then we add axioms for predicate logic, and prove the deduction theorem again. So this part of the chapter is routine stuff. And really the only question is: how well does the exposition unfold?
By my lights, not very well. OK, perhaps the general state of the world is rather getting to me, and my mood is less than sunny. But I did find this disappointing stuff.
For a start, the treatment of schemas is a mess. It really won’t do to wobble between saying (p. 19) that axioms are formulas which are instances of schemas, and saying that such a formula is an instance of an axiom (p. 21). Or how about this: “an instance of an instance of an axiom is an axiom” (p. 21). This uses ‘axiom’ in two different senses (i.e. first meaning axiom schema) and then meaning axiom), and it uses ‘instance’ in two different senses (first meaning instance (of schema) and then meaning variant schema got by systematically replacing individual schematic letters by schemas for perhaps non-atomic wffs).
Or how about this? — We are told that a formula is a theorem just if it is the end-formula of a derivation (from no assumptions). We are immediately told, though, that “in general we will prove schematic theorems that go proxy for an infinite number of proofs of their instances.” (p. 20) You can guess what this is supposed to mean: but it isn’t what the sentence actually says. There’s more of the same sort of clumsiness.
When it comes to laying out proofs, things again get messy. The following, for example, is described as a derivation (p. 32):
This is followed by the comment “Note that lines 1 and 2 do not have a ⊢ in front of them. They are assumptions, not theorems. We indicate on the left of the turnstile which assumptions a line makes use of. For instance, line 4 is proved from lines 1 and 3, but line 3 is a theorem — it does not use any assumptions.” But first, with this sort of Lemmon-esque layout, shouldn’t the initial lines have turnstiles after all? Shouldn’t the first line commence, after the line number, with “(1) ⊢” — since the assumption that the line makes use of is itself? And more seriously, in so far we can talk of line (9) as being derived from what’s gone before, it is the whole line read in effect as a sequent which is derived from line (8) read as a sequent — it’s not an individual formula derived from earlier ones by a rule of inference. So in fact this just isn’t a derivation any more in the original sense given in IPT in characterizing axiomatic derivations.
I could continue carping like this but it would get rather boring. However, a careful reader will find more to quibble about in these sections of the chapter, and — more seriously — a student coming to them fresh could far too easily be misled/confused.
The final long §2.15, I’m happy to say, is a rather different kettle of fish, standing somewhat apart from the rest of the chapter in both topic and level/quality of presentation. This section can be treated pretty much as a stand-alone introduction to a key fact about classical and intuitionist first-order Peano Arithmetic (with an axiomatic logic), namely that we can interpret the first in the second, thereby establishing that classical PA is consistent if the intuitionist version is. This is, I think, neatly done enough (though I suspect the discussion might need a slightly more sophisticated reader than what’s gone before).
Just one very minor comment. A student might wonder why what is here called the Gödel-Gentzen translation (atoms are left untouched) is different from what many other references call the Gödel-Gentzen translation (where atoms are double negated). A footnote of explanation might have been useful. But as I say, this twelve page section seems much better.
To be continued
I guess you have to write the “Intro to proof theory” yourself. I’d buy it. Thanks for the in-depth review.
I suspect that §2.15 is the part that actually interests the authors, that the earlier part is there because they think they have to say something about such things, and that it suffers from the ‘authors know what they meant’ problem: because they know what they meant, they see the text as saying the right sort of thing — without noticing that it might at best be unclear to readers who don’t already know what it’s supposed to be saying. (And because it’s about boring, standard stuff, they don’t read it carefully?)