Ordinal Notations and Proof Theory

Ordinal notations provide concrete representations of ordinals, enabling their use in proof theory and computability theory to measure the strength of formal systems.

Ordinal Notation Systems

Definition7.3Ordinal notation

An ordinal notation system is a recursive set of terms $T$ together with a well-ordering $\prec$ on $T$ such that $\mathrm{otype}(T, \prec)$ equals a specific ordinal. A key requirement is that the ordering $\prec$ is decidable (computable), so that the ordinal can be "manipulated" by algorithms.

ExampleCantor normal form as notation

For ordinals below $\varepsilon_0$ , the Cantor normal form provides a natural notation:

$\alpha = \omega^{\beta_1} c_1 + \cdots + \omega^{\beta_k} c_k$

where each $\beta_i < \alpha$ (since $\alpha < \varepsilon_0 \implies \omega^\alpha > \alpha$ ). The ordering of such terms is decidable by comparing exponents and coefficients. This notation system represents exactly the ordinals below $\varepsilon_0$ .

Proof-Theoretic Ordinals

Definition7.4Proof-theoretic ordinal

The proof-theoretic ordinal of a theory $T$ is the supremum of the ordinals $\alpha$ for which $T$ proves that $\alpha$ is well-ordered (when coded by a standard ordinal notation). It measures the "consistency strength" of $T$ .

Theorem7.2Gentzen's theorem

The proof-theoretic ordinal of Peano arithmetic (PA) is $\varepsilon_0$ . That is:

For every $\alpha < \varepsilon_0$ , PA proves that $\alpha$ (in Cantor normal form notation) is well-ordered.
PA does not prove that $\varepsilon_0$ is well-ordered.
The consistency of PA can be proved by induction up to $\varepsilon_0$ (Gentzen, 1936).

ExampleProof-theoretic ordinals of various theories

| Theory | Proof-theoretic ordinal | |---|---| | Primitive recursive arithmetic (PRA) | $\omega^\omega$ | | Peano arithmetic (PA) | $\varepsilon_0 = \omega^{\omega^{\omega^{\cdots}}}$ | | ATR $_0$ (arithmetical transfinite recursion) | $\Gamma_0$ | | $\Pi^1_1$ -CA $_0$ | $\psi_0(\Omega_\omega)$ | | Second-order arithmetic (full) | Unknown |

Goodstein's Theorem

RemarkGoodstein's theorem

A remarkable application of transfinite induction to $\varepsilon_0$ : Goodstein's theorem states that every Goodstein sequence eventually reaches $0$ .

A Goodstein sequence starts with a natural number $n$ , writes it in "hereditary base $b$ " notation, replaces $b$ by $b+1$ , subtracts 1, and repeats. Despite growing enormously at first, every sequence eventually terminates.

The proof uses the embedding into ordinals below $\varepsilon_0$ : replacing base $b$ by $\omega$ gives a decreasing sequence of ordinals (since $b+1 \to \omega$ preserves order but subtraction lowers the ordinal). By well-ordering of $\varepsilon_0$ , the sequence terminates.

Remarkably, Goodstein's theorem is unprovable in PA (Kirby-Paris, 1982), despite being a statement about natural numbers.