An Introduction to Proof Theory, Ch. 7 and Ch. 9
At an abstract level of description, the strategy of Gentzen’s consistency proof for PA can be readily described. We map proofs in his sequent calculus version of PA to ordinals less than 𝜀0. We show that there’s an effective reduction procedure which takes any proof in the system which ends with absurdity/the empty sequent and outputs another proof with the same conclusion but a smaller assigned ordinal. So if there is one proof of absurdity in PA, there is an infinite chain of such proofs indexed by an infinite descending chain of ordinals. That’s impossible, so we are done.
The devil is in all the details. And these will depend, of course, on the exact system of PA which we work with. If we do indeed start from something close to Gentzen’s own system, then things quickly get obscurely intricate in a very untransparent way. The assignment of ordinals initially seems pretty ad hoc and the reduction procedure horribly messy. It is the presence of PA’s induction rule which causes much of the trouble. So as Michael Rathjen suggests in his entry on Proof Theory in the Stanford Encyclopedia, it seems notably more elegant to introduce an infinitary version of PA with the omega-rule replacing the induction rule, and then proceed in two stages. First show that we can unfold any PA deduction into a PA𝜔 deduction, and then do a much neater Gentzen-style consistency proof for PA𝜔 (the general idea is familiar to old hands from the tantalizing Appendix in the first edition of Mendelson’s classic book!).
Mancosu, Galvan and Zach, however, stay old-school, giving us something close to Gentzen’s own proof. Even with various tweaks to smooth over some bumps, this takes them seventy-seven pages. And yes, these pages are spent relentlessly working though all the details, with extended illustrations of various reduction steps: it is not that the discussion is padded out by e.g. a philosophical discussion about the warrant for accepting the required amount of ordinal induction. Is the resulting hard slog worth it?
A mixed verdict (and I’ll be brief too). There’s something very positive to say in a moment. But first the more critical comment.
It sounds so very very ungrateful, I know, but I didn’t find the level of exposition here that brilliant. The signposting along the way could be more brightly lit (long sections aren’t subdivided, and [mixing my metaphors!] crucial paragraphs can appear without fanfare — see e.g. half way down p. 280). And more importantly, page by page, the exposition could often be at least a couple of degrees more perspicuous. It is not that the proof details here are particularly difficult; but still, and really rather too often, I found myself having to re-read or backtrack. I predict, then, that many of IPT’s intended readers (who may, recall, “have only a minimal background in mathematics and logic”) will find this less than maximally clear, and hence markedly tougher going than the authors wanted.
On the bright side, though, the somewhat more sophisticated reader — someone with enough mathematical nous to read these chapters pausing over the key ideas and explanations while skipping/skimming over much of the detail (and having a feel for which is likely to be which!) — should indeed fairly easily end up with a very good understanding of the general structure of Gentzen’s proof and what it is going to take to elaborate it. Such a reader should find that — judiciously approached — IPT provides a much more attractive introduction than e.g. Takeuti’s classic text. So that’s simply terrific! But as I say, I think this probably requires a reader not to do the hard end-to-end slog, but to be mathematically confident enough to first skim through to get the headline ideas, and then do a second pass to get more feel for the shape of some of the details; they can then dig down further again for as much of the remaining nitty-gritty that they then feel that they want/need (probably not a lot!). For this more sophisticated reader, prepared to mine IPT for what they need in an intelligent way, these chapters on Gentzen’s consistency proof will be a great resource.
And on that happier note, let me end!
The post An Introduction to Proof Theory, Ch. 7 and Ch. 9 appeared first on Logic Matters.
