42.05.02 · mathematical-logic / proof-theory

Proof theory — cut-elimination, Gentzen, and ordinal analysis

shipped3 tiersLean: none

Anchor (Master): Takeuti 1987 Proof Theory 2e (North-Holland) Ch. 2 sec. 11-12 (Gentzen's consistency proof and the epsilon-nought analysis); Pohlers 2009 Proof Theory: The First Step into Impredicativity (Springer) (the Veblen hierarchy, the Feferman-Schutte ordinal Gamma-naught, the Bachmann-Howard ordinal, ordinal collapsing functions, the omega-rule and cut-elimination for infinitary derivations); Gentzen 1934/35 Untersuchungen uber das logische Schliessen and 1936 Die Widerspruchsfreiheit der reinen Zahlentheorie; Schutte 1977 Proof Theory (Springer); Godel 1958 Dialectica

Intuition Beginner

The companion unit 42.05.01 pending treated a proof as a two-sided line and showed you can erase the detour rule called the cut. This unit takes the next step. When a theory also carries an induction rule, the finite erasing procedure breaks down, and the question becomes how much "transfinite climbing" is needed to finish the job. The amount of climbing turns out to measure exactly how strong the theory is.

Picture a proof as a route on a map. A cut is a detour: you drive out to a distant helper lemma, use it, then drive back, and the helper never appears at your destination. Erasing all cuts straightens every route into one that passes only through towns already named in your destination. For pure logic the straightening always finishes in finitely many steps. For arithmetic it does not, but it finishes if you are allowed to count down a tower of infinities.

That tower is the point of this unit. Each rung is an infinite number bigger than the one below: $ω$ , then $ω$ to the power $ω$ , then that whole tower raised to the $ω$ again, and so on. The limit of all these rungs is called $ε_{0}$ . Gentzen's discovery is that Peano arithmetic is consistent exactly up to $ε_{0}$ : the theory can climb any single rung but cannot reach the top. The height a theory can climb is its proof-theoretic ordinal, and that height is its consistency strength.

So erasing detours does two jobs at once. In pure logic it gives a normal form that makes consistency immediate. In arithmetic it converts the consistency question into an ordinal-measuring question, and the ordinal reached — $ε_{0}$ , then the Feferman-Schütte ordinal $Γ_{0}$ , then the Bachmann-Howard ordinal for stronger theories — becomes a ruler comparing theories. That ruler is what this unit builds.

Visual Beginner

A sequent proof is a tree of two-sided lines, and the cut rule is the one move whose helper formula disappears. The picture below is the ordinal analogue: a tower of ever-larger infinite numbers, each rung earned by raising $ω$ to the power of the rung below.

   THE ORDINAL TOWER  (each rung = omega raised to the rung below it)

           omega ^ ( omega ^ ( omega ^ ( ... ) ) )     <-- epsilon_0
           :                                           (PA cannot reach here)
           ^
           |
     omega ^ omega ^ omega                  rung 4
     omega ^ omega                          rung 3
     omega ^ omega                          wait: rung 2 = omega^omega
     omega                                  rung 1

   PA proves transfinite induction up to any FINITE rung,
   but NOT up to epsilon_0 itself.

   epsilon_0 = |PA|   (the proof-theoretic ordinal of Peano Arithmetic)

Read the tower from the bottom: $ω$ , then $ω^{ω}$ , then $ω^{ω^{ω}}$ , and so on without end. The limit is $ε_{0}$ . Each rung is strictly bigger than the one below, and only at the limit does the operation "raise $ω$ to this power" settle — $ω^{ε_{0}} = ε_{0}$ .

theory	proof-theoretic ordinal	what climbing that high buys
primitive recursive arithmetic (PRA)	$ω^{ω}$	finitary consistency of PRA
Peano arithmetic (PA)	$ε_{0}$	consistency of first-order arithmetic
$ATR_{0}$ (predicative analysis)	$Γ_{0}$	the Feferman-Schütte predicative limit
$Π_{1}^{1} - CA_{0}$	Bachmann-Howard ordinal	impredicative analysis

Higher ordinal, stronger theory: the height a theory can climb is its consistency strength, made into a single comparable number.

Worked example Beginner

Build $ε_{0}$ from below. Start with $ω$ , the first infinite number. Raise $ω$ to its own power: $ω^{ω}$ . Raise again: $ω^{ω^{ω}}$ . Each step stacks one more $ω$ on top of the tower. The rungs are $ω$ , then $ω^{ω}$ , then $ω^{ω^{ω}}$ , then $ω^{ω^{ω^{ω}}}$ , and so on.

The limit of this endless tower is $ε_{0}$ . Its defining trick is a fixed-point property: $ε_{0}$ is the first number $α$ with $ω^{α} = α$ . Check the pattern by hand. For $ω$ we have $ω^{ω}$ far bigger than $ω$ . For $ω^{ω}$ we have $ω^{ω^{ω}}$ far bigger than $ω^{ω}$ . Each rung sits strictly below the next. Only at the limit does the power settle: $ω^{ε_{0}} = ε_{0}$ .

Now the punch line. Gentzen proved that Peano arithmetic, PA, can prove transfinite induction up to every rung below $ε_{0}$ — $ω$ , $ω^{ω}$ , $ω^{ω^{ω}}$ , each one — but cannot prove transfinite induction up to $ε_{0}$ itself. The height PA can climb is exactly $ε_{0}$ . So $ε_{0}$ is called the proof-theoretic ordinal of PA, written $∣ P A ∣ = ε_{0}$ . A stronger theory climbs higher.

What this tells us: the consistency of PA is equivalent, over a weak base, to the well-foundedness of $ε_{0}$ — the claim that no endless descending chain of ordinals lives below $ε_{0}$ . PA cannot see that well-foundedness itself (Gödel's second theorem 42.01.09 pending), but a metatheory that grants induction up to $ε_{0}$ can, and that single grant is exactly what Gentzen's consistency proof consumes.

Check your understanding Beginner

Formal definition Intermediate+

Recall from 42.05.01 pending the sequent calculus $LK$ : sequents $Γ \Rightarrow Δ$ , initial sequents $A \Rightarrow A$ , the structural rules (weakening, contraction, exchange), the left and right logical rules with their eigenvariable conditions, and the cut rule. We do not redevelop the calculus here; this unit's object is the ordinal layer that the Hauptsatz leaves untouched once an induction rule is adjoined. Fix the language of first-order arithmetic with symbols $0, S, +, \times, =$ and the induction schema, giving the theory $PA$ .

Cantor normal form (CNF). Every nonzero ordinal $α < ε_{0}$ admits a unique expression

α = ω^{β_{1}} \cdot c_{1} + ω^{β_{2}} \cdot c_{2} + \dots + ω^{β_{n}} \cdot c_{n}, α > β_{1} \geq β_{2} \geq \dots \geq β_{n}, 0 < c_{i} < ω,

where each exponent $β_{i}$ is itself in CNF ^{[Pohlers Ch. 3-4]}. Iterating the exponent-descent terminates precisely because $α < ε_{0} = sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots}$ . CNF makes the ordinals below $ε_{0}$ a primitive-recursive notation system: there is an algorithm deciding, for any two notations, which ordinal is smaller, and so transfinite induction up to $α < ε_{0}$ reduces to induction over a computable well-order on finite strings.

Definition (proof-theoretic ordinal). For a sound, recursively axiomatised theory $T \supseteq PRA$ , the proof-theoretic ordinal $∥ T ∥$ (also written $∣ T ∣$ ) is the following coincident countable ordinal:

the supremum $sup {otp (≺) :≺ primitive-recursive well-ordering with T ⊢ TI (≺)}$ ;
equivalently, $sup {α : F_{α} is provably total in T}$ in the fast-growing hierarchy $(F_{α})$ ;
equivalently, the least $α$ along the canonical notation such that $T ⊬ TI (α)$ .

The equivalence of the first and third is Gentzen-style (a theory proves $TI$ up to exactly one bound); that of the first and second is the Wainer–Kreisel characterization of provable totality ^[Pohlers]. Two theories with the same proof-theoretic ordinal have the same consistency strength.

Veblen hierarchy. Put $φ_{0} (β) = ω^{β}$ , and define $φ_{α + 1}$ to enumerate in increasing order the common fixed points of ${φ_{γ} : γ \leq α}$ ; at limits set $φ_{λ} (β) = sup_{γ < λ} φ_{γ} (β)$ . Each $φ_{α}$ is a continuous increasing (normal) function. The Feferman-Schütte ordinal $Γ_{0}$ is the least $α$ with $φ_{α} (0) = α$ ; it bounds every predicatively definable ordinal. The Bachmann-Howard ordinal sits above $Γ_{0}$ and is reached only by impredicative constructions.

Fast-growing hierarchy. Set $F_{0} (n) = n + 1$ , $F_{α + 1} (n) = F_{α}^{n + 1} (n)$ (the $(n + 1)$ -fold self-composition), and $F_{λ} (n) = F_{λ [n]} (n)$ for a fixed fundamental sequence $λ [0] < λ [1] < \dots$ with $sup_{n} λ [n] = λ$ . Then $F_{α}$ dominates exactly the functions that a theory of proof-theoretic ordinal $> α$ can prove total: $F_{ε_{0}}$ dominates the $PA$ -provably total functions, $F_{Γ_{0}}$ those provably total in predicative analysis.

Counterexamples to common slips Intermediate+

" $ε_{0}$ is the largest ordinal PA can handle." PA can name and reason about many ordinals larger than $ε_{0}$ . What fails at $ε_{0}$ is specifically transfinite induction: PA proves $TI (α)$ for each $α < ε_{0}$ but not at $ε_{0}$ . The proof-theoretic ordinal measures induction strength, not expressive reach.
"Ordinal analysis proves the theory true." It does not. Ordinal analysis delivers relative consistency (the theory is consistent if a weak base plus $TI (∥ T ∥)$ is) and a bound on the provably total functions. It is a calibration, not a soundness proof; a theory of ordinal $ε_{0}$ could still be unsound in a language it does not control.
"A larger proof-theoretic ordinal means strictly more theorems in the same language." The ordinal compares consistency strength and provable totality, which is coarser than raw theorem-set inclusion. Two theories can be incomparable in theorem set yet have ordinals that line up, because the ordinal measures the transfinite-induction resources, one axis among several.

Key theorem with proof Intermediate+

The load-bearing result of pure structural proof theory is the Hauptsatz; the load-bearing result of this unit is the ordinal-analysis theorem that calibrates $PA$ at $ε_{0}$ , which is what the Hauptsatz becomes when an induction rule blocks outright cut-elimination.

Theorem (Cut-elimination, Gentzen's Hauptsatz — stated). Every $LK$ -derivation of a sequent $S$ transforms into a cut-free $LK$ -derivation of $S$ ; likewise for $LJ$ . ^{[Gentzen 1934-35]}

Proof sketch. Remove a topmost cut (more precisely a mix, which cuts all copies of the cut formula at once) by a double induction on the grade $g$ of the cut formula $A$ (its logical complexity) and on the rank $r$ (the combined heights of the chains of $A$ -containing sequents above each premise). The non-principal case, where $A$ was carried passively by the rule above a premise, permutes the mix upward past that rule: $r$ drops, $g$ fixed, inner hypothesis applies. The principal case, where $A$ was just introduced on both sides, replaces the mix on $A$ by mixes on its immediate subformulas: $g$ drops, outer hypothesis applies. The $\forall$ -case substitutes the eigenvariable by the witness term throughout, which is legitimate precisely because the eigenvariable condition kept that variable out of the side formulas. The full case analysis, with the mix reduction and the base cases against initial sequents and weakenings, is Proposition 1 of 42.05.01 pending. $□$

The immediate corollary is the subformula property: every formula occurring in a cut-free derivation of $S$ is a subformula of a formula of $S$ (each non-cut rule has its premise-formulas among the subformulas of its conclusion-formulas), from which the consistency of pure $LK$ follows as in 42.05.01 pending. The present unit's concern is what survives of this picture when the induction rule is adjoined.

Theorem (Gentzen's ordinal analysis of $PA$ ). $∣ PA ∣ = ε_{0}$ : that is, $PA ⊢ TI (α)$ for every $α < ε_{0}$ and $PA ⊬ TI (ε_{0})$ . Consequently $Con (PA)$ is equivalent over $PRA$ to $TI (ε_{0})$ . ^{[Gentzen 1936]} ^{[Takeuti Ch. 2]}

Proof. Two halves.

Lower bound ( $PA ⊢ TI (α)$ for each $α < ε_{0}$ ). Induct on the CNF of $α$ . For a leading term $ω^{β} \cdot c$ with $β < α$ , a primitive-recursive descent through $ω^{β}$ decomposes (by the recursive CNF of $β$ ) into finitely many descents through strictly smaller ordinals, each dispatched by the inner induction hypothesis. The finite coefficient $c < ω$ is absorbed by ordinary $PA$ -induction. Because the CNF exponent-descent terminates strictly below $ε_{0}$ , every $α < ε_{0}$ is dispatched inside $PA$ , giving $PA ⊢ TI (α)$ .

Upper bound ( $PA ⊬ TI (ε_{0})$ ). Assign to each $PA$ -derivation $D$ an ordinal $o (D) < ε_{0}$ in CNF, summing $ω$ -powers graded by cut-formula complexity and the depth of induction instances. Exhibit an effective reduction $D \mapsto D^{'}$ acting on any derivation of the empty sequent $\Rightarrow$ , with $D^{'}$ again ending in $\Rightarrow$ and $o (D^{'}) < o (D)$ : each maximal cut is pushed upward or eliminated (its grade drops), and each induction instance is unfolded one step (raising the local $ω$ -power but staying below $ε_{0}$ ).

If a derivation of $\Rightarrow$ existed, iterating the reduction would produce an infinite strictly descending chain $o (D) > o (D^{'}) > o (D^{''}) > \dots$ below $ε_{0}$ , contradicting $TI (ε_{0})$ . So no derivation of $\Rightarrow$ exists: $PA$ is consistent. Now suppose for contradiction that $PA ⊢ TI (ε_{0})$ . Then the reduction argument above — which is primitive-recursive except for the single call to $TI (ε_{0})$ — could be formalized inside $PA$ , yielding $PA ⊢ Con (PA)$ , against Gödel's second incompleteness theorem 42.01.09 pending. Hence $PA ⊬ TI (ε_{0})$ , and $∣ PA ∣ = ε_{0}$ . $□$

Bridge. The ordinal $∣ PA ∣ = ε_{0}$ is the foundational reason cut-elimination survives the move from pure logic to arithmetic: the grade-and-rank induction of the Hauptsatz, finite and bounded in 42.05.01 pending, generalises here to a transfinite descent that consumes exactly the one principle — $TI (ε_{0})$ — lying beyond $PA$ 's reach. This is exactly the calibrated face of Gödel's second theorem 42.01.09 pending: the missing consistency strength is not a vague gap but a single named ordinal. It builds toward the hierarchy below — $Γ_{0}$ for predicative theories, the Bachmann-Howard ordinal for impredicative $Π_{1}^{1}$ -analysis — and it appears again in the fast-growing hierarchy, where $F_{ε_{0}}$ dominates exactly the $PA$ -provably total functions, turning ordinal strength into growth rate and into concrete independence results such as Goodstein's theorem. The central insight is that a theory's strength, its consistency, and the functions it proves total are three readings of one ordinal, and the bridge from a syntactic cut-elimination procedure to a semantic measure of strength is the proof-theoretic ordinal itself.

Exercises Intermediate+

Exercise 4 (medium, symbolic).

A Goodstein sequence writes its current number in hereditary base $b$ (every exponent also written in base $b$ ), changes every $b$ to $b + 1$ , then subtracts $1$ . Translate the starting value $4$ to an ordinal by writing it in hereditary base $2$ and replacing every $2$ by $ω$ . Then show that after one Goodstein step the resulting natural number has grown while the associated ordinal has shrunk.

Hint

$4 = 2^{2}$ is already hereditary base $2$ . Replace the base $2$ by $ω$ to get the ordinal. For the step, change base to $3$ (giving $3^{3} = 27$ ), subtract $1$ to get $26$ , rewrite $26$ in hereditary base $3$ , replace $3$ by $ω$ , and compare ordinals.

Answer

Hereditary base $2$ : $4 = 2^{2}$ . Replacing $2$ by $ω$ gives the ordinal $ω^{ω} < ε_{0}$ . After one step: change base to $3$ , obtaining $3^{3} = 27$ ; subtract $1$ , giving $26 = 2 \cdot 3^{2} + 2 \cdot 3 + 2$ in hereditary base $3$ . Replace $3$ by $ω$ : the ordinal is $ω^{2} \cdot 2 + ω \cdot 2 + 2$ , which is *strictly smaller* than $ω^{ω}$ (lower leading exponent), even though $26 > 4$ . This descent of the ordinal shadow at every step, while the number itself first balloons, is why transfinite induction up to $ε_{0}$ proves every Goodstein sequence terminates, and why $PA$ — which lacks $TI (ε_{0})$ — cannot prove it. Rubric: full credit for the ordinal $ω^{ω}$ , the correct expansion of $26$ , and the strict decrease.

Exercise 5 (medium, symbolic).

Prove, inside $PA$ , that $TI (ω^{k})$ holds for each fixed standard natural number $k$ , by reducing transfinite induction up to $ω^{k}$ to $k$ -fold iterated ordinary induction.

Hint

An $ω^{k}$ -indexed descending chain projects, coordinate by coordinate through the CNF $ω^{k - 1} \cdot n_{k - 1} + \dots$ , to finitely many $ω^{k - 1}$ -indexed descents. Use induction on $k$ .

Answer

Base $k = 1$ : $TI (ω)$ is exactly ordinary induction on $N$ , available in $PA$ . Inductive step: assume $PA ⊢ TI (ω^{k})$ and prove $TI (ω^{k + 1})$ . A primitive-recursive well-ordering of type $ω^{k + 1}$ has each element of CNF $ω^{k} \cdot n + γ$ with $γ < ω^{k}$ . Any descending chain through $ω^{k + 1}$ has its leading coefficients $n$ descending finitely (by ordinary induction, the $k = 1$ case), and within each fixed leading block, the tail $γ$ descends through $ω^{k}$ , dispatched by the inductive hypothesis $TI (ω^{k})$ . Composing the two inductions inside $PA$ yields $PA ⊢ TI (ω^{k + 1})$ . Iterating reaches every finite-height tower $ω^{k}$ , but never the limit $ω^{ω}$ , let alone $ε_{0}$ . Rubric: full credit for the induction on $k$ and the leading-coefficient-plus-tail decomposition.

Exercise 6 (medium, symbolic).

Rank the fast-growing functions $F_{2}, F_{3}, F_{ω}, F_{ω^{ω}}, F_{ε_{0}}$ by eventual domination (which eventually exceeds which), and identify which of them dominates exactly the $PA$ -provably total functions.

Hint

The hierarchy is strictly increasing in $α$ : if $α < β$ then $F_{β}$ eventually dominates $F_{α}$ . Recall the proof-theoretic ordinal of $PA$ .

Answer

Since $α \mapsto F_{α}$ is increasing under eventual domination,

F_{2} < F_{3} < F_{ω} < F_{ω^{ω}} < F_{ε_{0}}

(each eventually dominated by the next). The Wainer–Kreisel characterization gives that the $PA$ -provably total recursive functions are exactly those dominated by some $F_{α}$ with $α < ε_{0}$ , equivalently by $F_{ε_{0}}$ overall. Thus $F_{ε_{0}}$ is the function that pins the $PA$ -provably total functions; $F_{Γ_{0}}$ plays the same role for predicative analysis. Rubric: full credit for the strict chain and the identification of $F_{ε_{0}}$ with $PA$ 's provable totality bound.

Exercise 7 (hard, symbolic).

Prove that $Con (PA)$ and $TI (ε_{0})$ are equivalent over the weak base theory $PRA$ : each is provable from the other inside $PRA$ .

Hint

One direction is Gentzen's reduction argument relativized to $PRA$ . The other uses the fact that the ordinal notation system below $ε_{0}$ and a proof of its well-foundedness are formalizable in any theory containing enough arithmetic to discuss proofs.

Answer

$TI (ε_{0}) \Rightarrow Con (PA)$ in $PRA$ : Gentzen's reduction $D \mapsto D^{'}$ on a purported derivation $D$ of the empty sequent is primitive-recursive and strictly lowers the ordinal $o (D) < ε_{0}$ . Formalized in $PRA$ , the existence of such a $D$ yields a primitive-recursive infinite descending sequence below $ε_{0}$ ; $TI (ε_{0})$ rules this out, so $PRA + TI (ε_{0}) ⊢ Con (PA)$ .

$Con (PA) \Rightarrow TI (ε_{0})$ in $PRA$ : if $PA$ proved the (primitive-recursive) well-foundedness of every proper initial segment below any $α < ε_{0}$ — which it does, by Exercise 5 and its transfinite analogue — and if $TI (ε_{0})$ failed, one could build inside $PA$ a primitive-recursive descending chain certifying failure; combined with the internal proof that all initial segments are well-founded this would yield an internal contradiction, and since the construction is finitary, $PA$ would prove $\neg TI (ε_{0}) \to \neg Con (PA)$ . Contrapositively $Con (PA)$ gives $TI (ε_{0})$ over $PRA$ . Rubric: full credit for both directions, the primitive-recursive reduction in the first, and the contrapositive linking internal contradiction to consistency in the second.

Exercise 8 (hard, symbolic).

In the infinitary semi-formal calculus with the $ω$ -rule — from $φ (0), φ (1), φ (2), \dots$ infer $\forall x φ (x)$ — every true $Π_{1}^{0}$ sentence has a countably infinite cut-free derivation. Explain why cut-elimination for this infinitary calculus sends a derivation of height $α$ to a cut-free derivation of height bounded by an $ω$ -tower in $α$ , and why this is the mechanism that produces the $ε_{0}$ bound for $PA$ .

Hint

Eliminating a single cut of grade $g$ at height $h$ replaces it by cuts of lower grade repeated up to $ω$ times; the height thus gets raised by one $ω$ -exponent per grade unit. Iterate over all grades and heights.

Answer

In the $ω$ -rule calculus a derivation is a (possibly countably infinite) tree whose height is itself an ordinal. Eliminating a cut whose formula has grade $g$ and whose subderivations rise to height $h$ replaces it by countably many cuts of grade $g - 1$ (one $ω$ -sequence of reductions), so the new derivation has height at most $ω^{h}$ -ish — formally, the height gets raised by one application of $α \mapsto ω^{α}$ . Eliminating cuts of grade $g$ , then $g - 1$ , and so on down to grade $0$ , composes this raising $g$ times, yielding a cut-free derivation whose height is an $ω$ -tower of depth $g$ in the original height. Embedding $PA$ into the infinitary calculus (induction unfolds into an $ω$ -branching $ω$ -rule) gives finite $PA$ -proofs infinitary shadows of some bounded height $α$ ; eliminating cuts raises the height below the least fixed point of $α \mapsto ω^{α}$ , namely $ε_{0}$ . Hence a $PA$ -proof of a contradiction would yield a cut-free infinitary derivation of the empty sequent of height $< ε_{0}$ , impossible by the subformula property at each ordinal level. The bound $ε_{0}$ is thus the cost, in transfinite height, of eliminating cuts from $PA$ . Rubric: full credit for the grade-by-grade $ω$ -exponent raising, the embedding of induction into the $ω$ -rule, and the identification of $ε_{0}$ as the resulting fixed point.

Lean formalization Intermediate+

lean_status: none. The formalization gap is substantive and twofold. First, Mathlib carries no inductive type of sequent-calculus derivations to which an ordinal measure could be attached: there is no LK.Derivation Γ Δ, no cut rule as a constructor, and therefore no cut_eliminate : Derivation → CutFreeDerivation to compose with an ordinal assignment. Second, even the ordinal-theoretic substrate — a Veblen function veblen : Ordinal → Ordinal → Ordinal, the Feferman-Schütte ordinal Gamma_0 as the least fixed point of veblen · 0, the Bachmann-Howard ordinal via collapsing on an uncountable Ω, and a fast-growing hierarchy F : Ordinal → ℕ → ℕ tied to provable totality — is absent. A Mathlib contribution roadmap would start with a CNF normal-form API below epsilon_0 (recoverable from existing Ordinal.opow), then a verified primitive-recursive ordinal-comparison, then the Veblen hierarchy; the proof-theoretic-ordinal theorem |PA| = ε₀ is a distant target that depends on a sequent-calculus formalization Mathlib does not yet host. Until then, this unit's correctness rests on the human reviewer documented in the unit metadata.

Advanced results Master

Ordinal analysis past $PA$ climbs through three calibrated regions — the predicative ( $\leq Γ_{0}$ ), the impredicative countable (Bachmann-Howard and beyond), and the infinitary engine (the $ω$ -rule) — and each region has a complementary computability reading via the fast-growing hierarchy, plus Gödel's Dialectica as an alternative consistency route.

Theorem 1 (predicative limit — Feferman-Schütte). The Feferman-Schütte ordinal $Γ_{0} = min {α : φ_{α} (0) = α}$ is the supremum of every ordinal that can be predicatively defined, in the precise sense of autonomous ramified progressions (Feferman 1964, Schütte 1965 independently) ^[Pohlers]. It calibrates the proof-theoretic ordinal of the predicative systems of reverse mathematics: $∣ ATR_{0} ∣ = Γ_{0}$ . The autonomy theorem says a predicative mathematician, starting from $PRA$ and repeatedly adjoining well-orderings whose well-foundedness has already been established, can reach every ordinal below $Γ_{0}$ and none at or above; $Γ_{0}$ is thus the exact predicative ceiling.

Theorem 2 (impredicative analysis and collapsing). The system $Π_{1}^{1} - CA_{0}$ of impredicative second-order arithmetic has proof-theoretic ordinal the Bachmann-Howard ordinal, lying strictly above $Γ_{0}$ ^[Pohlers]. The ordinal-analytic engine here is ordinal collapsing: one works in a notation system built on an uncountable ordinal $Ω$ (taken to name sets unavailable predicatively), performs cut-elimination in that enlarged system where the uncountable height supplies enough room, and then applies a collapsing function that maps the resulting notations back below $Ω$ , delivering a countable ordinal — the Bachmann-Howard ordinal — that records the impredicative strength. This local predicativity (Pohlers) is the modern form of Gentzen's reduction: the derivation is reduced transfinitely in an enlarged ordinal world, then collapsed to a countable measure.

Theorem 3 (infinitary proof theory, the $ω$ -rule — Schütte). Adjoin to a sequent calculus the infinitary $ω$ -rule — from the countably many premises $Γ \Rightarrow Δ, φ (n)$ for every $n \in N$ , infer $Γ \Rightarrow Δ, \forall x φ (x)$ ^[Pohlers]. Derivations become countably infinite trees of some ordinal height. Cut-elimination for this semi-formal calculus terminates, raising the derivation height by one $ω$ -exponent per eliminated cut grade; embedding $PA$ into it by unfolding induction into $ω$ -branching yields the bound $∣ PA ∣ = ε_{0}$ as the transfinite cost of cut-elimination, and analogously produces $Γ_{0}$ and the Bachmann-Howard ordinal for stronger theories. The infinitary calculus is the natural home of ordinal analysis: the ordinal a theory reaches is exactly the height its cut-elimination costs.

Theorem 4 (provable totality and independence). The Wainer–Kreisel characterization identifies the $PA$ -provably total recursive functions with those dominated by some $F_{α}$ , $α < ε_{0}$ , in the fast-growing hierarchy ^[Pohlers]. Consequently the termination of the Goodstein sequences, of Kirby-Paris's Hydra game, and the strengthened finite Ramsey theorem of Paris-Harrington are each true $Π_{2}^{0}$ (or $Π_{1}^{1}$ ) statements unprovable in $PA$ : each encodes, at finite level, a descent that requires $TI (ε_{0})$ to certify. The Goodstein theorem is particularly direct — Exercise 4 exhibits the ordinal shadow of each step — while Paris-Harrington reaches beyond $ε_{0}$ into mild fragments of $Π_{1}^{1}$ -comprehension.

Theorem 5 (Gödel's Dialectica — an alternative route). Gödel's 1958 Dialectica interpretation interprets $PA$ into the quantifier-free theory $T$ of primitive-recursive functionals of finite type (System $T$ ), reducing $Con (PA)$ to the termination of $T$ 's reduction sequences, proved by Tait-style computability ^{[Godel 1958]}. This reaches the same consistency strength as Gentzen's $ε_{0}$ proof without ordinals, and Spector's 1962 extension via bar-recursion reaches $Π_{1}^{1}$ -analysis — the same level Bachmann-Howard later pinned by ordinals. The Dialectica route and the Gentzen route are thus two complementary consistency proofs of identical strength: one syntactic-ordinal, one computational-functional.

Synthesis. Ordinal analysis is the central insight that a theory's consistency strength is a single ordinal, and putting these together the whole ladder — $∣ PRA ∣ = ω^{ω}$ , $∣ PA ∣ = ε_{0}$ , $∣ ATR_{0} ∣ = Γ_{0}$ , $∣ Π_{1}^{1} - CA_{0} ∣ =$ Bachmann-Howard — is the foundational reason proof theory can compare theories that raw theorem-counting cannot distinguish. The Hauptsatz of 42.05.01 pending is dual to the infinitary $ω$ -rule cut-elimination that produces these bounds: one removes detours from finite proofs, the other from countably infinite ones, and the ordinal a theory reaches is exactly what its detour-elimination costs in transfinite height. This generalises from arithmetic into analysis via the Veblen hierarchy and ordinal collapsing, and the bridge is the fast-growing hierarchy, where $ε_{0}$ , $Γ_{0}$ , and the Bachmann-Howard ordinal each translate into a growth rate pinning which functions the theory proves total and which true statements (Goodstein, the Hydra, Paris-Harrington) it cannot reach. Ordinal analysis thus builds toward a single calibrated picture in which consistency, provable totality, and independence are three faces of one ordinal measure — the constructive complement to Gödel's abstract incompleteness, and exactly bounded by it.

Full proof set Master

Proposition 1 ( $ε_{0}$ is the least fixed point of $α \mapsto ω^{α}$ ). $ε_{0} = sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots}$ satisfies $ω^{ε_{0}} = ε_{0}$ , and no smaller ordinal does.

Proof. Let $α_{0} = ω$ and $α_{n + 1} = ω^{α_{n}}$ , so $ε_{0} = sup_{n} α_{n}$ . Continuity of $β \mapsto ω^{β}$ (it carries suprema of increasing sequences to suprema) gives $ω^{ε_{0}} = ω^{s u p_{n} α_{n}} = sup_{n} ω^{α_{n}} = sup_{n} α_{n + 1} = sup_{n} α_{n} = ε_{0}$ , the last equality because $(α_{n + 1})_{n}$ is the sequence $(α_{n})_{n}$ shifted by one index. For minimality, let $δ < ε_{0}$ . Then $δ < α_{N}$ for some $N$ , so $ω^{δ} \leq ω^{α_{N}} = α_{N + 1} < ε_{0}$ ; but also $ω^{δ} > δ$ for every countable $δ$ that is not already an $ε$ -number (and $δ < ε_{0}$ is not). Hence $ω^{δ} > δ$ , so $δ$ is not a fixed point. Therefore $ε_{0}$ is the least fixed point. $□$

Proposition 2 ( $PA ⊢ TI (α)$ for every $α < ε_{0}$ ). For each ordinal $α < ε_{0}$ with its primitive-recursive CNF ordering, Peano arithmetic proves the transfinite-induction schema $TI (α)$ .

Proof. Induct on the CNF of $α$ . If $α = 0$ , $TI (0)$ is vacuous. If $α = ω^{β_{m}} \cdot c_{m} + \dots + ω^{β_{1}} \cdot c_{1}$ (CNF, leading exponent $β_{m}$ with $β_{m} < α$ ), suppose by the inner induction that $PA ⊢ TI (γ)$ for every $γ < α$ , in particular $PA ⊢ TI (β_{m})$ and $PA ⊢ TI (ω^{β_{m}})$ . A primitive-recursive descent through $α$ projects, by stripping the leading $ω^{β_{m}} \cdot c_{m}$ summand, to a finite descent of the natural-number coefficient $c_{m}$ (handled by ordinary $PA$ -induction) together with descents through the tail below $ω^{β_{m}}$ (handled by $TI (ω^{β_{m}})$ , itself reducible to $TI (β_{m})$ by the same argument iterated on $β_{m}$ 's CNF). Composing these inductions is internal to $PA$ , so $PA ⊢ TI (α)$ . The CNF exponent-descent terminates strictly below $ε_{0}$ , so the induction is well-founded and reaches every $α < ε_{0}$ . $□$

Proposition 3 (Goodstein termination is equivalent to $TI (ε_{0})$ over $PRA$ ). The statement "every Goodstein sequence terminates" is provable in $PRA + TI (ε_{0})$ and, conversely, implies $TI (ε_{0})$ over $PRA$ ; hence it is unprovable in $PA$ .

Proof. Associate to a natural number $n$ written in hereditary base $b$ the ordinal $ord_{b} (n) < ε_{0}$ obtained by replacing the base $b$ everywhere by $ω$ ; the result is in CNF below $ε_{0}$ because the hereditary exponent-depth is finite. At a Goodstein step, $n$ in hereditary base $b$ is rewritten in base $b + 1$ then decreased by $1$ . The replacement $b \mapsto b + 1$ does not change $ord_{b} (n) = ord_{b + 1} (n)$ (both map to the same $ω$ -expression). Subtracting $1$ from the base- $(b + 1)$ hereditary form strictly decreases the ordinal: in CNF the unit coefficient at the bottom drops, and if it was already zero the descent cascades to a higher exponent at strictly smaller leading term — a strict ordinal decrease $ord_{b + 1} (n - 1) < ord_{b + 1} (n) = ord_{b} (n)$ . Thus each step strictly lowers the ordinal shadow, giving a primitive-recursive descending chain below $ε_{0}$ . By $TI (ε_{0})$ no such infinite chain exists, so the sequence terminates: $PRA + TI (ε_{0}) ⊢ Goodstein$ .

For the converse, Kirby and Paris (1982) showed the Goodstein theorem is not provable in $PA$ by an indicator-chain argument, and that over $PRA$ the Goodstein theorem implies $TI (ε_{0})$ (the descent certified by any putative failure of $TI (ε_{0})$ can be encoded as a Goodstein sequence). Since $PA ⊬ TI (ε_{0})$ (Prop. below), $PA ⊬ Goodstein$ . $□$

Corollary ( $∣ PA ∣ = ε_{0}$ , restated). $PA ⊢ TI (α)$ for every $α < ε_{0}$ (Proposition 2) and $PA ⊬ TI (ε_{0})$ ; hence $∣ PA ∣ = ε_{0}$ .

Proof of the upper bound. If $PA ⊢ TI (ε_{0})$ , Gentzen's primitive-recursive reduction $D \mapsto D^{'}$ (formalizable in $PA$ save for the single call to $TI (ε_{0})$ , now assumed) would internalize to $PA ⊢ Con (PA)$ , contradicting Gödel's second incompleteness theorem 42.01.09 pending. Hence $PA ⊬ TI (ε_{0})$ . Combined with Proposition 2, the supremum of provable transfinite inductions is exactly $ε_{0}$ . $□$

Connections Master

The sibling unit 42.05.01 pending is the structural foundation this unit extends: it carries the full definition of the sequent calculi $LK$ and $LJ$ , the complete grade-and-rank proof of the Hauptsatz, and the subformula property with its pure-logic corollaries (consistency, the midsequent/Herbrand theorem, the LJ disjunction and existence properties, Craig interpolation). This unit takes the Hauptsatz as stated and adds the transfinite layer — ordinal assignment, $ε_{0}$ , the Veblen hierarchy — that the induction rule forces into view. Read the two as a single arc: 42.05.01 pending is the finite cut-elimination theorem, this unit is its transfinite continuation.

The incompleteness theorems 42.01.09 pending supply the exact ceiling that ordinal analysis respects. Gödel's second theorem says $PA ⊬ Con (PA)$ , and Gentzen's analysis locates the missing strength as the single principle $TI (ε_{0})$ , equivalent to $Con (PA)$ over $PRA$ . Every ordinal-analytic bound in this unit is a calibrated refinement of that abstract incompleteness result, turning "PA cannot prove its own consistency" into "PA can climb to exactly $ε_{0}$ and no higher."

Ordinals, transfinite induction, and recursion 42.03.02 provide the raw material: the ordinal $ε_{0} = sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots}$ as the least fixed point of $α \mapsto ω^{α}$ , the Cantor normal form that makes ordinals below $ε_{0}$ a primitive-recursive notation system, and the well-foundedness that forbids infinite descent. The Veblen hierarchy and the Bachmann-Howard ordinal studied here are direct continuations of the ordinal-arithmetic apparatus of that unit into the impredicative.

Computability and the halting problem 42.04.02 meet proof theory at the fast-growing hierarchy: the $PA$ -provably total recursive functions are exactly those dominated by some $F_{α}$ with $α < ε_{0}$ , so the proof-theoretic ordinal is also a recursion-theoretic boundary, separating the total functions $PA$ can certify from those (like $F_{ε_{0}}$ itself) it cannot. The independence of Goodstein's theorem and Paris-Harrington 42.04.08 sits on the same boundary, each a concrete true statement stranding just past what $PA$ reaches.

The deductive calculus and soundness 42.01.05 pending is the Hilbert-style system the sequent calculus reorganizes: modus ponens becomes the cut rule, generalization becomes the eigenvariable condition, and the semantic soundness induction of that unit ( $⊢$ below $⊨$ ) is the semantic twin of the structural cut-elimination induction of 42.05.01 pending and the transfinite ordinal-reduction induction of this unit. The three inductions — semantic, structural-finite, structural-transfinite — are three faces of the same control over what a theory can prove.

Historical & philosophical context Master

David Hilbert's programme proposed to secure all of mathematics by finitary consistency proofs: formalize each branch as an axiomatic system, then prove, by utterly finite combinatorial means, that the system cannot derive a contradiction. Kurt Gödel's 1931 incompleteness theorems ^{[Godel 1931]} showed no sufficiently strong, effectively axiomatized theory can prove its own consistency, blocking the programme in its naive form. Gerhard Gentzen, a student of Paul Bernays and Hermann Weyl, responded by isolating exactly which non-finitary principle a constructive consistency proof of arithmetic requires.

Gentzen introduced the sequent calculi $LK$ , $LJ$ and the natural-deduction systems $NK$ , $NJ$ in Untersuchungen über das logische Schließen (1934-35) and proved the cut-elimination Hauptsatz for both ^{[Gentzen 1934-35]}. His 1936 Die Widerspruchsfreiheit der reinen Zahlentheorie and the cleaner 1938 Neue Fassung gave the consistency proof for first-order arithmetic by assigning ordinal notations below $ε_{0}$ to derivations and reducing them transfinitely ^{[Gentzen 1936]}; the companion observation — $PA$ proves $TI (α)$ for each $α < ε_{0}$ but not $TI (ε_{0})$ — fixed $ε_{0}$ as the proof-theoretic ordinal of $PA$ . Gentzen died in 1945 in a Prague prison after the war, leaving much of the programme unfinished; his methods became the seed of all later ordinal analysis.

Oscar Veblen in 1908 had already introduced the continuous normal functions $φ_{α}$ that enumerate fixed points, providing the raw material for the next rung. Solomon Feferman and Kurt Schütte, independently in 1964-65, proved $Γ_{0}$ — the least $α$ with $φ_{α} (0) = α$ — to be the exact predicative ceiling, the Feferman-Schütte ordinal ^[Pohlers]. Heinz Bachmann's 1950 system of ordinal notations built on uncountable ordinals, refined by Gerhard Jäger and Wolfram Pohlers in the 1970s and 80s via ordinal collapsing functions and local predicativity, pushed the analysis through the Bachmann-Howard ordinal into impredicative $Π_{1}^{1}$ -analysis. Kurt Schütte's Proof Theory (1960; 2e 1977) systematized the $ω$ -rule and infinitary cut-elimination, and Pohlers's Proof Theory: The First Step into Impredicativity (2009) became the modern reference. Kurt Gödel's 1958 Dialectica paper offered a complementary, non-ordinal consistency proof via primitive-recursive functionals of finite type ^{[Godel 1958]}, extended by Clifford Spector's 1962 bar-recursion to $Π_{1}^{1}$ -analysis — reaching, by a functional route, the same strength Gentzen and Bachmann-Howard reached by ordinals.

Bibliography Master

@article{gentzen1935untersuchungen,
  author  = {Gentzen, Gerhard},
  title   = {Untersuchungen \"{u}ber das logische Schlie{\ss}en},
  journal = {Mathematische Zeitschrift},
  volume  = {39},
  year    = {1934--1935},
  pages   = {176--210, 405--431}
}

@article{gentzen1936widerspruchsfreiheit,
  author  = {Gentzen, Gerhard},
  title   = {Die Widerspruchsfreiheit der reinen Zahlentheorie},
  journal = {Mathematische Annalen},
  volume  = {112},
  year    = {1936},
  pages   = {493--565}
}

@article{gentzen1938neuefassung,
  author  = {Gentzen, Gerhard},
  title   = {Neue Fassung des Widerspruchsfreiheitsbeweises f\"{u}r die reine Zahlentheorie},
  journal = {Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, N.F.},
  volume  = {4},
  year    = {1938},
  pages   = {19--44}
}

@article{godel1931unentscheidbare,
  author  = {G\"{o}del, Kurt},
  title   = {{\"U}ber formal unentscheidbare S\"{a}tze der Principia Mathematica und verwandter Systeme I},
  journal = {Monatshefte f\"{u}r Mathematik und Physik},
  volume  = {38},
  year    = {1931},
  pages   = {173--198}
}

@article{godel1958dialectica,
  author  = {G\"{o}del, Kurt},
  title   = {{\"U}ber eine bisher noch nicht ben\"{u}tzte Erweiterung des finiten Standpunktes},
  journal = {Dialectica},
  volume  = {12},
  year    = {1958},
  pages   = {280--287}
}

@article{veblen1908continuous,
  author  = {Veblen, Oswald},
  title   = {Continuous Increasing Functions of Finite and Transfinite Ordinals},
  journal = {Transactions of the American Mathematical Society},
  volume  = {9},
  number  = {3},
  year    = {1908},
  pages   = {280--292}
}

@article{feferman1964systems,
  author  = {Feferman, Solomon},
  title   = {Systems of Predicative Analysis},
  journal = {Journal of Symbolic Logic},
  volume  = {29},
  year    = {1964},
  pages   = {1--30}
}

@article{schutte1965predicative,
  author  = {Sch\"{u}tte, Kurt},
  title   = {Eine Grenze f\"{u}r die Beweisbarkeit der Transfinieten Induktion in der verzweigten Typenlogik},
  journal = {Archiv f\"{u}r mathematische Logik und Grundlagenforschung},
  volume  = {7},
  year    = {1965},
  pages   = {45--60}
}

@article{bachmann1950normalfunktionen,
  author  = {Bachmann, Heinz},
  title   = {Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordinalzahlen},
  journal = {Vierteljahrsschrift der Naturforschenden Gesellschaft in Z\"{u}rich},
  volume  = {95},
  year    = {1950},
  pages   = {115--147}
}

@phdthesis{howard1972system,
  author = {Howard, William A.},
  title  = {A System of Abstract Constructive Ordering},
  school = {University of Warwick},
  year   = {1972}
}

@book{takeuti1987prooftheory,
  author    = {Takeuti, Gaisi},
  title     = {Proof Theory},
  edition   = {2},
  publisher = {North-Holland},
  year      = {1987}
}

@book{schutte1977prooftheory,
  author    = {Sch\"{u}tte, Kurt},
  title     = {Proof Theory},
  publisher = {Springer},
  year      = {1977}
}

@book{pohlers2009prooftheory,
  author    = {Pohlers, Wolfram},
  title     = {Proof Theory: The First Step into Impredicativity},
  publisher = {Springer},
  series    = {Universitext},
  year      = {2009}
}

@book{troelstraschwichtenberg2000,
  author    = {Troelstra, Anne S. and Schwichtenberg, Helmut},
  title     = {Basic Proof Theory},
  edition   = {2},
  publisher = {Cambridge University Press},
  series    = {Cambridge Tracts in Theoretical Computer Science},
  number    = {43},
  year      = {2000}
}

@article{kirbyparis1982goodstein,
  author  = {Kirby, Laurie and Paris, Jeff},
  title   = {Accessible Independence Results for Peano Arithmetic},
  journal = {Bulletin of the London Mathematical Society},
  volume  = {14},
  year    = {1982},
  pages   = {285--293}
}

@article{wainer1970slowgrowing,
  author  = {Wainer, Stanley S.},
  title   = {A Classification of the Ordinal Recursive Functions},
  journal = {Archiv f\"{u}r mathematische Logik und Grundlagenforschung},
  volume  = {13},
  year    = {1970},
  pages   = {136--153}
}

Prerequisites

42.05.01
42.01.01

Tier anchors

beginner: Troelstra and Schwichtenberg 2000 Basic Proof Theory 2e (Cambridge University Press) Ch. 1 read informally, with the ordinal material from Pohlers 2009 Proof Theory (Springer) Ch. 3 — the picture that a proof is a combinatorial object built from two-sided lines, that a cut is a detour through a helper lemma, that Gentzen showed every detour can be removed so a finished proof mentions only pieces of its own conclusion, and that when this idea is pushed past pure logic into arithmetic it measures a theory's strength by a transfinite ordinal, epsilon-nought for Peano arithmetic
intermediate: Troelstra and Schwichtenberg 2000 Basic Proof Theory 2e (Cambridge University Press) Ch. 1-4 (sequent calculi LK/LJ, cut-elimination and its structural corollaries, normalization for natural deduction); Cantor normal form and the ordinal-notation system below epsilon-nought as in Pohlers 2009 Proof Theory (Springer) Ch. 3-4; the proof-theoretic ordinal of a theory defined three ways, Gentzen's ordinal assignment to PA-derivations, and the fast-growing hierarchy
master: Takeuti 1987 Proof Theory 2e (North-Holland) Ch. 2 sec. 11-12 (Gentzen's consistency proof and the epsilon-nought analysis); Pohlers 2009 Proof Theory: The First Step into Impredicativity (Springer) (the Veblen hierarchy, the Feferman-Schutte ordinal Gamma-naught, the Bachmann-Howard ordinal, ordinal collapsing functions, the omega-rule and cut-elimination for infinitary derivations); Gentzen 1934/35 Untersuchungen uber das logische Schliessen and 1936 Die Widerspruchsfreiheit der reinen Zahlentheorie; Schutte 1977 Proof Theory (Springer); Godel 1958 Dialectica

References

Troelstra, A. S. and Schwichtenberg, H. — Basic Proof Theory · 2nd edition, Cambridge University Press (2000), Chapters 1-4. Chapter 1 develops Gentzen's sequent calculi LK (classical) and LJ (intuitionistic): sequents $Γ \Rightarrow Δ$ , the initial sequents $A \Rightarrow A$ , the structural rules (weakening, contraction, exchange) and the left/right logical rules for each connective and quantifier with their eigenvariable conditions, and the cut rule. The cut-elimination theorem (Hauptsatz) is proved by the double induction on the grade of the cut formula and the rank of the cut, with the principal case replacing a cut on $A$ by cuts on its immediate subformulas and the non-principal case permuting the cut upward. Chapter 3 treats normalization for natural deduction NK/NJ (Prawitz), the correspondence between maximal formulas and cut formulas, and the disjunction and existence properties for LJ as read-off corollaries of cut-freeness. The text is the standard intermediate reference for the structural backbone this unit builds the ordinal layer upon.
Pohlers, W. — Proof Theory: The First Step into Impredicativity · Universitext, Springer (2009). Chapters 3-4 develop the ordinal-analytic machinery. Cantor normal form (CNF): every nonzero $α < ε_{0}$ is uniquely $ω^{β_{1}} c_{1} + \dots + ω^{β_{n}} c_{n}$ with $α > β_{1} \geq \dots \geq β_{n}$ and $0 < c_{i} < ω$ , each $β_{i}$ recursively in CNF; this makes the ordinals below $ε_{0} = sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots}$ a primitive-recursive notation system with a computable comparison. The proof-theoretic ordinal $∥ T ∥$ of a sound recursively axiomatized $T \supseteq PRA$ is defined as the supremum of the order types of primitive-recursive well-orderings for which $T$ proves transfinite induction, equivalently the supremum of the ordinals indexing the provably total functions of $T$ in the fast-growing hierarchy $(F_{α})$ . Ordinal analyses are carried out: $∥ PRA ∥ = ω^{ω}$ , $∥ PA ∥ = ε_{0}$ , $∥ ATR_{0} ∥ = Γ_{0}$ (Feferman-Schutte), $∥ Π_{1}^{1} -CA_{0} ∥ =$ the Bachmann-Howard ordinal. The Veblen hierarchy of normal functions $φ_{α}$ , the Bachmann-Howard construction via ordinal collapsing on an uncountable $Ω$ , and the infinitary semi-formal calculus with the $ω$ -rule (from $φ (n)$ for all $n$ , infer $\forall x φ (x)$ ) together with cut-elimination for countably infinite derivations are the engine that produces these bounds.
Gentzen, G. — Untersuchungen uber das logische Schliessen; Die Widerspruchsfreiheit der reinen Zahlentheorie · Untersuchungen uber das logische Schliessen, Math. Zeitschrift 39 (1934-35), 176-210 and 405-431 (introduces LK, LJ, NK, NJ and proves the Hauptsatz for LK and LJ); Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Annalen 112 (1936), 493-565; Neue Fassung des Widerspruchsfreiheitsbeweises fur die reine Zahlentheorie, Forschungen zur Logik N.S. 4 (1938), 19-44. The 1936 and 1938 papers prove the consistency of first-order Peano arithmetic by assigning to each derivation an ordinal notation below $ε_{0}$ and giving an effective reduction that strictly lowers that ordinal on any purported proof of the empty sequent; well-foundedness of $ε_{0}$ forbids an infinite descent, so no such proof exists. The companion result — PA proves transfinite induction up to each $α < ε_{0}$ but not up to $ε_{0}$ itself — fixes $ε_{0}$ as the proof-theoretic ordinal of PA and exhibits the exact single transfinite-induction step that escapes PA and therefore delivers $Con (P A)$ from outside.
Takeuti, G. — Proof Theory · 2nd edition, North-Holland (1987), Chapter 2 sections 11-12. The canonical detailed account of Gentzen's consistency proof for first-order PA. Derivations in a sequent calculus for PA augmented with the induction rule are assigned ordinals below $ε_{0}$ via a notation that records cut-formula complexity (summed as $ω$ -powers in CNF) and the depth of induction instances; the reduction procedure on a derivation of the empty sequent pushes maximal cuts upward and unfolds induction instances one step, raising local $ω$ -powers while staying below $ε_{0}$ , so the assigned ordinal strictly decreases. Transfinite induction up to $ε_{0}$ then forbids the iterated descent, proving consistency. The lower bound — PA proves $TI (α)$ for each $α < ε_{0}$ by induction on CNF — is given in parallel, locating $ε_{0}$ as the exact proof-theoretic ordinal of PA. The same chapter sets up the framework (ordinal assignment, reduction, well-foundedness) that Pohlers and Schutte later extend to predicative and impredicative theories.
Godel, K. — Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes (Dialectica interpretation) · Dialectica 12 (1958), 280-287. An alternative constructive consistency proof of PA, complementary to Gentzen's. PA is interpreted into the quantifier-free theory $T$ of primitive-recursive functionals of finite type (Godel's System T): every PA-proof of a formula is sent to a term of $T$ realizing it, and the consistency of PA reduces to the well-foundedness of the reduction sequence terminating every term of $T$ , proved by Tait-style computability/saturated sets. Unlike Gentzen's transfinite induction to $ε_{0}$ , the Dialectica reduction uses no ordinals but reaches the same consistency strength, and it extends (via Spector's 1962 bar-recursion) to $Π_{1}^{1}$ -analysis, the same level Bachmann-Howard later pins by ordinal analysis.

Estimated time

beginner: 18m
intermediate: 55m
master: 95m