As I said in the last post, Chapter 7 of IPT makes a start on Gentzen’s (third, sequent calculus) proof of the consistency of arithmetic. Chapter 8 fills in enough of the needed background on ordinal induction. Then Chapter 9 completes the consistency proof. I’ll take things in a different order, commenting briefly on the relatively short ordinals chapter in this post, and then tackling the whole consistency proof (covering some 77 pages!) in the next one.
§8.1 introduces well-orders and induction along well-orderings, and §8.2 introduces lexicographical and related well-orderings. Then §§8.3 to 8.5 are a detailed account of ordinal notations for ordinals less than 𝜀0, and carefully explain how these can be well-ordered.
Mancosu, Galvan and Zach rightly make it very clear that we can get this far without taking on board any serious set theoretic commitments. In particular, the ordinal notations are finite syntactic objects and, if o1 and o2 are two distinct notations, it is decidable by a simple procedure which comes first in the well-ordering. However, §8.6 does pause to present “Set-theoretic definitions of the ordinals”, and the discussion continues in §8.7 and §8.8. These are written as if for someone who knows almost no set theory: but I suspect that they’d go too fast for a reader who hasn’t previously encountered von Neumann’s implementation of the ordinals by sets. (And I’d certainly want to resist our present authors uncritical identification of ordinals with their von Neumann implementations! — ordinals are numbers that can be modelled in set theory in the way that other kinds of numbers can be modelled in set theory, but are not themselves sets. But that’s a battle for another day!)
The chapter finishes with §8.9, where sets drop out of the picture again. We here get a brisk treatment of arguments by ordinal induction up to 𝜀0 for the termination of (i) the fight with the Hydra, and (ii) the Goodstein sequence starting from any number. These are lovely familiar examples: the discussion here is OK, but not especially neatly or excitingly done.
Back though to the earlier parts of the chapter, up to and including §8.5. These are pretty clear (though I suppose parts might go a bit quickly for some students). They should do the needed job of giving the reader enough grip on the idea of ordinal induction to be able to understand its use in Gentzen’s consistency proof. Onwards, then, to the main event …!
To be continued