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
“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. ”
“… according to the definition of a proof …”
Yeah, this is one of the strangest things I’ve seen in some texts and it seems all too common. The author takes the time and effort to define a proof precisely. Then they present something, and call it a “proof”. What was the point of the definition of a proof if it *never* gets used? Also, what if some reader just says something:
“huh? No, you just told me what a proof is. That isn’t a proof. It doesn’t satisfy your requirements. You can’t even have the consistency to use the right name when you present something using your own definition. That eviscerates your credibility. Why should I trust what you say when you can’t even stick to what you said held?”
It’s even worse since computers have been around in my opinion, since they generally require that the exact formal requirements get satisfied by the progammer or something will end up a bug sooner or later or the program won’t run at all even. And sure, shorthands can be fine to use sometimes, but again, *never* present an exact formal proof anywhere? I guess at least some authors have satisfied their formal requirements sometimes, and some others satisfied their formal requirements much and even most of the time.
I think you misunderstand my (mild) complaint. I wasn’t saying that the author of IPT were not presenting “exact formal proofs”. Very far from it: what they present satisfy the relevant formal requirements perfectly. Yes, they present proofs indirectly using schemas. But that is of course the standard way of getting the wanted generality, and is of course just fine. My small point, such as it was, is that just occasionally the authors say things which are a bit careless in moving between schemas and formulas.
It’s a shame they don’t get the details right re formulas and schemas. As you say, “it is easy to tidy this up so it says what is meant.” However, you first have to notice. So I think this could be another instance of the ‘authors know what they meant’ problem I mentioned in my comment on your Ch 2 post.
Re discussing Fitch-style natural deduction, an argument could be that while some readers would find it enlightening, others might be more confused than helped by the book discussing two different types of ND systems. Also, the book is already 400 pages long. Perhaps the authors reasoned reasoned like that.
Yes, I wasn’t suggesting adding a lot about Fitch-style ND: as you say, the book is long enough as it is. But not to make any mention (when it might aid understanding, and indeed enable you to speed up a bit) strikes me as an odd choice.