When mathematicians construct formal systems—the precise languages in which we express mathematical truths—a natural question emerges: how do we measure the strength of such a system? Not merely its elegance or utility, but its fundamental power to demonstrate truths within its own framework.
I remember sitting in a graduate seminar on mathematical logic, watching my professor draw two formal systems on the board—one capturing basic arithmetic, another extending it with principles about infinite sets. “Which is stronger?” he asked. The immediate response seemed obvious: the second, clearly. But then came the challenge: “Prove it. Give me a precise, numerical measure of exactly how much stronger.” The room fell silent. We could all see intuitively that one system reached further than the other, but translating that intuition into rigorous mathematics proved far from trivial.
This question leads us into one of mathematical logic’s most sophisticated tools: ordinal analysis, which assigns to each formal theory a specific “proof-theoretic ordinal” that measures its logical reach with remarkable precision. What began as an apparently simple question about comparing formal systems opens onto a profound machinery for mapping the entire hierarchy of mathematical reasoning.
The problem of measuring logical strength
Consider two different mathematical theories. One might prove all the theorems of basic arithmetic—addition, multiplication, the fundamental theorem of arithmetic. Another might additionally prove theorems about infinite sets, or establish the consistency of weaker systems. Intuitively, the second theory is “stronger” than the first. But can we make this intuition precise?
The challenge runs deeper than mere counting. We cannot simply tally how many theorems each theory proves, since both might prove infinitely many statements. Nor can we rely solely on which specific theorems they prove, since theories may be equivalent in power while expressing quite different mathematical content. What we need is a measure that captures something essential about a theory’s logical architecture—its capacity to reach higher levels of proof complexity.
This is precisely what ordinal analysis provides. As Solomon Feferman observes, “The aim of ordinal analysis is to measure the proof-theoretic strength of formal systems by associating with each system an ordinal that characterizes the extent of transfinite induction provable in the system.”1 The proof-theoretic ordinal of a theory represents, in a sense, how far “up” the hierarchy of logical complexity that theory can climb.
Starting simple: primitive recursive arithmetic
To understand how ordinals measure logical strength, we begin with Primitive Recursive Arithmetic (PRA), one of the weakest interesting systems in mathematical logic. PRA formalizes our intuitive notion of computation through primitive recursion: we can define functions by specifying their value at zero and giving a rule for computing f(n+1) from f(n). Every primitive recursive function is guaranteed to halt—we never encounter infinite loops or uncomputable operations.
Despite its apparent simplicity, PRA proves a substantial portion of elementary number theory. It can establish basic facts about addition and multiplication, prove that every number has a unique prime factorization, and verify the correctness of many concrete algorithms. What it cannot do, crucially, is prove its own consistency. This limitation is no accident—it follows from Gödel’s second incompleteness theorem, which demonstrates that any sufficiently strong consistent system cannot prove its own consistency from within.2
The proof-theoretic ordinal of PRA is ωω, the first ordinal beyond all finite powers ωn.3 This ordinal captures something fundamental about PRA’s limitations: the system can handle any fixed finite level of iteration, but it cannot “climb above itself” to grasp the full structure of primitive recursion as a single completed whole.
Moving upward: Peano Arithmetic
When we strengthen PRA by adding full mathematical induction as an axiom scheme—the principle that if a property holds for zero and is preserved by succession, then it holds for all natural numbers—we obtain Peano Arithmetic (PA), the standard formalization of elementary number theory. This seemingly modest addition yields dramatic consequences.
PA proves everything PRA proves and vastly more. Crucially, PA can prove the consistency of PRA, demonstrating that no contradiction follows from PRA’s axioms. This represents a genuine increase in logical power: PA reaches a level of reflective understanding about formal systems that PRA cannot attain. PA can, in a precise technical sense, “stand outside” PRA and verify its coherence.
The proof-theoretic ordinal of PA is ε0, the first epsilon number—the first ordinal α such that ωα = α.4 This ordinal marks a significant threshold in the hierarchy of recursive ordinals. While ε0 remains countable and recursively describable, it represents a fixed point in exponential iteration, capturing PA’s capacity to reason about arbitrarily nested applications of its induction principle.
The relationship between these ordinals reflects the logical relationship between the theories. Since ωω < ε0, we obtain a precise numerical confirmation of our intuitive judgment that PA is stronger than PRA. Moreover, this relationship explains why PA can prove PRA’s consistency: PA can carry out transfinite induction up to ε0, which suffices to formalize a proof of PRA’s consistency by induction up to ωω.
The general pattern: from theories to ordinals
The assignment of proof-theoretic ordinals follows a systematic procedure, though the technical details grow complex rapidly. The central idea, developed through the work of Gerhard Gentzen, Gaisi Takeuti, and others, involves analyzing the structure of proofs themselves.5
Every proof in a formal system can be viewed as a tree of logical inferences, with axioms at the leaves and the theorem to be proved at the root. By assigning ordinal “measures” to these proof trees—capturing their complexity in terms of how many times certain logical rules are applied and in what patterns—we can determine the smallest ordinal up to which the theory must be able to carry out transfinite induction in order to verify all its proofs.
This proof-theoretic ordinal serves as a precise measure of the theory’s strength. In many natural cases, if theory T₁ has proof-theoretic ordinal α and theory T₂ has proof-theoretic ordinal β, with α < β, then T₂ is provably stronger than T₁: specifically, T₂ can, under standard soundness and representability assumptions, prove the consistency of T₁, but T₁ cannot prove the consistency of T₂. As Michael Rathjen explains, “The proof-theoretic ordinal provides a yardstick for comparing the strength of theories and serves to delineate a theory’s proof-theoretic reach.”6
Beyond arithmetic: second-order theories
The hierarchy extends far beyond elementary arithmetic. When we move to second-order arithmetic—systems that can quantify not just over numbers but over sets of numbers—we encounter theories of dramatically increased strength, measured by correspondingly larger ordinals.
The system ACA0 (arithmetical comprehension with restricted induction), which allows us to form sets defined by arithmetical formulas, has proof-theoretic ordinal ε0, placing it on par with first-order PA.7 But stronger subsystems like ATR0 (arithmetical transfinite recursion) reach proof-theoretic ordinal Γ0, the Feferman-Schütte ordinal, which represents the limit of predicatively definable ordinals—ordinals we can define without appealing to the completed infinite.8
Moving further up the hierarchy, the system Π11-CA0 (comprehension for Π11 formulas) encompasses much of ordinary mathematical practice, including substantial portions of analysis and topology. Its proof-theoretic ordinal climbs into the realm of recursively large ordinals, far beyond the reach of simple transfinite iteration.9
What ordinals capture: the syntactic-semantic bridge
The profound achievement of ordinal analysis lies in forging a precise connection between purely syntactic operations (formal proofs) and semantic mathematical content (the actual mathematical structures theories describe). A theory’s proof-theoretic ordinal captures its ability to “prove its own proving,” to reflect upon and verify the consistency of its own logical operations.
This reflexive capacity represents genuine logical strength because consistency is fundamental. A theory that can verify the consistency of another theory can, in principle, justify confidence in that theory’s mathematical content. The hierarchy of ordinals thus mirrors a hierarchy of mathematical trust: stronger theories provide firmer foundations for weaker ones, though no consistent theory can fully ground itself.
As Wilfried Sieg notes, ordinal analysis reveals “structural features of proofs that correspond to mathematical operations needed for establishing theorems.”10 The ordinal assigned to a theory isn’t arbitrary; it reflects the actual mathematical resources—the iterative depth, the complexity of induction, the reach of recursive definitions—that the theory mobilizes in its demonstrations.
Contemporary significance and open questions
Modern ordinal analysis extends these techniques to far stronger systems, including fragments of set theory and theories with large cardinal axioms. Researchers have computed proof-theoretic ordinals for systems approaching the strength of ZFC (Zermelo-Fraenkel set theory with the axiom of choice) including fragments of set theory and systems that capture substantial parts of ZFC-style reasoning, though complete ordinal analyses for the strongest theories remain conjectural.11
The methodology also illuminates philosophical questions about mathematical knowledge. If we cannot prove a theory’s consistency within itself, does ordinal analysis provide an alternative path to justification? Can we trust the assignment of ordinals without circular reasoning? These questions remain actively debated, connecting technical results in proof theory to fundamental epistemological concerns.12
What remains undeniable is ordinal analysis’s success in creating a precise, mathematically rigorous measure of logical strength. By assigning specific ordinals to formal theories, mathematicians have constructed a map of the logical universe—a hierarchy showing how different mathematical systems relate to one another in provable power and reflective capacity. This hierarchy doesn’t merely describe mathematical practice; it reveals something deep about the structure of mathematical reasoning itself, showing how syntax and semantics intertwine in the architecture of formal proof.
- Feferman, Solomon. “Proof Theory: A Personal Report.” In Proof, Logic and Formalization, edited by Godehard Link, 447-485. London: Routledge, 1992, p. 451. ↩︎
- Gödel, Kurt. “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.” Monatshefte für Mathematik und Physik 38, no. 1 (1931): 173-198. ↩︎
- Schwichtenberg, Helmut. “Proof Theory: Some Applications of Cut-Elimination.” In Handbook of Mathematical Logic, edited by Jon Barwise, 867-895. Amsterdam: North-Holland, 1977, p. 889. ↩︎
- Gentzen, Gerhard. “Die Widerspruchsfreiheit der reinen Zahlentheorie.” Mathematische Annalen 112, no. 1 (1936): 493-565. ↩︎
- Takeuti, Gaisi. Proof Theory, 2nd ed. Amsterdam: North-Holland, 1987. ↩︎
- Rathjen, Michael. “The Art of Ordinal Analysis.” In Proceedings of the International Congress of Mathematicians, Vol. II, 45-69. New Delhi: Hindustan Book Agency, 2010, p. 46. ↩︎
- Simpson, Stephen G. Subsystems of Second Order Arithmetic, 2nd ed. Cambridge: Cambridge University Press, 2009, p. 106. ↩︎
- Feferman, Solomon, and Kurt Schütte. “Predicative Ordinal Analysis.” Mathematische Annalen 141, no. 1 (1960): 1-60. ↩︎
- Simpson, Subsystems of Second Order Arithmetic, p. 397. ↩︎
- Sieg, Wilfried. “Hilbert’s Programs: 1917-1922.” The Bulletin of Symbolic Logic 5, no. 1 (1999): 1-44, p. 38. ↩︎
- Rathjen, Michael. “Ordinal Analysis of Set Theories.” In The Oxford Handbook of Philosophy of Mathematics and Logic, edited by Stewart Shapiro, 485-503. Oxford: Oxford University Press, 2005. ↩︎
- Franzen, Torkel. Inexhaustibility: A Non-Exhaustive Treatment. Wellesley, MA: A K Peters, 2004. ↩︎