Cut elimination: Gentzen's theorem and subformula property

In 1934 Gerhard Gentzen proved that any mathematical proof can be rewritten so it never 'invents' new concepts -- all formulas used are contained in the statement being proved. This Hauptsatz ('main theorem') implies the consistency of Peano arithmetic.

• Proof assistants Coq and Lean use the Curry-Howard correspondence: cut elimination = program normalization.
• Microsoft Research uses Lean 4 to verify mathematics and industrial code -- rooted in Gentzen's 1934 theorem.

Sequent calculus LK

Gerhard Gentzen in 1934 introduced sequent calculus LK and proved the Hauptsatz (cut elimination). LK builds proofs of sequents Gamma => Delta (if all formulas in Gamma hold, at least one in Delta holds). The cut rule introduces 'lemmas' but complicates proof analysis. Cut elimination restores analyticity: all formulas in a proof are subformulas of the proven sequent.

Consequences of cut elimination

From Gentzen's theorem follow: consistency of PA (via ordinal analysis up to epsilon_0), Craig's interpolation theorem (1957), conservativity theorems for extensions. In computer science, cut elimination ensures normalization in simply typed lambda calculus (Curry-Howard correspondence).

Key results

• LK = sequent calculus. Cut rule introduces 'lemmas'.
• Gentzen's Hauptsatz: cut-free proof exists for any theorem of LK.
• Subformula property: cut-free proofs are analytic.
• Curry-Howard: Cut = beta-redex, cut elimination = lambda term normalization.