Chapter 3 of IPT is on Natural Deduction. The main proof-theoretic work, on normalization, is the topic of the following chapter, and so the topics covered here are relatively elementary ones.
In particular, the first four sections of the chapter simply introduce Gentzen-style proof systems for minimal, intuitionist, and classical logic. So, as with most of the previous chapter, the main question about these sections is: just how good is the exposition?
One initial point. The book, recall, is aimed particularly at philosophy students with only a minimal background in mathematics and logic. But if they are reading this book at all, then — a pound to a penny — they will have done some introductory logic course. And it is quite likely that in this course they will already have met natural deduction done Fitch-style (indenting subproofs in the way expounded in no less than thirty different logic texts aimed at philosophers). It seems strange, to say the least, not to mention Fitch-style natural deduction at all; wouldn’t it have helped many readers to do a compare-and-contrast, explaining why (for proof-theoretic work) Gentzen-style tree layouts are customarily the standard?
An explicit comparison might, indeed, have helped in various places. For example, on p. 73 we are bluntly told that the inference from A to (B ⊃ A) is allowed by the conditional proof rule, i.e. vacuous discharge is allowed. No explanation is given to the neophyte of why this isn’t a cheat. A student familiar with conditional proof in a Fitch-style setting (where there is no requirement that the formula at the head of a subproof is essentially used in the derivation of the end-formula of the subproof) should have a head start in understanding what is going on in the Gentzen setting and why it might be thought unproblematic. Why not make the connection?
Next, it is worth saying that, while this chapter is about natural deduction proofs, there isn’t a single actual example of a proof set out! For the tree arrays which populate the chapter aren’t object language proofs, with formulas as assumptions and a formula as conclusion — they are all entirely schematic, with every featured expression a metalinguistic schema. Ok, this is pretty common practice; and it wouldn’t be worth remarking on if it was very clearly explained that this is what is happening. But it isn’t (I suppose a mis-stated single sentence back on p. 20 in the previous chapter is somehow supposed to do the job). And worse, our authors sometimes seem to themselves forget that everything is schematic. For example, at the foot of p. 79 an attempted proof schema is laid out, ending with the schema 𝐴(𝑐) ⊃ ∀𝑥𝐴(𝑥). This is followed by the comment “The end-formula of this ‘deduction’ is not valid, so it should not have a proof”. Now, it is indeed formulas, not schemas, that have natural deduction proofs according to the definition of a proof on p. 69. OK, so what is “the end-formula” here? There is no unique such formula. Are we supposed to be generalising then about all formula-instances of the proof schema? But the end-formula of an instance of this attempted proof schema could perfectly well be valid. Ok, yes of course, it is easy to tidy this up so it says what is meant, along with a number of related mishaps: but the student reader shouldn’t be left having to do the work.
A third point. Oddly to my mind, the authors have decided to say nothing here about the supposed harmony between the core introduction and elimination rules shared by classical and intuitionist logic (there is just the briefest of mentions in the Preface of this as a topic that the reader might want to follow up). Well, I can certainly understand not wanting to get embroiled in the ramifying debates about the philosophical significance of harmony. But the relevant formal feature of the rules (that demarcates “or” from “tonk”) is so very neat that it is surely worth saying something about it, even when formal issues are at the forefront of attention. More generally — though I do realize this now is a rather unfocused grumble — I’d say that the expository §§3.1–3.4 don’t really bring out the elegance of Gentzen-style natural deduction.
Moving on to the rest of the chapter, §3.5 notes a couple of measures of the complexity of a deduction tree, and then the remaining two sections of the chapter look at a handful of results about deductions proved by induction on complexity. In particular, §3.7 shows that a formula is deducible in the axiomatic system for classical logic given in the previous chapter if and only if it is deducible in the classical natural deduction system described in this chapter. This bit of proof-theory is nicely done.
I’ve more quibbles that I’ll skip over. Overall, though, I would say that this chapter does fall somewhat short of my ideal of an introduction to Gentzen-style natural deduction. Still, students coming to it already knowing about Fitch-style proofs will surely be able to manage the transition and should get the hang of things pretty well. But I suspect that those who have never encountered a natural deduction system before might find it all significantly harder going.
To be continued