Cut-elimination
Teorema de corte-eliminación
- Date
- 1935 · confidence high
- Place
- Göttingen, Germany
- Credited to
- Gerhard Gentzen
- Field
- Knowledge & symbols
What was discovered
The cut-elimination theorem (Gentzen's Hauptsatz) is the central result establishing the significance of the sequent calculus: it states that any sequent provable using the cut rule also has a cut-free proof. It was proved by Gerhard Gentzen in 1935 for the systems LJ and LK, formalizing intuitionistic and classical logic.
What it led to
- Foundation of modern proof theory
- Basis of the Curry–Howard correspondence and typed functional programming
- Application in automated proof verification