The Measure

Fix a consistent theory T that is recursively axiomatized and strong enough to formalize its own syntax — at minimum EA (elementary arithmetic, I∆₀+exp), so that the provability predicate Prov_T satisfies the Hilbert–Bernays–Löb derivability conditions. The operator that drives everything is reflection:

Its weakest single instance, taking φ = ⊥, is ¬Prov_T(⌜⊥⌝) — exactly Con(T). So R(T) contains Con(T), and Gödel's second theorem does the rest:

So we iterate. R(T), R²(T), R³(T), … is a strictly increasing chain, and at the limit we take the union R^ω(T) = ⋃ₙ Rⁿ(T), then continue: R^{ω+1}, …, R^{ω·2}, …. The climb runs through the ordinals. But here is the subtlety on which this entire study will turn, and which the casual phrase “iterate through the ordinals” hides.

Two strengths of reflection will matter. Local reflection, above, adds Prov_T(⌜φ⌝)→φ for each fixed φ. Uniform reflection RFN(T) adds the quantified ∀x (Prov_T(⌜φ(ẋ)⌝) → φ(x)) — soundness asserted once, for all numerical instances at a stroke. Uniform reflection is strictly stronger, and it is the variant whose iteration yields the clean ordinal arithmetic of the next sections. Local reflection suffices for the bare fact of no-top; uniform reflection is the one that measures. The distinction is small to state and decisive in consequence: it is the difference between knowing the ladder is endless and knowing exactly how its rungs are spaced.

How do we attach a number to a theory's strength? Not by counting its theorems, which are infinite and uncomputable, but by asking how far it can prove induction to reach. Transfinite induction along a well-ordering ≺ — TI(≺) — is the principle that if a property has no ≺-least counterexample then it holds everywhere. A theory that can prove TI(≺) “understands” the ordinal ≺ orders. The strength of the theory is how high those orderings go.

One honest caution, in the spirit of the parent corpus. There is not one proof-theoretic ordinal but a small family — the Π⁰₂-ordinal (tied to provably-total functions), the Π¹₁-ordinal (tied to provable well-foundedness), the consistency-strength ordinal. For tame, natural theories these coincide, and for PA they all equal ε₀; for artificial theories they can be prised apart. We mean throughout the value they share on the theories that occur in practice. The robustness of that shared value — that PA has a single canonical ordinal at all — is itself a deep empirical fact about natural theories, not a triviality.

what ε₀ is  ε₀ is the least ordinal closed under α ↦ ω^α — the limit of ω, ω^ω, ω^(ω^ω), …, the first solution of the equation ε = ω^ε. It is countable, far below the first uncountable ordinal, and entirely concrete. Its concreteness is the technical engine of everything here: every ordinal below ε₀ has a unique Cantor normal form

The ordinal is the spine of a whole hierarchy of strengths. A few landmarks, each the proof-theoretic ordinal of a natural theory:

Gödel-2 says PA cannot prove Con(PA) by means it contains. It does not say consistency is unprovable full stop. Gentzen (1936, 1938) proved Con(PA) outright — from a finitary base (PRA) plus a single transfinite principle: induction up to ε₀. That one added principle is exactly what PA lacks, so the proof respects Gödel while defeating the naïve reading of him. Here is its architecture, which is more illuminating than its conclusion.

step one — ordinals to proofs  Work in a sequent calculus for PA. To each derivation d assign an ordinal o(d) < ε₀ that measures its logical complexity — built from the nesting of cuts (uses of lemmas) and the depth of the induction inferences, combined by ordinal addition and exponentiation. A direct, cut-free proof gets a small ordinal; a proof leaning on deep lemmas and iterated induction gets a large one. The assignment is finitary and explicit.

step two — reduction lowers the ordinal  Now suppose, for contradiction, that PA proves ⊥ — a derivation d of the empty sequent. Gentzen gives reduction steps — local rewritings that eliminate the topmost essential cut, unfold an induction one layer — each producing a new derivation d' of the empty sequent with o(d') < o(d), strictly smaller. A proof of contradiction can always be made structurally simpler at the cost of nothing but its ordinal.

