Gentzen Systems

Origin. Gerhard Gentzen (1934-1935). Twin proof systems: natural deduction and sequent calculus. Hauptsatz (cut elimination). Consistency proof for arithmetic. Foundation of structural proof theory.

Models. LK: classical sequent calculus. LJ: intuitionistic variant. NK, NJ: natural deduction counterparts. Structural rules explicit. Cut-free proofs have subformula property.

Formalism.

Sequent: Γ ⊢ Δ (intuitionistic: Γ ⊢ A, single conclusion) Γ: antecedents (assumed true) Δ: succedents (one concluded true)

Structural rules: Weakening: Γ ⊢ Δ / Γ, A ⊢ Δ Contraction: Γ, A, A ⊢ Δ / Γ, A ⊢ Δ Exchange: Γ, A, B, Δ ⊢ / Γ, B, A, Δ ⊢ Cut: Γ ⊢ A, Δ and A, Γ' ⊢ Δ' / Γ, Γ' ⊢ Δ, Δ'

Logical rules (LK examples): Right and: Γ ⊢ A, Δ Γ ⊢ B, Δ ─────────────────────── ∧R Γ ⊢ A ∧ B, Δ

Left and: Γ, A ⊢ Δ Γ, B ⊢ Δ ─────────── ∧L₁ ─────────── ∧L₂ Γ, A∧B ⊢ Δ Γ, A∧B ⊢ Δ

Cut elimination (Hauptsatz): Every LK/LJ proof converts to cut-free proof. Constructive: terminating procedure.

Consequences: Subformula property: cut-free proofs only use subformulas. Consistency: no proof of ⊢ (in LJ) or ⊢ ⊥. Interpolation: if A ⊢ B cut-free, interpolant exists.

Symbols.

Symbol	Unicode	Name	Meaning
⊢	U+22A2	Turnstile / Sequent arrow	Separates antecedent from succedent
Γ, Δ	U+0393, U+0394	Gamma, Delta / Contexts	Antecedent and succedent
∧	U+2227	Conjunction	Principal formula of ∧R, ∧L₁, ∧L₂
⊥	U+22A5	Falsum	The contradiction consistency excludes
ε	U+03B5	Epsilon	As in ε₀, the ordinal of the consistency proof
ω	U+03C9	Omega	Index of the infinitary ω-rule
LK	—	Klassisch	Gentzen's classical sequent calculus
LJ	—	Intuitionistisch	LK with at most one succedent formula
NK, NJ	—	Natural deduction	The classical and intuitionistic ND systems
W, C	—	Structural rules	Weakening, contraction
Cut	—	Cut rule	The rule the Hauptsatz eliminates

Metatheory. The Hauptsatz (Gentzen 1934–35) eliminates cut from LK and LJ constructively, by double induction on the degree and rank of the cut, and the same argument transfers to NK and NJ as normalization. Cut-free proofs are analytic, so consistency, Herbrand's theorem via the midsequent theorem, and Craig interpolation all follow. Gentzen (1936, 1938) proved the consistency of first-order arithmetic by assigning ordinals below ε₀ to derivations and showing the reduction procedure strictly decreases the assigned ordinal; the extra strength used is transfinite induction to ε₀, and Gentzen (1943) showed PA proves transfinite induction for every α < ε₀ but not for ε₀, so the calibration is exact and the second incompleteness theorem is respected. Schütte later replaced the finitary combinatorics by infinitary derivations with the ω-rule, where cut elimination is easy and the ordinal measures derivation height. Cut is not redundant in practice: Statman and Orevkov showed cut affords a non-elementary speedup, so the analytic system blows up hyperexponentially for its subformula property.

Applies to. Proof theory. Automated reasoning. Consistency proofs. Proof search. Foundations of mathematics.

Limitations. Cut elimination stops at induction: no finitary cut-elimination procedure covers arithmetic with the induction rule, which is why Gentzen needed transfinite induction to ε₀ and why Schütte moved to an infinitary calculus whose derivations are not finite objects. The classical–intuitionistic difference in LK and LJ is carried by a structural restriction on the succedent, not by any logical rule, so one cannot obtain LJ by deleting a rule of LK. Rule permutations proliferate: LK derivations differing only in the order of independent inferences are distinct, and the calculus offers no criterion of proof identity. LK and LJ do not present modal or substructural logics without further apparatus — labels, nesting, or modified structural rules — and the cut-free system's lack of lemmas is what makes the non-elementary blow-up unavoidable rather than an artefact of Gentzen's particular procedure.