Ordinal Logic

Origin. Alan Turing, Systems of Logic Based on Ordinals (PhD thesis under Church, 1938; published 1939) — the work he did between the halting problem and Bletchley Park, and the deepest response to incompleteness anyone made. Solomon Feferman, "Transfinite recursive progressions of axiomatic theories" (1962), reworked it and drew the conclusions; Feferman and Spector (1962) supplied the limitative results.

Models. Gödel: a consistent theory cannot prove its own consistency. So add its consistency as an axiom. The new theory cannot prove its consistency either — so add that, and iterate. The iteration is transfinite, and Turing's question is whether it terminates in something complete. It does, and the answer is worse than a failure: the completeness is real and the ordinal notation is doing all the work.

Formalism.

The progression: T₀ = PA T_{α+1} = T_α + Con(T_α) T_λ = ⋃_{α<λ} T_α for limit λ

The notation problem: "T_α" is not well defined by the ordinal α. To state Con(T_α) you must describe T_α, so the progression is indexed by ordinal notations a ∈ 𝒪 (Kleene's system), not by ordinals. Different notations for the same ordinal give different theories.

Turing's completeness theorem (1939): For every true Π⁰₁ sentence φ, there is a notation a ∈ 𝒪 with |a| = ω + 1 such that T_a ⊢ φ. Completeness for Π⁰₁ at level ω+1 — almost the bottom of the hierarchy.

Why that is a defeat: The notation a encodes φ's truth. Recognizing a as a notation is as hard as knowing φ. The progression is complete and the completeness is not effective: you cannot find a without already having what you wanted. Turing called the residue "intuition" and left it there.

Feferman's reflection progressions (1962): Iterate uniform reflection — ∀x (Prov_T(⌜φ(ẋ)⌝) → φ(x)) — rather than consistency. Gives Π⁰₂-completeness, and behaves better.

Autonomous progressions: Only use a notation once the theory has proved it is a notation. The autonomous closure of the reflection progression over PA has proof-theoretic ordinal Γ₀. Feferman–Schütte: Γ₀ is the limit of predicativity. Ordinal logic is where that number comes from.

Feferman–Spector (1962): There are paths through 𝒪 along which the progression is Π⁰₁-complete for the wrong reason — the completeness is an artifact of the path, and paths can be chosen to prove false Π⁰₂ sentences. The notation dependence is not a technicality.

Symbols.

Metatheory. Turing's theorem is the sharpest statement of what incompleteness costs: completeness is achievable, at level ω+1, and the price is that the index does the proving. That is not a defect in the construction — it is what the construction reveals, and it is why the subject is a philosophical result rather than a technique. Feferman's autonomous progressions turn it into one: by refusing notations the theory cannot certify, the iteration acquires a definite limit, and that limit is Γ₀ — so the analysis of predicativity is a corollary of Turing's thesis. Feferman–Spector shows the notation dependence cannot be argued away.

Applies to. Responses to incompleteness. Ordinal analysis and proof-theoretic strength. Predicativity and the Feferman–Schütte ordinal. Reflection principles. The philosophy of mathematical intuition, where Turing's residue is the standing problem.

Limitations. The completeness is not effective and the notation carries the content, so nothing is gained that was not assumed — which is the theorem, and which makes the progression useless as a method. Kleene's 𝒪 is Π¹₁-complete, so recognizing notations is as hard as the hierarchy it indexes. Feferman–Spector's pathological paths show the dependence is essential rather than an artifact of the notation system chosen. And Turing's own conclusion — that what remains is intuition — is a name for the gap and not an account of it.

© 2026 Lingenic LLC