Sequent Calculus

Origin. Gentzen introduced sequent calculus (1934-35). Proof system with sequents Γ ⊢ Δ. Cut-elimination theorem: proofs can be normalized. Foundation for proof theory. Structural proof analysis and proof search.

Models. Proofs as structured derivations. Natural deduction: proofs with assumptions. Sequent calculus: symmetric, explicit context. Left rules: use assumptions. Right rules: prove conclusions. Cut: compose proofs. Structural rules: manipulate contexts.

Formalism.

Sequent: Γ ⊢ Δ (antecedents ⊢ succedents) Classical: multiple conclusions (Δ is list). Intuitionistic: single conclusion (Δ is one formula).

Structural rules:

Weakening (W): Γ ⊢ Δ / Γ,A ⊢ Δ
Contraction (C): Γ,A,A ⊢ Δ / Γ,A ⊢ Δ
Exchange (E): Γ,A,B,Δ ⊢ Σ / Γ,B,A,Δ ⊢ Σ

Logical rules (classical): ∧-R: (Γ ⊢ A,Δ Γ ⊢ B,Δ) / Γ ⊢ A∧B, Δ ∧-L: Γ,A,B ⊢ Δ / Γ, A∧B ⊢ Δ

∨-R: Γ ⊢ A,B,Δ / Γ ⊢ A∨B, Δ ∨-L: (Γ,A ⊢ Δ Γ,B ⊢ Δ) / Γ, A∨B ⊢ Δ

→-R: Γ,A ⊢ B,Δ / Γ ⊢ A→B, Δ →-L: (Γ ⊢ A,Δ Γ,B ⊢ Δ) / Γ, A→B ⊢ Δ

Cut rule: (Γ ⊢ A,Δ Γ,A ⊢ Δ) / Γ ⊢ Δ (eliminable!)

Cut-elimination: Every proof with cut transforms to cut-free proof. "Hauptsatz" — Gentzen's main theorem.

Symbols.

Symbol	Unicode	Name	Meaning
⊢	U+22A2	Turnstile	Entails
Γ, Δ	—	Contexts	Formula lists
-R, -L	—	Right, Left	Introduction sides
cut	—	Cut	Proof composition
W, C, E	—	Structural	Weakening, contraction, exchange

Metatheory. Cut-elimination: central theorem. Subformula property (cut-free): only subformulas appear. Decidability: cut-free search terminates for propositional. Consistency: no proof of ⊢ ⊥. Interpolation: Craig interpolation. Proof identity and proof nets.

Applies to. Proof theory foundations. Automated theorem proving. Type theory (Curry-Howard). Logic programming (resolution). Proof normalization. Substructural logics.

Limitations. Proof search: rule application choices. Identity of proofs debated. Quantifiers complicate search. Non-deterministic (which rule?). Efficiency depends on strategy.