# 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 ${\displaystyle T}$ is the smallest recursive ordinal that the theory cannot prove is 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}$.

The existence of any recursive ordinal that the theory fails to prove is well ordered follows from the ${\displaystyle \Sigma _{1}^{1}}$ bounding theorem, as the set of natural numbers that an effective theory proves to be ordinal notations is a ${\displaystyle \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 ${\displaystyle \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.[1]
• 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 ${\displaystyle {\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

• ${\displaystyle \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 ${\displaystyle 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 ${\displaystyle \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.)