Ordinal Analysis

Ordinal analysis measures the strength of a formal theory by the least ordinal that the theory cannot prove to be well-ordered, assigning a precise proof-theoretic ordinal to each theory.

Definition

The proof-theoretic ordinal of a theory is the supremum of the order types of the recursive well-orderings whose well-foundedness the theory can prove; ordinal analysis is the program of computing this invariant and using it to compare and calibrate theories.

Scope

This topic covers Gentzen's consistency proof for arithmetic using transfinite induction up to the ordinal epsilon-zero, systems of ordinal notation, the proof-theoretic ordinal as an invariant of a theory, the methods of cut-elimination for infinitary derivations, and the analysis of subsystems of arithmetic and predicative theories.

Core questions

• How does an ordinal measure the strength of an arithmetical theory?
• Why does transfinite induction up to epsilon-zero prove the consistency of arithmetic?
• How are ordinal notations defined so that they can be reasoned about finitely?
• What ordinals correspond to the standard subsystems of second-order arithmetic?

Key theories

Gentzen consistency proof

Gentzen proved the consistency of first-order arithmetic by assigning ordinals below epsilon-zero to proofs and showing cut reduction decreases them, so transfinite induction up to epsilon-zero certifies consistency.

Proof-theoretic ordinal

Each sufficiently strong theory has a characteristic ordinal capturing the transfinite induction it can justify, providing a fine-grained and largely linear scale of logical strength.

Ordinal notation systems

Large ordinals are represented by finite syntactic notations, such as the Veblen functions and collapsing functions, allowing infinite ordinals to be manipulated within finitary or arithmetical theories.

Clinical relevance

Ordinal analysis provides the most refined available measure of the strength of mathematical theories: it pins down exactly which transfinite inductions a theory needs, classifies the provably recursive functions of a theory, and supplies relative consistency information complementary to that obtained from large cardinals.

History

Gentzen's 1936 and 1938 consistency proofs for arithmetic introduced ordinal analysis through transfinite induction up to epsilon-zero. Schuette, Feferman, and others extended the method to predicative theories and ramified analysis, and the development of collapsing functions later pushed ordinal analysis into strong impredicative systems.

Key figures

• Gerhard Gentzen
• Kurt Schuette
• Solomon Feferman
• Wolfram Pohlers

Seminal works

• pohlers2009
• takeuti1987
• schutte1977

Frequently asked questions

What is the proof-theoretic ordinal of first-order arithmetic?

It is epsilon-zero, the limit of the tower of omega exponentials. First-order arithmetic proves transfinite induction up to any ordinal below epsilon-zero but not up to epsilon-zero itself, which is exactly the principle Gentzen used to prove its consistency.

How does ordinal analysis relate to incompleteness?

Goedel's second theorem says arithmetic cannot prove its own consistency. Ordinal analysis identifies the additional principle, transfinite induction up to epsilon-zero, that does prove it, thereby measuring precisely how far beyond the theory one must reach to establish its consistency.