The overall 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 turns out to be 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 significantly neater Gentzen-style consistency proof for PA𝜔 (the general idea was worked out by Schütte, and is familiar to old hands from the tantalizing fourteen-page 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, after an initial dozen pages saying a bit more about PA, this takes them sixty-five pages. And yes, these pages are spent relentlessly working though all the details for the specific chosen version of PA, 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; nor are there discussions of variant Gentzen-style proofs like Schütte‘s. Is the resulting hard slog worth it?
A mixed verdict (and I’ll be brief too, despite the length of these chapters — as I don’t think there is much profit in trying to summarise here e.g. the stages of the reduction procedure, or in looking at particular points of exposition). There’s something 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, or having to work out the motivation for a technical detail for myself. 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 — to say the least — markedly tougher going than the authors wanted. The logically naive reader will struggle, surely.
But now forget about IPT’s official mission-statement! On the bright side, the more sophisticated reader — someone with enough mathematical nous to read these chapters pausing over the key ideas and explanations while initially skipping/skimming over much of the detail (and having a feel for which is likely to be which!) — should actually 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 more attractive introduction than e.g. Takeuti’s classic text. So that’s 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 able and 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; the reader can then drill down further to work through as much of the remaining nitty-gritty that they then feel that they really want/need (though for many, that is probably not much!). 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 indeed be a great resource.
And on that happier note, let me end!
Another solution in situations like this is to divide the material in two parts: nine chapters on the topics of the present nine, but giving only essential ideas, definitions, proof outlines and general discussion; followed by as many appendices giving full details of proofs that were merely sketched in the main text. The present appendices, totalling only 20 pages, consist of recapitulatory tables and lists, and could be retained as such. It would not matter for the reader if the total length of appendices exceeded the total length of main text — though the publishers might not like it.
Such a division would make it much easier for readers coming from philosophy (and others) to find what they want without needing to skim or plough through everything and disfigure their copies with selection marks, while sometimes in doubt on what exactly to select. A text/appendix separation can also stimulate authors to be a little more expansive and clearer in their general explanations and discussions, which sometimes look a little bare when left by themselves.
By the way, an anecdote on what looks suspiciously like malpractice on the part of a certain distributor. In May or June, when the book was announced as appearing on 17 August 2021, I placed an order for a copy with Amazon France. Distribution in the UK was timely, but not so in France; OK, Brexit and covid… But time passed and at the end of August I received an email from Amazon France inviting me to cancel my order given difficulties of supply. So, I check on their website: 15 copies then in stock and still so today, no problem — but at a price 20% higher than the one that I paid for the pre-publication order. You can guess what I suspect.
I very much like the text/appendices suggestion. I suspect that doing things that way would have been all gain, for exactly the reasons you give!
Hmmmm. Annoying about Amazon. Hope this isn’t a change for the worse. I’ve done a fair amount of pre-ordering from them over the years when there was a discount announced on the list price. And so far they have always honoured the deal (even when the list price has gone up considerably in the interim). … But I’ve started using Blackwell’s a lot more (whose discounts can be terrific too).
My experience with Blackwell’s has, unfortunately, not been good. When I ordered An Introduction to Proof theory, it took nearly two weeks to arrive and was sent in one of the worst ways: they gave it to Whistl who then gave it to Hermes. (Hermes is notoriously poor.)
When I ordered a different book from Blackwell’s near the end of July, it also took quite a long time and came via Whistl.
Amazon sometimes uses a nightmare method too (typically DPD), but I’ve had very good results from them when delivery is by Amazon or by Royal Mail.
It sounds like there’s still room for a different introduction to proof theory and the consistency proof. I’d certainly be interested by a book that went along the lines your comments suggest — or in a book (or something smaller) that left the introductory proof theory to an existing book (perhaps Negri and von Plato’s Structural Proof Theory?) and focused on ordinals and the consistency proof.
However, I sometimes find it difficult to tell quite how bad you think a book is. Is it (a) so bad it should be avoided, or (b) are you just not enthusiastic and think things are better handled elsewhere?
Some of your comments on the earlier part of IPT suggested (a), at least for the part about structural proof theory. For example, on Ch 4:
At other points, it seemed more like (b). For instance, in ‘Where next?’:
In any case, I’m inclined to defend IPT, at least a bit — given that one of it’s main goals is “providing an introduction to proof theory which might serve as a companion to reading the original articles by Gerhard Gentzen”. (p viii)
If, with that goal, IPT didn’t stay so close to the systems and proofs Gentzen used in the original articles, then a student, IPT in hand, who looks at those articles, or reaches the point in IPT where it says that Gentzen used different systems (the book had better say that somewhere, and try to explain the differences), the student would be quite justified in saying
The authors presumably looked at Gentzen’s original systems and proofs and decided they didn’t make things so difficult, or so complicated, that they shouldn’t be used. (It’s not clear how much you’d disagree.)
Then consider that it’s aimed at “students, especially those in philosophy, who have only a minimal background in mathematics and logic”. (p viii). Given that target audience, it would at least be risky to cover other systems and proof styles as well. It can be hard enough to get used to working with formal systems while learning just one. The more different systems the student has to try to understand, the more confusing it can be.
Also, students with that minimal background won’t necessarily have the ‘mathematical maturity’ needed to ‘fill in’ proofs, to handle (what you described in your comments on Ch 6)
Your comments suggest that something like mathematical maturity (‘mathematical nous’ / mathematical ability and confidence) is also needed for a reader to deal effectively with the long, detailed proofs in the book:
However, that looks like an argument for giving the less mathematically sophisticated reader more help in spotting the headline ideas, rather than an argument for leaving out the details. And students are often used to doing that sort of reading anyway (skim first, etc), in other subjects. So I don’t think it should be assumed that they would just slog through.
(1) If there’s inconsistency of tone in the posts over two weeks, it’s because my reactions (and level of irritation!) varied. A summary retrospective judgement? — The book probably should be mostly avoided by its officially intended audience (at least, avoided as their initial introduction to proof theory), but could usefully be mined by more advanced readers.
(2) Would we think it sensible to introduce e.g. Gödel’s ideas and main theorems to students by sticking very closely to his original papers? Is it more sensible to introduce Gentzen’s work in that way? A bit perhaps, but not a lot. In so far as some of the mess of the book comes from wanting to cleave closely to Gentzen’s originals, I just think (in an unfriendly way) that this shows the unwisdom of introducing proof theory by this approach.
(3) On the last point “that looks like an argument …” yes — but that would, I think, argue for a differently structured presentation (as e.g. suggested in David Makinson’s comment).
At least IPT gets to Gentzen’s consistency proof. The books that are better at introducing proof theory don’t seem to. (Or is Takeuti’s book also better as an introduction?)
Structural Proof Theory, for example, says of ordinal proof theory, “This is a part of proof theory we shall not discuss.” Instead, there’s a great deal in that book that doesn’t interest me at all.
So, while SPT may well be better at introducing (structural) proof theory, it’s not better at ordinal proof theory or at explaining Gentzen’s consistency proof.
Yes indeed. That’s why I ended up with more positive comments on the final chapters of IPT. The gap in the introductory literature is indeed bigger when it comes to ordinal proof theory, and IPT fill it. So, as I said, a very useful resource which sufficiently ept students can mine. But oh, I just wish IPT were done in a much more reader-friendly way! (Am I challenging myself to try to do better?? — I have an old, half-written, rough draft short book from ten years back …!)
In practice, I imagine that most students who want to know the details of Gentzen’s proof already have a decent background in mathematical logic – e.g., they would have studied the completeness and incompleteness theorems at this point. So at least this book serves as a useful reference for those students. And future textbook authors who *don’t* want to present all the details now have the option of referring their readers to this book.
The situation reminds me a bit of the second incompleteness theorem. Since almost every book skips over the details, it would be nice to have at least *one* readable reference where students could see the details for themselves. Unfortunately, the few sources I know that claim to work through all the details of the second incompleteness theorem (like Tourlakis’s logic book) have unusual notation and terminology.
I would have really liked the inclusion of *both* Gentzen-style and Shutte-style consistency proofs. I appreciate the authors’ choice to organize the book around Gentzen’s big ideas, but it would be nice to give readers at least *some* taste of how the field has developed since then. It would also help prepare readers for tougher proof theory books (like Pohlers.)
Anyway, thanks for the review!