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
LK	—	—	Classical calculus
LJ	—	—	Intuitionistic
W, C	—	—	Weakening, Contraction
Cut	—	—	Cut rule

Metatheory. Cut elimination constructive. Complexity bounds on cut elimination. Herbrand's theorem via cut-free proofs. Decidability of propositional fragments. Extensions: ω-rule, infinitary systems.

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

Limitations. Full arithmetic requires transfinite induction. Propositional decidable but slow. Rule permutations obscure proof identity. Extensions complex.