Theorem

Cut-Elimination Theorem (Gentzen's Hauptsatz)

Logic and Foundations

The Cut-Elimination Theorem states that any proof in a sequent-calculus system for first-order logic that uses the cut rule, which allows a lemma to be introduced and then discharged, can be transformed into a proof of the same statement that uses no cut rule at all. Named for Gerhard Gentzen, who called it his Hauptsatz, or main theorem, it shows every proof can in principle be reduced to one built entirely from the formula being proved, a fact with wide consequences for proof theory including consistency proofs and the subformula property.

Facts

Statement

Any sequent that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. 1

Proof Year

1935 1

Classification

Statement Form

Existence Theorem 1

Sources

1. Cut-elimination theorem

Lead paragraph, third sentence
The cut-elimination theorem states that any sequent that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule.
Lead paragraph, second sentence
It was originally proved by Gerhard Gentzen in part I of his landmark 1935 paper

Switch Atlas

The Inner World

The Civil World

The Natural World

Cut-Elimination Theorem (Gentzen's Hauptsatz)