The Staircase

Gödel's second theorem says that a consistent, computably axiomatized theory T extending arithmetic cannot prove its own consistency: T ⊬ Con(T). The collection has met this many times as a limit. But attend to what it does not say. It does not say Con(T) is false — if T is consistent, Con(T) is true. It says only that this particular truth lies just past T's reach. And a truth just past reach is an invitation: adjoin it.

And now the same theorem applies again, one floor up. T₁ is itself consistent, computably axiomatized, and extends arithmetic — so by Gödel, T₁ ⊬ Con(T₁). The wall has reappeared, raised by exactly one storey. Adjoin Con(T₁) to get T₂; the wall reappears again. There is no theory at which this stops, because the obstacle is not a feature of any particular theory but of the form of self-reference itself — every system rich enough to describe its own provability is blind to its own consistency, and curing the blindness produces a new system with the same blindness, forever. The diagonal does not put up one wall. It puts up a wall on every floor, which is the same as building a staircase. The limit, looked at twice, is a step; and once there is one step there is no last one.

Iterate the step. From T build T₁, T₂, T₃, …, each the last plus its consistency. After all the finite stages, gather them: T_ω = ⋃ₙ Tₙ, the theory with every finite reflection as an axiom. It too is consistent and computably axiomatized, so Gödel applies and the climb resumes — T_{ω+1} = T_ω + Con(T_ω), and onward. To name the rungs past the limit you need the transfinite ordinals; this is the idea, arising the moment Gödel's theorem appeared, of iterating Gödelian extension along the ordinals, made precise by Turing's ordinal logics of 1939 and carried much further in Feferman's 1962 theory of transfinite progressions.

Two refinements turn the idea into a theory. First, consistency is only the mildest reflection. The general move is to add not just "T does not prove a contradiction" but "what T proves is true," in one of two strengths:

Second, and more delicate: the theory at stage α must be computably axiomatized, so the climb cannot be indexed by abstract ordinals but only by ordinal notations — concrete codes for ordinals drawn from Kleene's 𝒪, the recursive system of names for the constructive ordinals. A progression is therefore not a single tower but an assignment of theories to notations, from which a sequence is extracted by choosing a path through 𝒪. That distinction — ordinal versus notation, tower versus path — looks like bookkeeping. It is, in fact, where the deepest surprise of the subject will hide, and §V will spring it. For now, the climb is underway and the natural question is how to measure how far it has gone.

The measure is Gentzen's, from 1936, and it is the founding act of ordinal proof theory. Recall ε₀: the least ordinal closed under the tower of exponentials, ε₀ = sup{ω, ω^ω, ω^{ω^ω}, …}, equivalently the least α with ω^α = α. Gentzen showed that the consistency of arithmetic is provable by transfinite induction along ε₀ — and, exactly complementing it, that arithmetic itself can prove transfinite induction up to every α < ε₀ but not up to ε₀.

Two things in this deserve to be felt. The first is that the height is a number — an ordinal, the most transparent object mathematics has — so the vague notion "how strong is this theory" is made exact and comparable: stronger theories have larger ordinals, and the ordinal even pins down which functions the theory can prove total (for arithmetic, exactly those eventually dominated by the ε₀-level of the fast-growing hierarchy). The diagonal's wall has been replaced by a ruler.

The second is a correction the collection's honesty discipline insists on. It is often said that a theory's consistency can only be proved in a stronger theory. Gentzen's witnessing system shows this is false as stated. PRA + TI(ε₀) proves Con(PA), yet it does not contain PA — it lacks full induction for formulas with quantifiers. And PA does not contain it either, since PA cannot prove TI(ε₀). The two theories are incomparable: one buys reach into the transfinite at the cost of ordinary induction, the other the reverse. Consistency is not bought by sheer strength but by a different strength — more transfinite ladder, less of something else. The staircase is real, but you do not climb it by simply having more; you climb it by reaching further up the ordinals, and that is a specific currency.

Gödel's own unprovable sentence is a coded curiosity, true but artificial — a formula engineered to talk about its own provability. For decades it was possible to believe that incompleteness, while real, never touched ordinary mathematics: that every natural theorem a working mathematician might state was, if true, provable. The 1970s and 80s ended that belief. There are entirely natural finite statements — about sequences of integers, about colorings, about a combinatorial monster — that are true, that mathematicians would state without a thought of logic, and that arithmetic cannot prove. They are the staircase made concrete.

This is the payoff that makes the ordinal measure more than proof-theorists' bookkeeping. The height ε₀ is not a technical artifact of one consistency proof; it is a threshold that ordinary mathematics keeps bumping into from the other side. Goodstein, Hercules, and Paris–Harrington each encode, in innocent finite language, a demand for transfinite induction up to ε₀ — exactly the rung Gentzen identified as the one arithmetic cannot stand upon. The unprovability is not a curiosity grafted on by a logician; it is the staircase showing through the floor of number theory. A statement is unprovable in PA precisely when its content reaches above PA's ordinal, and these reach, demonstrably, to ε₀.

If each rung settles a little more, perhaps the whole climb settles everything — perhaps iterated reflection, pushed far enough up the ordinals, proves every true sentence of arithmetic, and incompleteness is merely the condition of standing on any one step rather than the whole staircase. Astonishingly, in one precise sense this is true. And, just as precisely, it is a trap.

This is where the distinction flagged in §II — ordinal versus notation, tower versus path — turns out to carry the whole weight. An ordinal is a pure quantity; a notation is a recursive program that names it, and there can be cleverness in the program that the ordinal itself does not contain. Feferman's completeness exploits exactly that slack: it chooses, for each truth to be proved, a path through the notations whose structure already encodes the truth, so that "reaching the rung" and "knowing the answer" become the same act. The staircase does reach the top — but only if you are allowed to decide how to count the steps after you already know where you are going. Feferman would later call such notation-paths, with characteristic precision, the dishonest ones.

So the honest verdict is the one that respects the spirit of Gödel's theorem rather than evading it. Measured by genuine strength — by which ordinals a theory can prove well-founded, by which consistency statements it settles — the ascent has no top: every theory stands on a definite rung, and there is always a higher one, and no canonical climb captures all truths. Completeness is reachable only by smuggling, and smuggling is not climbing. Incompleteness is not defeated by the staircase; it is organized by it — turned from a single wall into an endless, well-ordered, ordinal-measured ascent that no honest route ever finishes.