cutelimination

Cut-elimination is a fundamental result in proof theory concerning the sequent calculus. In Gentzen’s systems for classical and intuitionistic logic, known as LK and LJ, proofs are built from initial sequents using inference rules plus the cut rule. The cut rule allows one to deduce a sequent from two premises that share a common formula, effectively combining intermediate results. Cut-elimination asserts that every provable sequent has a cut-free proof, i.e., a proof that uses no cut rule. Consequently, cut-free proofs enjoy the subformula property: every formula appearing in the proof is a subformula of the end-sequent.

Gentzen proved the Hauptsatz (main theorem) of cut-elimination in the 1930s. The standard proof proceeds by induction on a measure that combines the complexity of the cut formula and the height of the proof. It provides a construction that reduces the complexity of cuts step by step, ultimately transforming any proof with cuts into a cut-free one. This requires showing that cuts can be permuted upward through other inferences and that each reduction preserves provability. The result yields consistency proofs for arithmetic and stronger theories since a cut-free proof cannot derive falsehoods from true premises if the end-sequent is valid.

Consequences and scope: Cut-elimination implies the subformula property, interpolation, and connections with normalization in typed lambda calculi via the Curry–Howard correspondence. It informs proof search and automated theorem proving, though elimination can cause exponential growth in proof size. The theorem has been extended to many logics beyond LK and LJ, including modal and linear logics, and to natural deduction via normalization.