Let’s pause to take stock. Chapters 3 to 6 of IPT comprise some two hundred pages — a book’s worth in itself — on Gentzen-style natural deduction and normalization theorems, and then on the sequent calculus and cut-elimination theorems. These topics are much-discussed elsewhere, at various levels of sophistication. What’s distinctive about the coverage of IPT is that it is (i) supposed to be accessible to near beginners in logic, while (ii) sticking pretty closely to discussing Gentzen’s own formal systems, and Gentzen’s own proofs about them (and later developments of them): “One of the main goals we set for ourselves,” say the authors, “is that of providing an introduction to proof theory which might serve as a companion to reading the original articles by Gerhard Gentzen.” Moreover, (iii) “In order to make the content accessible to readers without much mathematical background, we carry out the details of proofs in much more detail than is usually done.”
In discussing these four chapters, I’ve quibbled about various points of presentation. But I suppose my main unhappiness has been about the overall shape of the project itself, given the intended readership. Gentzen is often a remarkably clear writer; but I’m not at all convinced that sticking so closely to his original papers is the best way to start learning about structural proof theory. And I’m even less convinced that giving massively detailed proofs is the way to help the beginner get clear about the Big Ideas (especially when so many of the details are pretty tedious, and are made more tedious by the decision to cleave to Gentzen’s original formal systems). Of course, I’m not the intended naive reader, and (unlike the authors!) I haven’t given lecture courses on proof theory: maybe their approach works a treat with many students. All I can do is register my doubts, and (as I have done in passing) suggest familiar alternatives that on balance I would recommend more warmly to beginners, who can then dip into IPT if/when they feel the need.
But now we move on to the last three chapters of the book. These focus on Gentzen’s third proof of the consistency of arithmetic — the one using ordinal induction in the setting of a sequent calculus presentation of arithmetic. Chapter 7 makes a start at setting up the proof. Chapter 8 pauses to explain ordinal notations and the idea of ordinal induction. Then the final Chapter 9 makes use of ordinal induction to complete the consistency proof.
Now, while there are quite a few other options for expositions of natural deduction and sequent calculi available for readers with different levels of mathematical sophistication but little background logic, here the situation is surely quite different. Yes, there are a fair number of very short presentations (a few paragraphs) giving an arm-waving explanation of the basic proof-idea of Gentzen’s second or third proofs: but we don’t have even an handful of worked through but still accessible accounts of how the argument goes. There’s the chapter in Gaisi Takeuti’s justly admired 1975 Proof Theory, but that’s fairly tough going for anyone. I’ve seen the long Chapter 1 of Wolfram Pohler’s 1989 Proof Theory described as giving “a very clean, streamlined approach”, but — to say the very least — it will be impenetrable for the relative beginner. There’s a little 77 page 2014 book by Anna Horská with the promising title Where is the Gödel-Point Hiding: Gentzen’s Consistency Proof of 1936 and his Representation of Constructive Ordinals. It’s dreadful. What else is there?
Paolo Mancosu, Sergio Galvan and Richard Zach therefore have little competition here. Any decent presentation of Gentzen’s argument which makes it more available will be very welcome. And, taking a very superficial look at the next chapter, it seems that you don’t have to have read all the previous chapters in order to join the party here. Assuming you already know a bit about the sequent calculus and cut elimination proofs, my impression is that a quick skim of Chapter 6 will be enough to set you up for diving into Chapter 7. Which is good.
These final chapters are the ones that I’ve been most looking forward to seeing: so how do they work out?
To be continued