By this I mean the consistency, or inconsistency, of certain systems of mathematical axioms. There are very few systems, of very low strength, that we know are consistent. Presburger arithmetic is complete and consistent (and even decidable, but the decision procedure is has at least doubly-exponential runtime) but cannot even define the multiplication function . Once one has a system of axioms with at least the expressive strength of Robinson arithmetic Q (which doesn’t include induction!), then Gödel’s theorem kicks in and one can construct undecidable statements in the system, including the self-consistency sentence. However, one can get consistency statements *assuming an extra fact*, namely that if one assumes that the system could prove a certain countable ordering is in fact well-founded then consistency follows. This is known as ordinal analysis, and the original result due to Gentzen is that if one has the axioms of Peano arithmetic (PA) plus the assumption that the set of finite rooted trees (with a certain natural ordering) is well-founded, then PA is consistent. This follows from careful analysis of PA proofs, which are represented (following Gentzen) as finite rooted trees. Another way to look at it is that this ordered set is the ‘smallest ordinal PA cannot prove is well-ordered’, though this requires an external viewpoint. Often people implicitly identify the set of finite rooted trees with the (von Neumann) ordinal ε_{0}.

One might ask in what system such implications are proved—what is the metatheory here? This leads to the remark in a blog post by Russell O’Connor:

As I understand, Gentzen showed that believing in the consistency of PA is equivalent to believing in the well-foundedness of ε

_{0}. This can be rephrased as a claim that a particular program, say the hydra game, terminates on all inputs. Therefore, if you believe in the well-foundness of ε_{0}and you believe Gentzen’s argument, which is done in PRA, then you believe PA is consistent, even if it has impredicative induction principles.PRA has consistency strength equivalent to the well-foundness of ω

^{ω}, which can be stated again as the termination of some other program on all inputs. Presumably this equivalence is proved in a still weaker system.

Curious about this ‘still weaker system’, I asked on MathOverflow “What is the weakest system that suffices to prove that well-foundedness of ω^{ω }implies consistency of PRA?” Emil Jeřábek provided a very nice answer, and even ironed out some wrinkles: it gets more difficult to talk about what well-foundedness means as the background theory gets weaker. Instead of the classical definition, which requires talking about subsets of the collection, one talks about induction schema instead, and how complex formulas can be that one wants to use. But in any case, the short answer is that the ‘still weaker system’ is the theory PA^{–}, which is roughly the part of PA that models an ordered semiring (ie the natural numbers with their ordering) with no induction. This is basically Robinson arithmetic, which while incomplete (after Gödel) it is “only just” incomplete.

This then gets to the heart of ordinal analysis: if one believes the fragment of arithmetic capturing the ordered semiring structure of is consistent, then well-foundedness of ω^{ω }implies consistency of PRA. So then one should feel comfortable with Gentzen’s proof that PA’s consistency follows from the well-foundedness of ε_{0}. One may, like Voevodsky, question the consistency of PA, but the soundness of the proof of the implication only requires ‘believing’ a much weaker system is consistent.

One can represent, as Jeřábek does on MathOverflow, the set ω^{ω }as the set of all finite tuples of natural numbers; in essence , with an ordering—the shortlex order—reminiscent of the plain ordering of the natural numbers expressed in some base (secretly this is base ω!). I have a hard time imagining how this can fail to be well-founded, if I make the background assumption that ω itself is well-founded. And that is the point: one reduces consistency arguments to very concrete syntactical structures. We try to bootstrap ourselves up into believing systems are consistent through this process, though we really don’t know what the ordinal consistency strength for eg ZFC or even Z is.

One could try to go down the rabbit hole, and ask what is the corresponding result for Q: what well-foundedness statement is enough to prove Q’s consistency? But it appears that the theories are getting so weak that one needs to resort to different tools. As far as PA is concerned, Timothy Chow gives a conceptual statement (see Theorem 2) equivalent to the well-foundedness of ε_{0}

THEOREM 2. If M is a Turing machine that given i as input, outputs an ordinal M(i), and M(i) ≥ M(i+1) for all i, then the sequence stabilizes.

with a footnote saying “the theorem can be further weakened to assert the stabilization of all primitive recursive descending sequences of ordinals”. (Here by “ordinals” Chow means something he describes in finitary terms using finite nested lists à la Lisp)

If you find it ‘intuitive’ that ω^{ω }is well-founded, and Theorem 2 of Chow’s note convincing, then you have just been convinced that PA is consistent.