step three — well-foundedness closes it  Iterating reduction would produce o(d) > o(d') > o(d'') > ⋯, an infinite strictly descending sequence of ordinals below ε₀. But ε₀ is well-ordered: no such sequence exists. The supposed proof of ⊥ is therefore impossible. PA is consistent.

the modern form  Schütte recast the argument so the ordinals fall out by themselves. Replace PA's induction rule by the infinitary ω-rule — to conclude ∀x φ(x), take as premises all of φ(0), φ(1), φ(2), …. Proofs become well-founded infinite trees, each with an ordinal height. Every PA-proof embeds into an ω-proof of height < ε₀; cut-elimination on these infinite trees raises the height but keeps it below ε₀ for arithmetic conclusions; and a cut-free ω-proof of the empty sequent is impossible by a one-line induction on its height. The bound ε₀ emerges as the supremum of the heights — the same number, now visibly the ceiling of the cut-elimination process.

the same idea, made watchable  The whole engine — a strictly descending ordinal proves termination, and the ordinal is below ε₀ — can be run on a concrete sequence of ordinary integers. Write a number in hereditary base 2: in base 2, then rewrite the exponents in base 2, and so on. Now repeatedly (i) bump the base by one everywhere, and (ii) subtract one. The integers can balloon astronomically. Yet the sequence always reaches zero — and it does so for exactly Gentzen's reason.

Index a family of functions by the ordinals, each one iterating the last. This is the fast-growing hierarchy:

Each successor level applies the previous one a number of times equal to its own input — diagonal self-feeding, the recursion theorem's constructive face. The growth is staggering almost at once: f₃(3) is already a number with more than a hundred million digits, and f₃(4) leaves every magnitude with a physical meaning far behind. Try it — and watch how few rungs it takes to outrun every nameable number.

the theorem that fuses the two readings  A close cousin, the Hardy hierarchy H_α — H₀(n)=n, H_{α+1}(n)=H_α(n+1), H_λ(n)=H_{λ[n]}(n) — counts steps rather than iterating, and satisfies H_{ω^α} ≈ f_α: the two hierarchies are the same growth, indexed differently. With them the central identity becomes exact.

why the two readings coincide  This identity is not a numerical coincidence awaiting an explanation; it has a structural one. To prove a function total is to prove that a certain recursion halts, and a proof's own architecture — by the Curry–Howard correspondence, a proof is a program — is itself a recursion whose nesting is bounded by the ordinals the theory can certify well-founded. Strength and growth are therefore the same resource read off the same object: the ordinal that bounds how deeply a theory's proofs may recurse is exactly the ordinal that bounds how fast the functions those proofs certify may grow. Consistency, in this light, is a conservation law — it says precisely that the recursion never escapes the well-founded ordinals. That is why proving a function total just past the boundary, as Goodstein's rate f_{ε₀} demands, is equivalent to proving the very consistency the theory cannot reach: to certify the growth is to certify the well-foundedness, and they are one ordinal because proof and computation are one act.

And now Goodstein closes its own circle. Cichoń (1983) computed its rate: the number of steps a Goodstein sequence takes to terminate grows like H_{ε₀} — that is, like f_{ε₀}. So “every Goodstein sequence terminates” is, in function form, “f_{ε₀} is total” — one notch past the last rate PA can certify. The independence of §III and the growth boundary of §IV are not two facts. They are the same threshold, ε₀, named once as an ordinal and once as a speed.

If one round of reflection helps, why not iterate to the end? This was Turing's thesis (1939). His ordinal logics attach to each notation a for an ordinal a theory T_a, obtained by iterating consistency or reflection along the notation. The question is whether, climbing far enough, the tower becomes complete — whether every truth eventually gets proved at some height.

the startling half  Feferman (1962) proved it can. A progression by uniform reflection, pursued along a suitable path through the ordinal notations, proves every true Π⁰₁ sentence — and with more care, with transfinitely iterated reflection of higher type, every true arithmetical sentence whatsoever. On its face this is a completeness theorem for arithmetic, recovered at the transfinite limit of self-trust. The ladder, climbed forever, seems to reach the top after all.

So the bookkeeping is exact, and merciless. To collect the promised completeness you must first certify “the path I am climbing is well-founded.” That certification is a Π¹₁ statement, and no amount of arithmetic delivers it. You have not removed the incompleteness. You have relocated it — out of the object theory, where it was a single unprovable Π⁰₁ sentence, and up into the well-foundedness of the ladder itself, where it is a Π¹₁ one. This is the literal sense in which the diagonal recurs “one level up”: the deficit climbs a quantifier. The measure of the climb has become the obstacle to the climb.

The deepest response to a permanent limit is to make it productive. Take the limit's own instrument — the calibration of strength — and apply it not to artificial Gödel sentences but to the working theorems of analysis, algebra, and combinatorics. Ask, for each: exactly which axioms does this theorem need? This is reverse mathematics (Friedman, Simpson): prove the theorem from a weak base, then prove the axiom back from the theorem, pinning its strength precisely.

the big five  The base is RCA₀ — recursive comprehension, roughly “computable sets exist.” Above it, five subsystems of second-order arithmetic recur with astonishing regularity, and the bulk of ordinary mathematics turns out equivalent, over the base, to one of exactly these five:

the wall reaches ordinary mathematics  Nor is the boundary only artificial. Past the big five, Harvey Friedman's program exhibits natural theorems that demand still more: Kruskal's tree theorem is impredicative — it proves well-foundedness past Γ₀, to the small Veblen ordinal — so it outruns ATR₀; the Robertson–Seymour graph-minor theorem outruns even Π¹₁-CA₀; and Friedman's finite Boolean relation theory cannot be proved without large cardinals. These are statements a combinatorialist might prove on any given Tuesday, each pinned to an exact, and sometimes enormous, height on the ladder.