Abstract
Gentzen introduces two formal systems for logical deduction: natural deduction and the sequent calculus. Natural deduction provides a formalization closer to informal mathematical reasoning, with introduction and elimination rules for each logical connective. The sequent calculus offers a more symmetric presentation suitable for proof-theoretic analysis. The paper establishes fundamental results including the equivalence of the two systems, the admissibility of cut, and the subformula property. This work laid the foundation for structural proof theory and influenced the development of type theory through the Curry-Howard correspondence.
Key Contributions
- Introduction of natural deduction systems (NK for classical, NJ for intuitionistic)
- Introduction of sequent calculus (LK for classical, LJ for intuitionistic)
- Proof of the cut-elimination theorem (Hauptsatz)
- Demonstration that cut-free proofs satisfy the subformula property
- Establishment of consistency proofs for arithmetic using proof-theoretic methods
Significance
Gentzen’s natural deduction system later became the basis for the Curry-Howard correspondence, where introduction rules correspond to type constructors and elimination rules to destructors. The sequent calculus provides the foundation for linear logic, focusing logic, and many modern proof assistants. Cut-elimination remains one of the central proof-theoretic tools for establishing consistency and computational properties of logical systems.