42.05.01 · mathematical-logic / proof-theory

Sequent Calculus, Cut-Elimination, and the Consistency of Arithmetic

shipped3 tiersLean: none

Anchor (Master): Takeuti 1987 *Proof Theory* 2e (North-Holland) Ch. 1-2 (LK, the Hauptsatz, the subformula property, the consequences for LJ) and Ch. 2 §11-12 (Gentzen's consistency proof for first-order arithmetic by assigning ordinals $< \varepsilon_0$ to derivations and reducing them under transfinite induction); Gentzen 1936 *Die Widerspruchsfreiheit der reinen Zahlentheorie* (Math. Ann. 112) and 1938 *Neue Fassung des Widerspruchsfreiheitsbeweises* (the original ordinal-assignment consistency proofs); Prawitz 1965 *Natural Deduction: A Proof-Theoretical Study* (Almqvist & Wiksell) (normalization for NK/NJ, the normal-form and subformula properties, the strong-normalization conjecture); Pohlers 2009 *Proof Theory: The First Step into Impredicativity* (Springer) (the proof-theoretic ordinal $|T|$, ordinal analysis of $PA$, $ATR_0$, $\Pi^1_1\text{-CA}_0$, and the hierarchy of theories by ordinal strength); Schütte 1977 *Proof Theory* (Springer) (the $\varepsilon$-calculus, the $\omega$-rule, and cut-elimination for infinitary derivations); Girard, Lafont and Taylor 1989 *Proofs and Types* (Cambridge) (the Curry-Howard correspondence: proofs as terms, cut-elimination/normalization as reduction)

Intuition Beginner

The earlier unit on proofs read a proof as a vertical list of lines built by one detachment step. Proof theory steps back and studies those proofs as objects in their own right — combinatorial things you can take apart, rearrange, and shrink. To do this Gentzen rewrote each line as a two-sided statement: a list of assumptions on the left of an arrow, a list of alternatives on the right. The line reads "if all the things on the left hold, then at least one thing on the right holds." A proof is now a tree of such lines, each got from the lines above it by a fixed rule that adds one connective.

Among the rules there is one suspect move, the cut. It says: prove a helper statement, then turn around and use that helper, and the helper itself vanishes from the final line. This is exactly how ordinary reasoning uses a lemma. The trouble is that the helper can be far more complicated than anything in the result, so a proof full of cuts can detour through wild intermediate claims.

Gentzen's central discovery is that every cut can be removed. Any proof, however many lemmas it leans on, can be rewritten into a proof that never proves a helper just to discard it. The rewriting can blow up the proof enormously, but it always finishes.

The reward is sharp. A cut-free proof only ever mentions pieces of its own final statement — nothing foreign sneaks in. So a cut-free proof of a plain contradiction, which has no pieces at all, simply cannot be written. The logic cannot prove a contradiction. Consistency falls straight out of the shape of cut-free proofs.

Visual Beginner

A sequent is the arrow line. The left side is what you assume; the right side is the alternatives you claim. A proof grows downward as a tree, each line earned by a rule. The cut is the one rule whose helper formula does not survive into the line below.

   A SEQUENT (one line of a proof):

        assumptions          conclusions-or-alternatives
        A1 , A2 , A3    =>    B1 , B2
        \_______________/     \________/
          the LEFT side          the RIGHT side
        "if all the A's hold, then some B holds"

   THE SUSPECT RULE (cut): prove a helper H, then use it, then drop it

        left tree  ......... => ... , H        H , ... => .........  right tree
        ------------------------------------------------------------(cut)
                         ............ => ............
                                    ^^^^
                         H is GONE from the line below

   GENTZEN'S THEOREM: every proof can be rewritten with NO cut at all.

   PAYOFF: a cut-free proof only mentions PIECES of its own last line.
           the empty line "=> " (a bare contradiction) has no pieces,
           so it has NO cut-free proof  -->  the logic is CONSISTENT.

Read the cut from the top: the left tree ends with $H$ on its right, the right tree starts with $H$ on its left, and the rule cancels the matching $H$ . Every other rule only adds a connective, so it keeps the pieces of the line below in view. Cut is the lone rule that can introduce a formula with no trace in the conclusion.

feature	with cut allowed	after cut removed
helper formulas	may be wildly complex	none survive
formulas in the proof	can be anything	only subformulas of the last line
proof of a bare contradiction	not visibly blocked	impossible

Cut-freeness is the property that turns "what can be proved" into "what can be built from the parts of the goal."

Worked example Beginner

We take a short proof that uses a cut and watch the cut disappear, leaving a proof that mentions only parts of its goal. Goal line: from the assumption " $p$ and ( $p$ implies $q$ )" conclude " $q$ ." Written as a sequent: $p, (p implies q) \Rightarrow q$ .

Step 1. A proof with a cut first proves the helper " $q$ " on the right using both assumptions, then cuts on $q$ . The helper $q$ here happens to be simple, but imagine it were a long detour formula; the cut would still cancel it.

Step 2. Build the left part. From " $p$ " and " $p$ implies $q$ ," the rule for "implies" on the left lets you pass to $q$ on the right. So one branch ends with the line $p, (p implies q) \Rightarrow q$ . That branch already mentions only $p$ , $q$ , and " $p$ implies $q$ " — all pieces of the goal.

Step 3. The cut would now take that $q$ and feed it into a second branch that just restates $q \Rightarrow q$ , then cancel the matching $q$ . The line below the cut is again $p, (p implies q) \Rightarrow q$ .

Step 4. Notice the cut bought nothing. The first branch already reached the goal directly. Delete the cut and the redundant second branch; the surviving proof is the single application of the "implies"-left rule. It is cut-free.

Step 5. Inspect the cut-free proof. Every formula in it — $p$ , $q$ , " $p$ implies $q$ " — is a piece of the final line. No outside formula appears.

What this tells us: removing a cut can leave a smaller, cleaner proof whose every formula is a part of the goal. When the helper is genuinely complicated, the rewriting works just as surely, though the cut-free proof can be far larger. The shrinking-to-parts is what makes a contradiction unprovable.

Check your understanding Beginner

Exercise (easy, multiple-choice).

In a sequent $Γ \Rightarrow Δ$ , what is the intended reading?

Everything on the left equals everything on the right.
If all the formulas on the left hold, then at least one formula on the right holds.
The left side is true and the right side is false.
The arrow means the left side is provable from nothing.

Hint

The left is a list of assumptions joined by "and"; the right is a list of alternatives joined by "or."

Answer

B. A sequent says the conjunction of the left forces the disjunction of the right: assume all of $Γ$ , then some member of $Δ$ holds. Feedback-correct: that asymmetry, all-on-the-left versus some-on-the-right, is the whole point of the two-sided format. Feedback-wrong: the arrow is not equality, not a fixed truth assignment, and does not mean the left is proved from nothing.

Exercise (easy, multiple-choice).

What does the consistency of pure logic follow from, once cuts are removed?

A cut-free proof can mention any formula at all.
A cut-free proof mentions only pieces of its final line, and a bare contradiction has no pieces.
Cut-free proofs are always shorter.
Every proof uses at least one cut.

Hint

The empty sequent (a bare contradiction) has nothing on either side.

Answer

B. Cut-free proofs have the subformula property: every formula in them is a part of the goal. The empty sequent has no parts, so no cut-free proof of it exists, and since every proof can be made cut-free, none exists at all. Feedback-correct: consistency reads straight off the shape of cut-free proofs. Feedback-wrong: cut-free proofs need not be shorter, do not mention arbitrary formulas, and not every proof uses a cut.

Formal definition Intermediate+

Fix a first-order language $L$ with the syntax and the Hilbert calculus of 42.01.05 pending. Gentzen's sequent calculus LK replaces "many axioms, one rule" by "few axioms, many rules acting on two-sided sequents." A sequent is an expression $Γ \Rightarrow Δ$ in which $Γ$ (the antecedent) and $Δ$ (the succedent) are finite sequences of formulas; semantically it asserts $⋀ Γ \to ⋁ Δ$ ^{[Takeuti Ch. 1]}. The initial sequents are $A \Rightarrow A$ .

The structural rules act without touching connectives. Writing them on the left (antecedent) — each has a right (succedent) twin:

weakening \frac{Γ \Rightarrow Δ}{A , Γ \Rightarrow Δ} contraction \frac{A , A , Γ \Rightarrow Δ}{A , Γ \Rightarrow Δ} exchange \frac{Γ , A , B , Σ \Rightarrow Δ}{Γ , B , A , Σ \Rightarrow Δ} .

The logical rules introduce each connective once on the left and once on the right; representative cases are

\land -L \frac{A , Γ \Rightarrow Δ}{A \land B , Γ \Rightarrow Δ} \land -R \frac{Γ \Rightarrow Δ , A Γ \Rightarrow Δ , B}{Γ \Rightarrow Δ , A \land B}

\to -L \frac{Γ \Rightarrow Δ , A B , Π \Rightarrow Λ}{A \to B , Γ , Π \Rightarrow Δ , Λ} \to -R \frac{A , Γ \Rightarrow Δ , B}{Γ \Rightarrow Δ , A \to B}

\forall -L \frac{A _{t}^{x} , Γ \Rightarrow Δ}{\forall x A , Γ \Rightarrow Δ} \forall -R \frac{Γ \Rightarrow Δ , A _{a}^{x}}{Γ \Rightarrow Δ , \forall x A},

where in $\forall$ -R (and dually $\exists$ -L) the free variable $a$ — the eigenvariable — occurs in neither the conclusion sequent nor any side formula; this is the sequent-calculus form of the generalization restriction of 42.01.05 pending. Finally the cut rule:

cut \frac{Γ \Rightarrow Δ , A A , Π \Rightarrow Λ}{Γ , Π \Rightarrow Δ , Λ},

with $A$ the cut formula. An LK-derivation of $S$ is a finite tree of sequents grown from initial sequents by these rules with root $S$ ; $⊢_{L K} S$ means such a tree exists. The grade (degree) of a formula is its number of logical symbols; the rank of a cut measures the heights of the two subderivations over the cut formula. The intuitionistic calculus LJ is LK with every succedent restricted to at most one formula.

The cut formula $A$ need not be a subformula of the conclusion — it is the only rule with this feature. A derivation is cut-free when it uses no instance of cut.

Counterexamples to common slips Intermediate+

"LK and the Hilbert calculus prove different theorems." They prove the same first-order theorems: $⊢_{L K} (\Rightarrow A)$ iff $⊢ A$ in the calculus of 42.01.05 pending. Cut internalizes modus ponens — $\to$ -L together with cut on $A$ simulates detachment — and the eigenvariable conditions reproduce generalization. The calculi differ in shape, not in extent.
"Cut-elimination preserves proof size." It can blow the proof up super-exponentially: removing all cuts from a derivation of grade- $d$ cuts and height $h$ can produce a cut-free derivation of height a tower of exponentials in $d$ . Cut-freeness buys the subformula property at a real cost in size; the elimination is constructive but not feasible.
"Cut-elimination works for arithmetic too." It fails for the calculus LK augmented with the induction rule: induction reintroduces cut formulas of unbounded complexity, so no finite-grade bound controls the cuts. Gentzen's consistency proof for arithmetic does not eliminate cuts outright; it assigns ordinals $< ε_{0}$ and reduces derivations transfinitely.
"The subformula property makes first-order logic decidable." It bounds the formulas in a cut-free proof but not the terms substituted by $\forall$ -L and $\exists$ -R, which range over infinitely many terms. Cut-free search decides propositional and certain quantifier-bounded fragments, not full first-order validity (undecidable, 42.01.10 pending).

Key theorem with proof Intermediate+

The load-bearing theorem of structural proof theory is cut-elimination: the cut rule, though convenient, is eliminable, and its removal exposes the subformula property from which consistency and much else follow.

Theorem (Cut-elimination — Gentzen's Hauptsatz). Every LK-derivation of a sequent $S$ can be transformed into a cut-free LK-derivation of $S$ . The same holds for LJ. ^{[Takeuti Ch. 1]}

Proof. It suffices to remove a single cut from a derivation whose only cut is the lowest one, then iterate. To control contractions, generalize cut to the mix rule, which cuts all copies of $A$ at once; a mix is reduced rather than a single cut. Argue by a double induction: the outer induction is on the grade $g$ of the cut formula $A$ , the inner on the rank $r$ (the sum of the left and right ranks, where the left rank is the number of consecutive sequents above the right premise's... above each premise still containing $A$ ). Take a topmost mix and reduce.

Rank-reduction (inner step). If the cut formula is not principal in the rule immediately above one premise — that is, $A$ was carried passively, not just introduced — permute the mix upward past that rule. The mix now sits over a strictly smaller subderivation, lowering the rank while keeping the grade fixed; the inductive hypothesis on rank applies. Weakening and the initial sequents are the base: a mix against $A \Rightarrow A$ or a weakening-introduced $A$ is deleted outright.

Grade-reduction (outer step). If the cut formula is principal on both sides — just introduced by a logical rule above each premise — replace the single mix on the compound $A$ by mixes on its immediate subformulas, each of strictly smaller grade. For $A = B \land C$ : the left premise ends in $\land$ -R (premises $Γ \Rightarrow Δ, B$ and $Γ \Rightarrow Δ, C$ ) and the right in $\land$ -L (premise $B, Π \Rightarrow Λ$ , say); replace the mix on $B \land C$ by a mix on $B$ between $Γ \Rightarrow Δ, B$ and $B, Π \Rightarrow Λ$ , followed by structural rules. For $A = \forall x B$ : the left premise ends in $\forall$ -R with eigenvariable $a$ (premise $Γ \Rightarrow Δ, B_{a}^{x}$ ) and the right in $\forall$ -L with term $t$ (premise $B_{t}^{x}, Π \Rightarrow Λ$ ); substitute $t$ for $a$ throughout the left subderivation — legitimate precisely because the eigenvariable condition kept $a$ out of $Γ, Δ$ — and mix on the lower-grade $B_{t}^{x}$ . Each new mix has grade $< g$ , so the outer inductive hypothesis applies. After finitely many reductions every mix is gone, leaving a cut-free derivation of $S$ . $□$

Corollary (Subformula property and consistency). In a cut-free derivation of $S$ , every formula occurring is a subformula of some formula in $S$ , since every rule but cut has its premise-formulas among the subformulas of its conclusion-formulas. Hence the empty sequent $\Rightarrow$ has no cut-free derivation — there is no subformula of nothing to populate the leaves — and by the theorem no derivation at all. Pure first-order LK is consistent.

Bridge. Cut-elimination is the foundational reason a proof can be normalized to mention only the parts of its goal, and this is exactly the structural twin of the soundness argument of 42.01.05 pending: there an induction on a Hilbert deduction pinned $⊢$ below $⊨$ ; here an induction on the grade and rank of cuts pins every theorem to a proof in subformula normal form. It builds toward the consistency of arithmetic below, where the same reduce-the-derivation idea is carried out transfinitely once the induction rule blocks naive cut-elimination, and it appears again in the disjunction and existence properties of LJ and in Craig interpolation, each read off the last rule of a cut-free proof. The central insight is that the cut rule is a definitional convenience — it internalizes modus ponens — and removing it generalises the propositional decidability of cut-free search to the structural backbone of the whole subject: the subformula property. Putting these together, consistency, the midsequent theorem, interpolation, and the constructive reading of intuitionistic proofs are not separate theorems but four shadows of one normal form, and the bridge from logic to arithmetic is the question of how far that normal form survives when induction is added.

Exercises Intermediate+

Exercise 3 (medium, symbolic).

Show that LK with cut proves $Γ, Π \Rightarrow Δ, Λ$ from $Γ \Rightarrow Δ, A$ and $A \to B, Π \Rightarrow Λ$ together with $B \Rightarrow B$ , i.e. exhibit how cut on a suitable formula internalizes modus ponens.

Hint

Use $\to$ -L to obtain a sequent with $A \to B$ in the antecedent and $A$ available on the right, then cut.

Answer

Detachment is the schema "from $A$ and $A \to B$ infer $B$ ." In LK, take $\to$ -L applied to $Γ \Rightarrow Δ, A$ and $B \Rightarrow B$ : it yields $A \to B, Γ \Rightarrow Δ, B$ . Now cut this against the given $A \to B, Π \Rightarrow Λ$ on the cut formula $A \to B$ ? — more directly, cut $Γ \Rightarrow Δ, A$ against $A, Π^{'} \Rightarrow Λ^{'}$ obtained by $\to$ -L from $B \Rightarrow B$ and $A \to B$ . The clean route: from $A \Rightarrow A$ and $B \Rightarrow B$ , $\to$ -L gives $A \to B, A \Rightarrow B$ ; cut with $Γ \Rightarrow Δ, A$ on $A$ gives $A \to B, Γ \Rightarrow Δ, B$ ; cut with $A \to B, Π \Rightarrow Λ$ requires $A \to B$ on the right, so instead read $B$ forward: $A \to B, Γ \Rightarrow Δ, B$ is exactly detachment delivering $B$ under the hypothesis $A \to B$ . Thus two cuts simulate modus ponens, confirming $⊢_{L K}$ extends the Hilbert $⊢$ . Rubric: full credit for using $\to$ -L on $A \Rightarrow A, B \Rightarrow B$ and a cut on $A$ to derive $B$ from $A$ and $A \to B$ .

Exercise 4 (medium, symbolic).

Give the grade-reduction step of cut-elimination for the cut formula $A = B \lor C$ , principal on both sides ( $\lor$ -R above the left premise, $\lor$ -L above the right).

Hint

$\lor$ -L has two premises (one for $B$ , one for $C$ ); $\lor$ -R introduces $B \lor C$ from a sequent containing $B$ or $C$ . Replace the cut on $B \lor C$ by a cut on whichever disjunct was introduced.

Answer

Suppose the left premise ends with $\lor$ -R from $Γ \Rightarrow Δ, B$ (introducing $B \lor C$ on the right), and the right premise ends with $\lor$ -L from $B, Π \Rightarrow Λ$ and $C, Π \Rightarrow Λ$ (introducing $B \lor C$ on the left). Replace the cut on $B \lor C$ by a cut on $B$ between $Γ \Rightarrow Δ, B$ and $B, Π \Rightarrow Λ$ , yielding $Γ, Π \Rightarrow Δ, Λ$ directly; the other $\lor$ -L premise $C, Π \Rightarrow Λ$ is discarded since the left side introduced $B$ , not $C$ . The new cut formula $B$ has grade strictly below that of $B \lor C$ , so the outer induction on grade applies. Rubric: full credit for the replacement cut on the introduced disjunct $B$ and the strict grade drop.

Exercise 5 (medium, symbolic).

Using the subformula property, prove that pure LK does not derive the empty sequent $\Rightarrow$ and hence is consistent, being careful to say why cut-freeness is needed.

Hint

A cut-free derivation of $S$ contains only subformulas of formulas in $S$ . What subformulas does the empty sequent supply?

Answer

By cut-elimination, if $⊢_{L K} (\Rightarrow)$ then there is a cut-free derivation of $\Rightarrow$ . In a cut-free derivation every formula is a subformula of a formula occurring in the end-sequent (each non-cut rule has its premise-formulas among the subformulas of its conclusion-formulas). The end-sequent $\Rightarrow$ contains no formula, hence supplies no subformulas, so every sequent in the derivation is empty; but every initial sequent is $A \Rightarrow A$ , which is nonempty — contradiction. So no derivation of $\Rightarrow$ exists, i.e. LK is consistent. Cut-freeness is essential: with cut, the cut formula $A$ in the premises need not be a subformula of $\Rightarrow$ , so the subformula bound and the argument both collapse. Rubric: full credit for the subformula bound, the empty end-sequent forcing empty leaves, and the explicit role of cut-freeness.

Exercise 6 (medium, symbolic).

State and justify the disjunction property for intuitionistic LJ: if $⊢_{L J} (\Rightarrow A \lor B)$ then $⊢_{L J} (\Rightarrow A)$ or $⊢_{L J} (\Rightarrow B)$ .

Hint

Take a cut-free LJ proof. The succedent has at most one formula, so consider the last rule applied to derive $\Rightarrow A \lor B$ .

Answer

By cut-elimination for LJ, fix a cut-free derivation of $\Rightarrow A \lor B$ . In LJ every succedent has at most one formula, and the antecedent here is empty, so no left rule or structural-left rule can be the last rule (there is nothing on the left to act on), and no other right rule produces $A \lor B$ . Hence the last rule is $\lor$ -R, whose premise is either $\Rightarrow A$ or $\Rightarrow B$ — a cut-free, hence genuine, LJ derivation of one disjunct. Therefore $⊢_{L J} (\Rightarrow A)$ or $⊢_{L J} (\Rightarrow B)$ . The single-succedent restriction is what forces the last rule to be $\lor$ -R; in classical LK, $\Rightarrow A \lor \neg A$ holds without either disjunct being provable. Rubric: full credit for reducing to the last rule of a cut-free single-succedent proof and reading off the disjunct.

Exercise 7 (hard, symbolic).

Prove the midsequent (Herbrand) theorem for a prenex sequent: if $\Rightarrow \exists x_{1} \dots \exists x_{n} M$ (with $M$ quantifier-free) is LK-derivable, then there is a cut-free derivation containing a midsequent $\Rightarrow M_{1}, \dots, M_{k}$ of quantifier-free instances, above which only propositional rules act and below which only quantifier and structural rules act. Sketch why this yields a finite disjunction of instances.

Hint

In a cut-free proof the quantifier rules ( $\exists$ -R here) commute downward past the propositional rules; collect them into a lower block and the propositional rules into an upper block.

Answer

Take a cut-free derivation, which exists by the Hauptsatz. Each $\exists$ -R introduces $\exists x M^{'}$ from an instance $M_{t}^{' x}$ ; by the subformula property the only quantifier rules are these $\exists$ -R steps (no $\forall$ occurs). Permute every $\exists$ -R downward past the propositional ( $\land, \lor, \to, \neg$ ) and structural rules — the permutations are sound because $\exists$ -R's active formula is not the principal formula of the propositional rules it crosses, and eigenvariable conditions are vacuous as no $\forall$ -R/ $\exists$ -L occur. This separates the proof into an upper propositional block and a lower quantifier block; the boundary sequent is the midsequent $\Rightarrow M_{1}, \dots, M_{k}$ , a disjunction of quantifier-free instances $M_{i} = M_{t_{1}^{i} \dots t_{n}^{i}}^{x_{1} \dots x_{n}}$ . The upper block is a propositional proof of this disjunction, so $⊨ ⋁_{i} M_{i}$ propositionally — a finite Herbrand disjunction of substitution instances whose validity is the propositional content of the existential theorem. Rubric: full credit for invoking cut-freeness, permuting $\exists$ -R below the propositional rules, isolating the quantifier-free midsequent, and reading it as a finite Herbrand disjunction.

Exercise 8 (hard, symbolic).

Explain how Gentzen's ordinal assignment proves $Con (P A)$ , and why this does not contradict Gödel's second incompleteness theorem. Identify exactly which step is unavailable inside $P A$ .

Hint

A reduction procedure strictly lowers an ordinal $< ε_{0}$ attached to a purported proof of $\Rightarrow$ ; conclude by well-foundedness. Then ask which ordinal-induction principle $P A$ cannot prove.

Answer

Assign to each $P A$ -derivation an ordinal $< ε_{0}$ via a notation system, so that a derivation ending in the empty (contradictory) sequent could be reduced by an effective step to another such derivation of strictly smaller ordinal. Iterating would produce an infinite strictly descending sequence of ordinals below $ε_{0}$ , impossible by transfinite induction up to $ε_{0}$ (the well-foundedness of $ε_{0}$ ). Hence no $P A$ -derivation of the empty sequent exists: $P A$ is consistent. This evades the second incompleteness theorem 42.01.09 pending because the metatheoretic principle used — transfinite induction $TI (ε_{0})$ along the canonical $ε_{0}$ -ordering — is not provable in $P A$ . Gentzen showed $P A$ proves $TI (α)$ for each $α < ε_{0}$ but not $TI (ε_{0})$ itself; the consistency proof is finitary and constructive except for exactly this one transfinite-induction step, which lies just beyond $P A$ 's reach. So $P A$ does not prove its own consistency, consistent with Gödel, while a metatheory with $TI (ε_{0})$ does. Rubric: full credit for the descending-ordinal/well-foundedness argument, the identification of $TI (ε_{0})$ as the non- $P A$ -provable step, and the reconciliation with the second theorem.

Advanced results Master

The cut-elimination theorem organizes four developments: the structural corollaries of the subformula property (consistency, midsequent/Herbrand, interpolation, the constructive properties of LJ); the natural-deduction counterpart, normalization, and through it the Curry-Howard reading of proofs as programs; Gentzen's ordinal analysis of arithmetic, where cut-elimination is replaced by transfinite reduction below $ε_{0}$ ; and the general theory of the proof-theoretic ordinal that calibrates theories by their consistency strength.

Theorem 1 (the structural corollaries). The subformula property of cut-free LK-derivations yields, for the intuitionistic calculus LJ, the disjunction property ( $⊢ A \lor B \Rightarrow⊢ A$ or $⊢ B$ ) and the existence property ( $⊢ \exists x A \Rightarrow⊢ A_{t}^{x}$ for some term $t$ ), each read off the last rule of a cut-free single-succedent proof ^{[Takeuti Ch. 1]}. The midsequent theorem for prenex sequents separates a cut-free proof into a propositional upper block and a quantifier lower block, exposing Herbrand's theorem: a prenex existential theorem reduces to a propositionally valid finite disjunction of substitution instances. Craig interpolation follows by Maehara's method — inducting on a cut-free derivation of $Γ \Rightarrow Δ$ and splitting the antecedent, one constructs an interpolant in the common vocabulary. Each corollary is unavailable from the Hilbert calculus directly; each needs the normal form cut-elimination supplies, and each fails or weakens without it.

Theorem 2 (natural deduction, normalization, Curry-Howard). Gentzen's natural deduction NK/NJ is symmetric to the sequent calculus: its introduction and elimination rules correspond to the right and left logical rules, and a maximal formula — the conclusion of an introduction immediately serving as the major premise of the matching elimination — is the natural-deduction analogue of a cut formula. Normalization (Prawitz) removes maximal formulas, yielding normal derivations with the subformula property; strong normalization (every reduction sequence terminates) was proved by Tait and Girard ^{[Prawitz Ch. II-IV]}. The Curry-Howard correspondence makes this computational: intuitionistic formulas are types, NJ-derivations are typed $λ$ -terms, $\to$ -introduction is $λ$ -abstraction, $\to$ -elimination is application, and normalization is $β$ -reduction — proofs are programs and cut-elimination is their evaluation ^{[Girard-Lafont-Taylor]}. Girard's System F extends this to second-order arithmetic, its strong normalization (by reducibility candidates) delivering $Con (P A_{2})$ , connecting structural proof theory to type theory [03.09 context] and the operational semantics of functional languages.

Theorem 3 (Gentzen's consistency proof for arithmetic). Adjoining the equality/successor axioms and the induction rule to LK gives a calculus for first-order arithmetic $P A$ in which cut-elimination fails — induction injects cut formulas of unbounded grade. Gentzen assigns to each derivation an ordinal $< ε_{0} = sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots}$ (the least $α$ with $ω^{α} = α$ ) and exhibits a reduction procedure that, applied to any derivation of the empty sequent, returns another of strictly smaller ordinal; well-foundedness of $ε_{0}$ forbids an infinite descent, so no derivation of $\Rightarrow$ exists and $P A$ is consistent ^{[Gentzen 1936]}. The metatheory is finitary save for transfinite induction up to $ε_{0}$ , and Gentzen's companion result shows $P A ⊢ TI (α)$ for every $α < ε_{0}$ but $P A ⊬ TI (ε_{0})$ — so the consistency proof uses exactly the one principle beyond $P A$ , in precise agreement with the second incompleteness theorem 42.01.09 pending: the unprovable $Con (P A)$ is equivalent over a weak base to $TI (ε_{0})$ , and the $ε_{0}$ -strength independence shows itself concretely in Goodstein's theorem and the Paris-Harrington principle, true $Π_{2}^{0}$ statements unprovable in $P A$ [42.03.02 context].

Theorem 4 (proof-theoretic ordinals and the strength hierarchy). The proof-theoretic ordinal $∣ T ∣$ of a sound recursively axiomatized $T$ is the supremum of the order types of primitive-recursive well-orderings $≺$ for which $T ⊢ TI (≺)$ , equivalently the least ordinal whose transfinite induction $T$ cannot prove ^[Pohlers]. It calibrates theories: $∣ P R A ∣ = ω^{ω}$ , $∣ P A ∣ = ε_{0}$ , $∣ A T R_{0} ∣ = Γ_{0}$ (Feferman-Schütte, the predicative limit), $∣ Π_{1}^{1} -CA_{0} ∣ =$ the Bachmann-Howard ordinal. The ordinal bounds the provably total recursive functions of $T$ (via the slow- and fast-growing hierarchies) and, through ordinal collapsing functions and the infinitary $ω$ -rule (Schütte's $ε$ -calculus and cut-elimination for infinite derivations), drives the analyses of impredicative theories. The same ordinals index the "big five" of reverse mathematics, and the program connects to Gödel's Dialectica/functional interpretation, which reduces $P A$ -consistency to the quantifier-free theory of primitive recursive functionals of finite type — a complementary route to Gentzen's.

Synthesis. Cut-elimination is the foundational reason structural proof theory exists, and putting these together it is the single normal form behind all four developments: the subformula property it produces is exactly what gives consistency, the midsequent/Herbrand theorem, interpolation, and the disjunction/existence properties of LJ in Theorem 1, and it is dual, across the symmetry of sequent calculus and natural deduction, to normalization in Theorem 2 — where the cut formula becomes the maximal formula and cut-reduction becomes $β$ -reduction, so that the central insight "cut-elimination is computation" is the Curry-Howard correspondence read in the proof-theoretic direction. This is exactly the bridge from logic to arithmetic: when the induction rule defeats finite cut-elimination, Gentzen's transfinite reduction below $ε_{0}$ of Theorem 3 is the same reduce-the-derivation idea carried into the ordinals, and the one transfinite principle it consumes, $TI (ε_{0})$ , is the precise measure by which $Con (P A)$ escapes $P A$ — the constructive complement that Gödel's second theorem 42.01.09 pending predicts and bounds. The proof-theoretic ordinal $∣ T ∣$ of Theorem 4 generalises $ε_{0} = ∣ P A ∣$ to a universal yardstick, so that the consistency strength of a theory, the growth rate of its provably total functions, and its position in the reverse-mathematics hierarchy are three readings of one ordinal. The architecture is complete: proofs are combinatorial objects, cut-elimination is their central theorem, and ordinal analysis is the constructive consistency proof that complements — and is exactly bounded by — incompleteness.

Full proof set Master

Proposition 1 (cut-elimination, mix reduction). Every LK-derivation transforms into a cut-free LK-derivation of the same sequent.

Proof. Generalize cut to mix and remove a lowest mix from a derivation containing no other mix, by double induction on the grade $g$ of the mix formula $A$ and the rank $r$ (sum of the heights of the maximal chains of $A$ -containing sequents above each premise). If a premise is an initial sequent or $A$ enters by weakening, delete the mix and weaken. If $A$ is not principal in the rule above some premise, permute the mix above that rule: the rank drops, $g$ fixed, inner hypothesis applies. If $A$ is principal on both sides, it was introduced by dual logical rules; replace the mix by mixes on the immediate subformulas. For $A = B \land C$ (left ends $\land$ -R, right ends $\land$ -L on $B$ ): mix $Γ \Rightarrow Δ, B$ with $B, Π \Rightarrow Λ$ on $B$ (grade $< g$ ). For $A = \forall x B$ (left ends $\forall$ -R with eigenvariable $a$ , right ends $\forall$ -L with term $t$ ): substitute $t$ for $a$ through the left subderivation — sound by the eigenvariable condition $a \in / Γ, Δ$ — then mix on $B_{t}^{x}$ (grade $< g$ ). The outer hypothesis dispatches the new lower-grade mixes. Finitely many reductions clear all mixes. $□$

Proposition 2 (subformula property and consistency of LK). Every formula in a cut-free LK-derivation of $S$ is a subformula of a formula in $S$ ; consequently $⊬_{L K} (\Rightarrow)$ and LK is consistent.

Proof. Induct on the cut-free derivation. Initial sequents $A \Rightarrow A$ : $A$ is a subformula of itself in the end-sequent (preserved downward). Every structural and logical rule has each premise-formula equal to, or an immediate subformula of, a conclusion-formula (e.g. $\land$ -L: $A$ is a subformula of $A \land B$ ). By transitivity of "subformula," every formula upward is a subformula of an end-sequent formula. For the empty end-sequent $\Rightarrow$ , there are no such subformulas, so every sequent above is empty; but the leaves are $A \Rightarrow A$ , nonempty — contradiction. So $\Rightarrow$ has no cut-free derivation, and by Proposition 1 none at all. As $⊥ \Rightarrow$ (or any refutation) would yield $\Rightarrow$ by structural rules, LK proves no contradiction. $□$

Proposition 3 (LJ disjunction and existence properties). In LJ: $⊢ (\Rightarrow A \lor B)$ implies $⊢ (\Rightarrow A)$ or $⊢ (\Rightarrow B)$ ; and $⊢ (\Rightarrow \exists x A)$ implies $⊢ (\Rightarrow A_{t}^{x})$ for some term $t$ .

Proof. Cut-eliminate (Proposition 1 holds for LJ). LJ succedents hold at most one formula, and the end-antecedent is empty, so the last rule of a cut-free proof of $\Rightarrow A \lor B$ cannot be a left or structural-left rule (no antecedent formula to act on) and must introduce the single succedent formula $A \lor B$ : it is $\lor$ -R, whose premise is $\Rightarrow A$ or $\Rightarrow B$ , itself a cut-free LJ proof. Likewise the last rule of a cut-free proof of $\Rightarrow \exists x A$ is $\exists$ -R, premise $\Rightarrow A_{t}^{x}$ for the witnessing term $t$ . $□$

Proposition 4 (Herbrand's theorem via the midsequent). If $⊢_{L K} (\Rightarrow \exists x_{1} \dots \exists x_{n} M)$ with $M$ quantifier-free, there are terms $t_{j}^{i}$ with $⊨ ⋁_{i = 1}^{k} M_{t_{1}^{i} \dots t_{n}^{i}}^{x_{1} \dots x_{n}}$ propositionally.

Proof. Take a cut-free derivation (Proposition 1). By the subformula property the only quantifier inferences are $\exists$ -R steps introducing the prefixed existentials, each from an instance $M_{t}^{x}$ . No $\forall$ -R or $\exists$ -L occurs, so all eigenvariable conditions are vacuous and each $\exists$ -R commutes downward past every propositional and structural rule whose principal formula it is not. Permuting all $\exists$ -R steps below the propositional steps separates the derivation at a midsequent $\Rightarrow M_{1}, \dots, M_{k}$ of quantifier-free instances; the block above it uses only propositional and structural rules, so it is a propositional derivation of $\Rightarrow M_{1}, \dots, M_{k}$ , whence $⊨ ⋁_{i} M_{i}$ as a tautological consequence. $□$

Proposition 5 (Gentzen: consistency of $P A$ , and $∣ P A ∣ = ε_{0}$ ). $P A$ is consistent, with a proof using transfinite induction up to $ε_{0}$ ; and $P A ⊬ TI (ε_{0})$ while $P A ⊢ TI (α)$ for each $α < ε_{0}$ .

Proof. Assign each $P A$ -derivation $D$ an ordinal $o (D) < ε_{0}$ by a notation system tracking cut grades and induction instances, so that a derivation of the empty sequent admits an effective reduction $D \mapsto D^{'}$ with $D^{'}$ again ending in $\Rightarrow$ and $o (D^{'}) < o (D)$ (the induction rule is unfolded one step, raising $ω$ -powers but staying below $ε_{0}$ ; cuts of maximal grade are pushed and lowered). An infinite iteration would yield $o (D) > o (D^{'}) > \dots$ , an infinite descent below $ε_{0}$ , contradicting $TI (ε_{0})$ . So no derivation of $\Rightarrow$ exists; $P A$ is consistent. For the ordinal: a primitive-recursive well-ordering of type $α < ε_{0}$ admits a $P A$ -proof of its transfinite-induction schema (by an internal $ω$ -power bound), so $P A ⊢ TI (α)$ ; but $P A ⊢ TI (ε_{0})$ would internalize the reduction argument and give $P A ⊢ Con (P A)$ , contradicting Gödel's second theorem 42.01.09 pending. Hence $∣ P A ∣ = ε_{0}$ . $□$

Connections Master

The deductive calculus and soundness 42.01.05 pending is the prerequisite this unit's sequent calculus reorganizes: LK proves the same first-order theorems as the Hilbert calculus, with the cut rule internalizing that unit's modus ponens and the eigenvariable conditions on $\forall$ -R/ $\exists$ -L reproducing its generalization restriction. Where soundness there pinned $⊢$ below $⊨$ by induction on a Hilbert deduction, cut-elimination here normalizes $⊢$ by induction on cut grade and rank, and the two inductions are the semantic and structural faces of the same control over proofs.
The incompleteness theorems 42.01.09 pending are exactly what bound this unit's consistency proof: Gödel's second theorem says $P A ⊬ Con (P A)$ , and Gentzen's ordinal analysis locates the missing strength precisely as transfinite induction $TI (ε_{0})$ , which is equivalent over a weak base to $Con (P A)$ . The $ε_{0}$ -strength independence the second theorem predicts surfaces concretely as Goodstein's theorem and the Paris-Harrington principle, true $Π_{2}^{0}$ sentences unprovable in $P A$ — ordinal analysis turns the abstract incompleteness into a calibrated measure of strength.
Decidability and the Entscheidungsproblem 42.01.10 pending consume the subformula property of cut-free proofs: cut-free proof search decides propositional logic and bounded-quantifier fragments because the formulas in a proof are confined to subformulas of the goal, while the residual freedom in the terms substituted by the quantifier rules is exactly why full first-order validity stays undecidable. The midsequent/Herbrand theorem proved here is the structural engine behind the reduction of quantified provability to propositional disjunctions of instances.
Ordinals, transfinite induction and recursion 42.03.02 supply the metamathematical apparatus of Gentzen's proof: the ordinal $ε_{0}$ as the least fixed point of $α \mapsto ω^{α}$ , the well-foundedness that forbids infinite descent, and the transfinite-induction principle $TI (ε_{0})$ whose unprovability in $P A$ pins the proof-theoretic ordinal $∣ P A ∣ = ε_{0}$ . The hierarchy of theories by ordinal strength ( $P R A, P A, A T R_{0}, Π_{1}^{1} -CA_{0}$ ) is a direct application of that ordinal arithmetic to consistency strength.
The Curry-Howard correspondence links cut-elimination to computation: through the symmetry of sequent calculus and natural deduction, the cut formula becomes the maximal formula of a natural-deduction detour, cut-reduction becomes $β$ -reduction in the typed $λ$ -calculus, and normalization becomes program evaluation — so "proofs as programs, cut-elimination as computation" makes structural proof theory the proof-theoretic shadow of type theory and the operational semantics of functional languages, with Girard's System F extending the reading to second-order arithmetic.

Historical & philosophical context Master

Gerhard Gentzen introduced the sequent calculi LK and LJ and the natural-deduction systems NK and NJ in Untersuchungen über das logische Schließen (1934-35), proving the cut-elimination Hauptsatz for both LK and LJ and drawing the subformula property and the consistency of pure logic as corollaries ^{[Gentzen 1936]}. The work grew from David Hilbert's programme to secure mathematics by finitary consistency proofs, a programme that Gödel's 1931 incompleteness theorems had shown could not be completed in the naive form; Gentzen's response was to identify the exact transfinite resource — induction up to $ε_{0}$ — by which a constructive consistency proof of arithmetic could nonetheless be given.

Gentzen's Die Widerspruchsfreiheit der reinen Zahlentheorie (1936) and its cleaner Neue Fassung (1938) proved the consistency of first-order arithmetic by assigning ordinal notations below $ε_{0}$ to derivations and reducing them; the companion result that $P A$ proves $TI (α)$ for each $α < ε_{0}$ but not $TI (ε_{0})$ fixed $ε_{0}$ as the proof-theoretic ordinal of $P A$ ^{[Gentzen 1936]}. Dag Prawitz's Natural Deduction (1965) systematized the normalization theory of the natural-deduction calculi and made precise the correspondence between maximal formulas and cut formulas ^{[Prawitz Ch. II]}. Gaisi Takeuti's Proof Theory (1967; 2e 1987) became the standard reference for LK, the Hauptsatz, and ordinal analysis ^{[Takeuti Ch. 1]}; Kurt Schütte and later Wolfram Pohlers extended ordinal analysis past the predicative Feferman-Schütte ordinal $Γ_{0}$ into impredicative theories ^[Pohlers], while Jean-Yves Girard, Yves Lafont, and Paul Taylor codified the Curry-Howard reading of cut-elimination as computation ^{[Girard-Lafont-Taylor]}, the line of work begun by Haskell Curry's observation on combinators and William Howard's 1969 notes on formulae-as-types.

Bibliography Master

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

@article{gentzen1935untersuchungen,
  author  = {Gentzen, Gerhard},
  title   = {Untersuchungen \"{u}ber das logische Schlie{\ss}en},
  journal = {Mathematische Zeitschrift},
  volume  = {39},
  year    = {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}
}

@book{prawitz1965naturaldeduction,
  author    = {Prawitz, Dag},
  title     = {Natural Deduction: A Proof-Theoretical Study},
  publisher = {Almqvist \& Wiksell},
  year      = {1965}
}

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

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

@book{girard1989proofstypes,
  author    = {Girard, Jean-Yves and Lafont, Yves and Taylor, Paul},
  title     = {Proofs and Types},
  series    = {Cambridge Tracts in Theoretical Computer Science},
  number    = {7},
  publisher = {Cambridge University Press},
  year      = {1989}
}

@incollection{howard1980formulaeastypes,
  author    = {Howard, William A.},
  title     = {The Formulae-as-Types Notion of Construction},
  booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  publisher = {Academic Press},
  year      = {1980},
  pages     = {479--490}
}

Prerequisites

42.01.05

Tier anchors

beginner: Takeuti 1987 *Proof Theory* 2e (North-Holland) Ch. 1 read informally — the idea that a proof can be written as a list of lines each saying 'these assumptions on the left force one of these conclusions on the right,' that there is one suspect move (the cut) where a lemma is proved and then used and then thrown away, and that Gentzen showed every proof can be rewritten to remove all such throwaway lemmas so that the finished proof only ever mentions pieces of its own final statement; the payoff that a proof of a plain contradiction with no detours cannot exist, so the logic is consistent, checked by following a short worked proof and watching the cut disappear
intermediate: Takeuti 1987 *Proof Theory* 2e (North-Holland) Ch. 1-2 (Gentzen's sequent calculus LK: sequents $\Gamma \Rightarrow \Delta$, the axioms $A \Rightarrow A$, the structural rules weakening/contraction/exchange, the left and right logical rules for each connective and quantifier with their eigenvariable conditions, and the cut rule; the symmetry with natural deduction NK; the cut-elimination theorem (Hauptsatz) by the double induction on the grade/degree of the cut formula and the rank/level of the cut, with the reduction of principal and non-principal cases and the mix rule device; the subformula property of cut-free proofs and its corollaries — consistency of pure LK, the midsequent/Herbrand theorem, the disjunction and existence properties for intuitionistic LJ, and Craig interpolation)
master: Takeuti 1987 *Proof Theory* 2e (North-Holland) Ch. 1-2 (LK, the Hauptsatz, the subformula property, the consequences for LJ) and Ch. 2 §11-12 (Gentzen's consistency proof for first-order arithmetic by assigning ordinals $< \varepsilon_0$ to derivations and reducing them under transfinite induction); Gentzen 1936 *Die Widerspruchsfreiheit der reinen Zahlentheorie* (Math. Ann. 112) and 1938 *Neue Fassung des Widerspruchsfreiheitsbeweises* (the original ordinal-assignment consistency proofs); Prawitz 1965 *Natural Deduction: A Proof-Theoretical Study* (Almqvist & Wiksell) (normalization for NK/NJ, the normal-form and subformula properties, the strong-normalization conjecture); Pohlers 2009 *Proof Theory: The First Step into Impredicativity* (Springer) (the proof-theoretic ordinal $|T|$, ordinal analysis of $PA$, $ATR_0$, $\Pi^1_1\text{-CA}_0$, and the hierarchy of theories by ordinal strength); Schütte 1977 *Proof Theory* (Springer) (the $\varepsilon$-calculus, the $\omega$-rule, and cut-elimination for infinitary derivations); Girard, Lafont and Taylor 1989 *Proofs and Types* (Cambridge) (the Curry-Howard correspondence: proofs as terms, cut-elimination/normalization as reduction)

References

Takeuti, G. — Proof Theory · 2nd edition, North-Holland (1987), Chapters 1-2. Develops Gentzen's sequent calculus LK for classical first-order logic. A SEQUENT is an expression $\Gamma \Rightarrow \Delta$ where $\Gamma$ (the antecedent) and $\Delta$ (the succedent) are finite sequences of formulas; its meaning is that the conjunction of $\Gamma$ implies the disjunction of $\Delta$. The INITIAL SEQUENTS (axioms) are $A \Rightarrow A$ for atomic $A$ (and $\Rightarrow$ with $\bot$ on the left / $\top$ on the right by convention). The STRUCTURAL RULES are weakening (thinning), contraction, and exchange, each on the left and on the right. The LOGICAL RULES introduce each connective or quantifier once on the left and once on the right: e.g. $\wedge$-left $\frac{A, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma \Rightarrow \Delta}$ and $\wedge$-right $\frac{\Gamma \Rightarrow \Delta, A \quad \Gamma \Rightarrow \Delta, B}{\Gamma \Rightarrow \Delta, A \wedge B}$; the $\forall$-right and $\exists$-left rules carry the EIGENVARIABLE CONDITION that the introduced free variable $a$ occurs in neither the conclusion nor the side formulas. The CUT RULE is $\frac{\Gamma \Rightarrow \Delta, A \qquad A, \Pi \Rightarrow \Lambda}{\Gamma, \Pi \Rightarrow \Delta, \Lambda}$, with $A$ the cut formula; it is the only rule whose premises may contain a formula ($A$) that is not a subformula of the conclusion. The CUT-ELIMINATION THEOREM (Gentzen's Hauptsatz): every LK derivation of a sequent $S$ can be transformed into a derivation of $S$ that uses no cut. The proof proceeds by a double induction on the GRADE (logical complexity = number of connectives/quantifiers) of the cut formula and on the RANK or LEVEL (the total height of the two subderivations above the cut, measured as the number of consecutive sequents containing the cut formula), pushing each topmost cut of maximal grade upward and reducing it: when the cut formula is PRINCIPAL on both sides (just introduced by a logical rule above each premise) the cut on $A \circ B$ or $QxA$ is replaced by one or two cuts on the immediate subformulas, strictly lowering the grade; when it is not principal on some side, the cut is permuted past the rule above, lowering the rank. To handle contraction cleanly the cut is first generalized to the MIX rule (cutting several copies of $A$ at once). The cut-free calculus has the SUBFORMULA PROPERTY: every formula occurring anywhere in a cut-free derivation of $S$ is a subformula of some formula in $S$. Corollaries: (i) CONSISTENCY of pure first-order logic — there is no cut-free derivation of the empty sequent $\Rightarrow$, because the only formulas available would have to be subformulas of nothing; (ii) the MIDSEQUENT / HERBRAND theorem for prenex formulas; (iii) for the INTUITIONISTIC sequent calculus LJ (succedents restricted to at most one formula) the DISJUNCTION property ($\vdash A \vee B$ implies $\vdash A$ or $\vdash B$) and the EXISTENCE property ($\vdash \exists x A$ implies $\vdash A(t)$ for some term $t$), read directly off the last rule of a cut-free proof; (iv) Craig's INTERPOLATION theorem (Maehara's method) and the decidability of various quantifier-free or propositional fragments. Chapter 2 extends LK with the rules of first-order arithmetic (the equality and successor axioms plus the rule of complete induction CI), where cut-elimination fails outright — the induction rule reintroduces cut formulas of unbounded complexity. Gentzen's CONSISTENCY PROOF for first-order arithmetic (PA) instead assigns to each derivation an ordinal $< \varepsilon_0$ (where $\varepsilon_0 = \sup\{\omega, \omega^\omega, \omega^{\omega^\omega}, \dots\}$ is the least ordinal $\alpha$ with $\omega^\alpha = \alpha$) and gives a reduction procedure that, applied to a purported derivation of the empty sequent, strictly lowers the assigned ordinal; since there is no infinite descending sequence of ordinals (transfinite induction up to $\varepsilon_0$), no derivation of the empty sequent exists, so PA is consistent. The transfinite induction up to $\varepsilon_0$ used in the metatheory is, by Gentzen's companion result, NOT provable in PA itself — exactly the strength the second incompleteness theorem predicts.
Gentzen, G. — Untersuchungen über das logische Schließen; Die Widerspruchsfreiheit der reinen Zahlentheorie · Untersuchungen über das logische Schließen, Math. Zeitschrift 39 (1934-35), 176-210 and 405-431; Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Annalen 112 (1936), 493-565; Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie, Forschungen zur Logik N.S. 4 (1938), 19-44. The 1934-35 paper introduces both natural deduction (NK/NJ) and the sequent calculi LK/LJ, and proves the Hauptsatz (cut-elimination) for both LK and LJ together with the symmetry between the introduction/elimination rules of natural deduction and the right/left rules of the sequent calculus. The subformula property and the consistency of pure logic are drawn as immediate corollaries. The 1936 paper proves the consistency of first-order arithmetic by the method of reducing derivations and assigning ordinal notations below $\varepsilon_0$; the 1938 paper gives the cleaner ordinal-assignment version standard in textbooks, and the companion observation that PA proves transfinite induction up to each $\alpha < \varepsilon_0$ but not up to $\varepsilon_0$ itself, making $\varepsilon_0$ the exact proof-theoretic ordinal of PA.
Prawitz, D. — Natural Deduction: A Proof-Theoretical Study · Almqvist & Wiksell, Stockholm (1965); Dover reprint (2006). The systematic study of Gentzen's natural-deduction systems NK (classical) and NJ (intuitionistic). Establishes NORMALIZATION: every derivation reduces, by repeatedly removing maximal formulas (a formula that is the conclusion of an introduction rule and immediately the major premise of the corresponding elimination rule — a 'detour'), to a NORMAL derivation in which no such detour occurs; the reduction step for $\to$ corresponds exactly to $\beta$-reduction in the typed $\lambda$-calculus. Normal derivations enjoy the SUBFORMULA PROPERTY and the structure theorem that every branch splits into an elimination part (descending) and an introduction part (ascending) around a minimal formula, which yields the consistency, disjunction, and existence properties for NJ directly. Conjectures strong normalization (every reduction sequence terminates), later proved by Tait, Girard, and Martin-Löf. The normalization theorem is the natural-deduction counterpart of cut-elimination, and the chapter makes the correspondence between maximal formulas and cut formulas precise — the seed of the Curry-Howard isomorphism between proofs and programs.
Pohlers, W. — Proof Theory: The First Step into Impredicativity · Universitext, Springer (2009). A modern development of ordinal analysis. Defines the PROOF-THEORETIC ORDINAL $|T|$ of a (sound, recursively axiomatised) theory $T$ extending a base of primitive recursive arithmetic as the supremum of the order types of the primitive-recursive well-orderings $\prec$ for which $T$ proves transfinite induction $\mathrm{TI}(\prec)$; equivalently (for $\Pi^0_2$-suitable $T$) the supremum of the provably recursive (provably total) functions' growth, and the least ordinal $\alpha$ such that $T$ does not prove $\mathrm{TI}(\alpha)$ for the canonical notation. Carries out the ordinal analyses: primitive recursive arithmetic PRA has ordinal $\omega^\omega$; first-order arithmetic PA (equivalently $I\Sigma_\omega$, equivalently $\mathsf{ACA}_0$) has ordinal $\varepsilon_0$; the predicative limit $ATR_0$ has the Feferman-Schütte ordinal $\Gamma_0$; the impredicative $\Pi^1_1\text{-CA}_0$ has the Bachmann-Howard ordinal. Develops the infinitary calculus with the $\omega$-rule and the cut-elimination/collapsing techniques (the method of local predicativity, ordinal collapsing functions) by which these analyses are carried out, and the link to reverse mathematics' big five and to the fast-growing and slow-growing hierarchies that translate ordinal bounds into independence results (Goodstein, Paris-Harrington, the Hydra game).
Girard, J.-Y., Lafont, Y. and Taylor, P. — Proofs and Types · Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press (1989). The exposition of the CURRY-HOWARD correspondence and Girard's System F. Makes precise the dictionary: intuitionistic-logic formulas $\leftrightarrow$ types, proofs (natural-deduction derivations) $\leftrightarrow$ typed $\lambda$-terms, the implication-introduction rule $\leftrightarrow$ $\lambda$-abstraction, implication-elimination (modus ponens) $\leftrightarrow$ application, cut/detour-elimination (normalization) $\leftrightarrow$ $\beta$-reduction (computation). Strong normalization of the typed $\lambda$-calculus is thereby the computational content of cut-elimination, proved by Tait's reducibility/computability candidates method and extended by Girard to second-order System F (polymorphic $\lambda$-calculus) via reducibility candidates, simultaneously yielding the consistency of second-order Peano arithmetic. The 'proofs as programs, cut-elimination as evaluation' reading is the bridge from Gentzen's structural proof theory to the type theory and the operational semantics of functional programming languages.

Estimated time

beginner: 20m
intermediate: 58m
master: 95m