Overview
Ordinal logics are formal systems that extend a base theory (such as Peano arithmetic) by iteratively adding consistency statements or reflection principles indexed by ordinals, typically recursive ordinals, thereby creating a transfinite hierarchy of increasingly strong theories. The concept was introduced by Alan Turing in his 1939 PhD thesis "Systems of Logic Based on Ordinals" as a constructive response to Gödel's incompleteness theorems. Ordinal logics provide a method to systematically "defeat" incompleteness by climbing the ordinal hierarchy, though they themselves remain incomplete. They have since become a central tool in proof theory, particularly in ordinal analysis, where the ordinal strength of a theory is measured by its proof-theoretic ordinal.
1 Background
1.1 Gödel’s incompleteness theorems
Gödel’s first incompleteness theorem (1931) states that any consistent formal system capable of expressing basic arithmetic contains a sentence that is true but not provable within the system. The second incompleteness theorem further shows that such a system cannot prove its own consistency. These results impose fundamental limits on the reach of formal deduction, implying that no single recursively axiomatizable theory can capture all arithmetical truths.
1.2 The need for transfinite iterations
Gödel’s theorems suggest that to prove more truths, one must move to stronger theories. A natural approach is to add a consistency statement for a given theory T (e.g., Con(T)) as a new axiom, yielding a stronger theory T+Con(T). This process can be repeated, but after finitely many steps it reaches a fixed point in expressibility. To go further, one must iterate the process transfinitely, using ordinals to index the stages. Ordinal logics formalize this iterative construction, allowing the hierarchy to extend into the transfinite.
2 Turing’s ordinal logics
2.1 Definition and construction
Turing defined an ordinal logic as a system that assigns to each ordinal (or, more precisely, to each notation for a recursive ordinal) a formal theory. Starting from a base theory (say, Peano arithmetic), one defines a progression: for an ordinal \(\alpha\), the theory \(T_\alpha\) is obtained by adding to the union of all earlier theories the statement that each earlier theory is consistent. For successor ordinals, this step is well-defined; for limit ordinals, one takes the union of the earlier theories. The result is a transfinite chain of theories of increasing strength.
2.2 Use of ordinal notations
Because ordinals themselves are abstract objects, Turing needed a concrete way to represent them within arithmetic. He used systems of ordinal notations, which assign natural numbers (or finite sequences) to recursive ordinals. The notation system provides a computational handle on the ordinal hierarchy, enabling the iterative construction to be described arithmetically.
2.2.1 Kleene’s O and recursive ordinals
A particularly important notation system was later developed by Stephen Kleene: Kleene’s \(\mathcal{O}\), which encodes the recursive ordinals (those that are order types of recursive well-orderings). \(\mathcal{O}\) is a set of natural numbers with a partial order relation that mirrors ordinal comparison. Every recursive ordinal has at least one notation in \(\mathcal{O}\), but \(\mathcal{O}\) is itself not recursive—it is a \(\Pi^1_1\)-complete set. Turing’s original work predated Kleene’s system; he used a simpler notation based on Church’s lambda calculus.
2.3 Properties and limitations
2.3.1 Incompleteness of the hierarchy
Despite being transfinite, Turing’s ordinal logics are still subject to Gödel’s theorems. For any fixed ordinal notation system, the resulting hierarchy of theories is itself incomplete: there exist true arithmetical sentences not provable in any theory of the progression. The hierarchy can be continued further by choosing a larger ordinal, but the choice of notation becomes crucial: two different notations for the same ordinal may yield theories of different strength.
2.3.2 Relationship with the Turing jump
Turing observed a close connection between ordinal logics and the Turing jump, an operation in computability theory that takes a set of natural numbers to its halting problem. Adding a consistency statement corresponds roughly to taking the jump of the set of theorems of the original theory. Climbing the ordinal hierarchy parallels iterating the Turing jump along a path through the recursive ordinals, a concept later formalized as the hyperarithmetical hierarchy.
3 Later developments
3.1 Feferman’s transfinite progressions
3.1.1 Axiomatic reflection principles
Solomon Feferman (1962) refined Turing’s approach by replacing mere consistency statements with reflection principles. A reflection principle for a theory T asserts that any sentence provable in T is true. Feferman showed that progressions using uniform reflection principles (e.g., \(\mathsf{RFN}(T)\)) yield a smoother relationship with the ordinal hierarchy and can be used to characterize the theorems of various subsystems of arithmetic.
3.1.2 Autonomous progressions
Feferman also introduced the concept of autonomous progressions, where the ordinal notations used are only those that can be proved to be well-ordered within the theories already constructed. This approach yields a least fixed point, known as Feferman’s theory \(\widehat{\mathsf{ID}}_1\) or the system of predicative analysis. Autonomous progressions provide a natural stopping point that corresponds to the limit of predicative mathematics.
3.2 Ordinal analysis
3.2.1 Proof-theoretic ordinals
Ordinal analysis measures the strength of a formal theory by assigning to it a proof-theoretic ordinal—the smallest ordinal that cannot be proved to be well-ordered within the theory. This ordinal is often presented in terms of a notation system based on ordinal collapsing functions. The proof-theoretic ordinal of Peano arithmetic is \(\varepsilon_0\), that of the theory of arithmetical comprehension (\(\mathsf{ACA}_0\)) is also \(\varepsilon_0\), and stronger theories have larger ordinals (e.g., \(\Gamma_0\) for \(\mathsf{ATR}_0\), \(\psi(\Omega_\omega)\) for \(\Pi^1_1\)-\(\mathsf{CA}_0\)).
3.2.2 Major ordinal analyses (e.g., PA, arithmetical comprehension)
The ordinal analysis of Peano arithmetic (\(\varepsilon_0\)) was carried out by Gentzen (1936) using cut elimination. For the subsystem \(\mathsf{ACA}_0\) of second-order arithmetic, the ordinal is also \(\varepsilon_0\), reflecting its proof-theoretic equivalence with PA. Stronger systems such as \(\mathsf{ATR}_0\) (ordinal \(\Gamma_0\)) and \(\Pi^1_1\)-\(\mathsf{CA}_0\) (ordinal \(\psi(\Omega_\omega)\)) have been analyzed by Feferman, Schütte, Buchholz, and others. These analyses often involve complex ordinal notation systems and are central to modern proof theory.
3.3 Connections to reverse mathematics
Reverse mathematics investigates which set existence axioms are necessary to prove theorems of ordinary mathematics. Subsystems of second-order arithmetic are ranked by their proof-theoretic ordinals, and ordinal logics provide a framework for understanding the relative strength of these subsystems. For instance, the progression based on \(\mathsf{ACA}_0\) corresponds to iterating the Turing jump along \(\omega\), while stronger systems correspond to hyperarithmetical or even higher iterations.
4 Applications
4.1 Foundational issues in mathematics
Ordinal logics serve as a tool for calibrating the proof-theoretic strength of mathematical theories. They help delimit the boundaries of predicative mathematics, provide consistency proofs for subsystems of analysis, and illuminate the relationship between constructive and classical mathematics. The autonomous progression of Feferman, for example, yields a theory that captures predicative reasoning, a foundational stance that avoids impredicative definitions.
4.2 Computational aspects
4.2.1 Feasible ordinal notations
In practice, the applicability of ordinal logics depends on having manageable ordinal notations. Notations based on Madore’s \(\psi\) function, Bachmann–Howard ordinals, or the \(\theta\) function are used in ordinal analysis to represent ordinals up to the limit of well-known theories. These notations must be primitive recursive (or at least computable) to be used in formal theories. Research continues on finding notations that are both expressive and feasible for computer-assisted proof theory.
5 Open problems and current research
5.1 Limits of ordinal analysis
Ordinal analysis has been successfully applied to theories up to the strength of \(\Pi^1_2\)-comprehension and beyond, but the exact proof-theoretic ordinals for very strong theories (e.g., Zermelo–Fraenkel set theory) remain unknown. It is unclear whether a “natural” ordinal notation system can capture the full strength of such theories, or whether ordinal analysis as a method has a fundamental upper bound.
5.2 Relation to ω-logic and completeness
There is ongoing interplay between ordinal logics and \(\omega\)-logic (logic that admits infinite proofs). \(\omega\)-logic is complete for arithmetical sentences in a certain sense, and ordinal logics can be seen as finite approximations to \(\omega\)-logic. The question of how to characterize the set of arithmetical truths via transfinite iterations of reflection or consistency is still actively investigated, with connections to the concept of “ordinal completeness” and the structure of the hyperarithmetical hierarchy.