Proof Theory and Cut-Elimination

Why This Matters

Proof theory treats proofs themselves as objects of study. Instead of asking "is this statement true?", it asks "what is the structure of a proof of this statement?" The central result is Gentzen's Hauptsatz (cut-elimination theorem): any proof that uses lemmas can be transformed into a proof that does not. This is surprising because lemmas seem essential to mathematical practice, yet they are theoretically eliminable.

For computer science and AI: cut-elimination is the logical counterpart of beta-reduction in lambda calculus (via Curry-Howard). Proof search algorithms in automated theorem provers often work in cut-free systems because the search space is smaller. Tactic-based proof assistants like Lean and Coq effectively manage cuts (lemma usage) through their tactic language.

Proof Systems

Definition

Natural Deduction

Natural deduction (Gentzen, 1935) organizes proofs by introduction and elimination rules for each connective. Each logical connective ($\land, \lor, \to, \forall, \exists, \neg$) has:

• An introduction rule: how to prove a statement with that connective as the main connective.
• An elimination rule: how to use a statement with that connective.

Example: to prove $A \to B$ (introduction), assume $A$ and derive $B$. To use $A \to B$ (elimination, modus ponens), combine it with a proof of $A$ to get $B$.

Definition

Sequent Calculus

Sequent calculus (Gentzen, 1935) uses sequents of the form $\Gamma \vdash \Delta$, meaning "from the assumptions $\Gamma$, at least one of the conclusions $\Delta$ follows." Rules operate on both sides of the turnstile $\vdash$.

In classical logic, $\Delta$ can have multiple formulas (classical sequent calculus). In intuitionistic logic, $\Delta$ has exactly one formula.

The sequent calculus makes the structure of proofs more explicit than natural deduction, which is why it is preferred for proof-theoretic analysis.

Definition

Cut Rule

The cut rule in sequent calculus is:

$\frac{\Gamma \vdash A, \Delta \qquad \Gamma', A \vdash \Delta'}{\Gamma, \Gamma' \vdash \Delta, \Delta'}$

This says: if you can prove $A$ (left premise) and you can use $A$ to prove something (right premise), then you can combine them. The formula $A$ is the cut formula: it appears in the premises but not the conclusion. The cut rule corresponds to using a lemma.

Main Theorems

Theorem

Cut-Elimination Theorem (Gentzen's Hauptsatz)

Statement

Every proof in sequent calculus that uses the cut rule can be transformed into a proof of the same sequent that does not use the cut rule. Formally: if $\Gamma \vdash \Delta$ is provable in sequent calculus with cut, then it is provable without cut.

Intuition

Lemmas are convenient but not necessary. Every indirect proof (one that goes through intermediate results) can be "unfolded" into a direct proof. The price is that the direct proof may be much longer. Cut-elimination is the logical analogue of inlining all function calls in a program.

Proof Sketch

The proof proceeds by double induction on (1) the complexity of the cut formula and (2) the height of the proof tree above the cut. The key steps:

1. If the cut formula $A$ is introduced on both sides of the cut by their respective rules, the cut can be replaced by cuts on simpler formulas (reducing complexity).
2. If the cut formula is not the principal formula of the last rule on one side, the cut can be pushed upward in the proof tree (reducing height).
3. Since both measures decrease and are bounded below, the process terminates.

The procedure transforms the proof step by step, replacing each cut with cuts on simpler formulas until no cuts remain.

Why It Matters

Cut-elimination has three major consequences:

1. Consistency of arithmetic: Gentzen used cut-elimination (extended to arithmetic with transfinite induction up to $\varepsilon_0$) to prove the consistency of Peano Arithmetic. This was the first consistency proof for arithmetic.

2. Subformula property: in a cut-free proof, every formula appearing in the proof is a subformula of the conclusion. This drastically restricts the search space for proof search.

3. Computational content: via Curry-Howard, cut-elimination corresponds to program evaluation (beta-reduction). A proof with cuts is a program with function calls; cut-elimination inlines all calls.

Failure Mode

Cut-elimination can cause an exponential (or worse) blowup in proof size. A proof of length $n$ with cuts may require a proof of length $2^{2^{\cdots^n}}$ (tower of exponentials) without cuts. In practice, proofs with lemmas are far more manageable. Also, cut-elimination for first-order logic is well-understood, but extending it to stronger systems (second-order arithmetic, set theory) requires additional techniques and sometimes transfinite methods.

The Subformula Property

A cut-free proof has the subformula property: every formula appearing in the proof is a subformula of the formulas in the conclusion. This means:

• To prove $A \land B \to A$, the only formulas that appear in a cut-free proof are $A \land B \to A$, $A \land B$, $A$, and $B$. No "unrelated" formula can appear.
• This makes proof search in cut-free systems tractable in principle: you only need to consider subformulas of the goal.

This is why many automated reasoning systems work with cut-free calculi: the search space is bounded by the structure of the goal.

Connection to Computation

Via the Curry-Howard correspondence:

Proof theory	Lambda calculus
Proof	Program (lambda term)
Cut rule	Function application (using a lemma = calling a function)
Cut-elimination	Beta-reduction (evaluation)
Cut-free proof	Normal form (fully evaluated program)
Subformula property	Types in normal forms come from the input/output types

Cut-elimination guarantees that proofs can be simplified, just as beta-reduction guarantees that programs can be evaluated. The Church-Rosser theorem (confluence of beta-reduction) corresponds to confluence of cut-elimination: the final cut-free proof is unique (up to trivial permutations).

Connection to Proof Assistants

Modern proof assistants use tactics to construct proofs interactively. Tactics like apply, intro, cases, and simp correspond to proof rules and proof transformations. The kernel then verifies that the constructed proof term is well-typed.

Cut-elimination tells us that the tactic have (which introduces a lemma, i.e., a cut) is always eliminable in principle. In practice, have is used constantly because proofs without lemmas are unreadably large. The theoretical eliminability of cuts guarantees that no new provability is gained by using lemmas; they are purely a matter of proof organization.

Common Confusions

Watch Out

Cut-elimination does not mean you should avoid lemmas

Cut-elimination is a metatheorem about the proof system, not advice for proof writing. Proofs with lemmas (cuts) are shorter, more readable, and more modular. Cut-elimination says these lemmas do not add logical power, but they add enormous practical value. No working mathematician or proof engineer avoids lemmas.

Watch Out

The subformula property is about cut-free proofs only

Proofs with cuts can mention any formula. The subformula property only holds for cut-free proofs. This is precisely why cut-elimination is useful for proof search: it tells you that restricting attention to subformulas is complete.

Exercises

ExerciseCore

Problem

In natural deduction, what are the introduction and elimination rules for $\to$ (implication)? Write them out explicitly.

Hint

Reveal Solution

ExerciseAdvanced

Problem

Explain the proof-size blowup in cut-elimination. Give an informal argument for why eliminating a single cut can double the proof size.

Hint

Reveal Solution

ExerciseAdvanced

Problem

How does the cut rule correspond to function application in the Curry-Howard correspondence? Write a specific example.

Hint

Reveal Solution

References

Canonical:

• Gentzen, "Investigations into Logical Deduction" (1935)
• Girard, Lafont, Taylor, Proofs and Types (1989), Chapters 1-6
• Troelstra & Schwichtenberg, Basic Proof Theory (2000)

Accessible:

• Negri & von Plato, Structural Proof Theory (2001)

Next Topics

• [Dependent type theory](/topics/type-theory): the full Curry-Howard correspondence for predicate logic
• SAT/SMT and automated reasoning: where cut-free proof search becomes practical