Ordinal analysis

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength.

Definition

All theories discussed are assumed to be recursive countable theories, and are assume to be powerful enough to make statements about the natural numbers.

The proof theoretic ordinal of a theory is the smallest recursive ordinal that the theory cannot prove is well founded.

The proof theoretic ordinal of a theory is a countable ordinal less than the Church-Kleene ordinal. It is in practice a good measure of the strength of a theory. If theories have the same proof theoretic ordinal they are often equiconsistent, and if one has a larger proof theoretic ordinal than another it can often prove the consistence of the second theory.

Examples

• Gentzen showed using cut elimination that the proof theoretic ordinal of Peano arithmetic is ε₀.
• ${\mathsf {RCA}}_{0}$, Recursive Comprehension has proof theoretic ordinal ω^ω.
• ${\mathsf {WKL}}_{0}$, Weak König's lemma has proof theoretic ordinal ω^ω.
• ${\mathsf {ACA}}_{0}$, Arithmetical comprehension has proof theoretic ordinal ε₀.
• ${\mathsf {ATR}}_{0}$, Arithmetical Transfinite Recursion has proof theoretic ordinal the Feferman-Schütte ordinal Γ₀.
• $\Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}$, $\Pi _{1}^{1}$ comprehension has a rather large proof theoretic ordinal.

References

• Pohlers, W., Proof theory