Ordinal analysis

In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In addition to obtaining the proof-theoretic ordinal of a theory, in practice ordinal analysis usually also yields various other pieces of information about the theory being analyzed, for example characterizations of the classes of provably recursive, hyperarithmetical, or ${\displaystyle \Delta _{2}^{1}}$ functions of the theory.

The field of ordinal analysis was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof-theoretic ordinal of Peano arithmetic is ε₀. See Gentzen's consistency proof.

Ordinal analysis concerns true, effective (recursive) theories that can interpret a sufficient portion of arithmetic to make statements about ordinal notations.

The proof-theoretic ordinal of such a theory ${\displaystyle T}$ is the supremum of the order types of all ordinal notations (necessarily recursive, see next section) that the theory can prove are well founded—the supremum of all ordinals ${\displaystyle \alpha }$ for which there exists a notation ${\displaystyle o}$ in Kleene's sense such that ${\displaystyle T}$ proves that ${\displaystyle o}$ is an ordinal notation. Equivalently, it is the supremum of all ordinals ${\displaystyle \alpha }$ such that there exists a recursive relation ${\displaystyle R}$ on ${\displaystyle \omega }$ (the set of natural numbers) that well-orders it with ordinal ${\displaystyle \alpha }$ and such that ${\displaystyle T}$ proves transfinite induction of arithmetical statements for ${\displaystyle R}$.

Some theories, such as subsystems of second-order arithmetic (Z₂), have no conceptualization or way to make arguments about transfinite ordinals. For example, to formalize what it means for a subsystem ${\displaystyle T}$ of Z₂ to "prove ${\displaystyle \alpha }$ well-ordered", we instead construct an ordinal notation ${\displaystyle (A,{\tilde {<}})}$ with order type ${\displaystyle \alpha }$. ${\displaystyle T}$ can now work with various transfinite induction principles along ${\displaystyle (A,{\tilde {<}})}$, which substitute for reasoning about set-theoretic ordinals.

However, some pathological notation systems exist that are unexpectedly difficult to work with. For example, Rathjen gives a primitive recursive notation system ${\displaystyle (\mathbb {N} ,<_{T})}$ that is well-founded if and only if PA is consistent,^{p. 3} despite having order type ${\displaystyle \omega }$. Including such a notation in the ordinal analysis of PA would result in the false equality ${\displaystyle {\mathsf {PTO(PA)}}=\omega }$.

Since an ordinal notation must be recursive, the proof-theoretic ordinal of any theory is less than or equal to the Church–Kleene ordinal ${\displaystyle \omega _{1}^{\mathrm {CK} }}$. In particular, the proof-theoretic ordinal of an inconsistent theory is equal to ${\displaystyle \omega _{1}^{\mathrm {CK} }}$, because an inconsistent theory trivially proves that all ordinal notations are well-founded.