Ordinal analysis

In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. The field was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof-theoretic ordinal of Peano arithmetic is ε0.

Definition

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 $T$ is the smallest recursive ordinal that the theory cannot prove is well founded—the supremum of all ordinals $\alpha$ for which there exists a notation $o$ in Kleene's sense such that $T$ proves that $o$ is an ordinal notation. Equivalently, it is the supremum of all ordinals $\alpha$ such that there exists a recursive relation $R$ on $\omega$ (the set of natural numbers) that well-orders it with ordinal $\alpha$ and such that $T$ proves transfinite induction of arithmetical statements for $R$ .

The existence of any recursive ordinal that the theory fails to prove is well ordered follows from the $\Sigma _{1}^{1}$ bounding theorem, as the set of natural numbers that an effective theory proves to be ordinal notations is a $\Sigma _{1}^{0}$ set (see Hyperarithmetical theory). Thus the proof-theoretic ordinal of a theory will always be a countable ordinal less than the Church–Kleene ordinal $\omega _{1}^{\mathrm {CK} }$ .

In practice, the proof-theoretic ordinal of a theory is a good measure of the strength of a theory. 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.

Examples

Theories with proof-theoretic ordinal ω2

• RFA, rudimentary function arithmetic.
• 0, arithmetic with induction on Δ0-predicates without any axiom asserting that exponentiation is total.

Theories with proof-theoretic ordinal ω3

Friedman's grand conjecture suggests that much "ordinary" mathematics can be proved in weak systems having this as their proof-theoretic ordinal.

Theories with proof-theoretic ordinal ωn (for n = 2, 3, ... ω)

• 0 or EFA augmented by an axiom ensuring that each element of the n-th level ${\mathcal {E}}^{n}$ of the Grzegorczyk hierarchy is total.

Theories with proof-theoretic ordinal the Feferman–Schütte ordinal Γ0

This ordinal is sometimes considered to be the upper limit for "predicative" theories.

Theories with larger proof-theoretic ordinals

• $\Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}$ , Π11 comprehension has a rather large proof-theoretic ordinal, which was described by Takeuti in terms of "ordinal diagrams", and which is bounded by ψ0ω) in Buchholz's notation. It is also the ordinal of $ID_{<\omega }$ , the theory of finitely iterated inductive definitions.
• T0, Feferman's constructive system of explicit mathematics has a larger proof-theoretic ordinal, which is also the proof-theoretic ordinal of the KPi, Kripke–Platek set theory with iterated admissibles and $\Sigma _{2}^{1}{\mbox{-}}{\mathsf {AC}}+{\mathsf {BI}}$ .
• KPM, an extension of Kripke–Platek set theory based on a Mahlo cardinal, has a very large proof-theoretic ordinal ϑ, which was described by Rathjen (1990).
• MLM, an extension of Martin-Löf type theory by one Mahlo-universe, has an even larger proof-theoretic ordinal ψΩ1M + ω).

Most theories capable of describing the power set of the natural numbers have proof-theoretic ordinals that are so large that no explicit combinatorial description has yet (as of 2008) been given. This includes second-order arithmetic and set theories with powersets. (The CZF and Kripke-Platek set theories mentioned above are weak set theories without powersets.)