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 / Sequent arrow	Separates antecedent from succedent
Γ, Δ	U+0393, U+0394	Gamma, Delta / Contexts	Antecedent and succedent multisets
Σ	U+03A3	Sigma / Context	Third context, as in the exchange rule
∧	U+2227	Conjunction	Introduced by ∧-R and ∧-L
∨	U+2228	Disjunction	Introduced by ∨-R and ∨-L
→	U+2192	Implication	Introduced by →-R and →-L
⊥	U+22A5	Falsum	Absurdity; ⊢ ⊥ is what consistency denies
-R, -L	—	Right, Left	The two sides a connective may be introduced on
cut	—	Cut rule	Composition of proofs on a shared formula
W, C, E	—	Structural rules	Weakening, contraction, exchange
LK, LJ	—	Classical, intuitionistic	Gentzen's two calculi

Metatheory. Gentzen's Hauptsatz (1934–35): every derivation in LK or LJ transforms into a cut-free derivation, by a constructive procedure driven by a double induction on the degree of the cut formula and on the rank of the cut. Cut-free derivations have the subformula property, from which four things follow: consistency, since no cut-free derivation can end in the empty sequent; the midsequent theorem for prenex sequents, and hence Herbrand's theorem; Craig interpolation, constructed by Maehara's method by splitting each cut-free sequent; and for LJ the disjunction and existence properties. LJ is LK with succedents restricted to at most one formula, so the difference between classical and intuitionistic logic is structural rather than a matter of logical rules. Cut elimination is not free: Statman (1978) and Orevkov (1979) exhibited sequences of formulas whose shortest cut-free proofs are hyperexponentially larger than proofs using cut, so cut gives a non-elementary speedup. Cut-free propositional search terminates, giving decidability; first-order cut-free search is only semi-decidable.

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

Limitations. The subformula property comes with a non-elementary blow-up, and the reason is mathematical rather than incidental: a cut-free proof cannot state a lemma once and reuse it, so every use must be re-derived in place. Ordinary two-sided sequents do not present every logic analytically — S5 and Gödel–Dummett logic resisted cut-free ordinary sequent formulation, which is what prompted hypersequents, and modal logics generally need labels or nesting. The structural rules are not decoration: dropping contraction and weakening yields linear logic, dropping exchange yields non-commutative calculi, so presentation and consequence relation are not separable. Cut cannot be eliminated once an induction rule is added — Gentzen's consistency proof for arithmetic replaces induction by transfinite induction to ε₀, or by the infinitary ω-rule, rather than eliminating cuts finitarily. Finally, derivations differing only by permutation of independent rules are distinct objects, so the calculus supplies no notion of proof identity; proof nets were introduced to supply one.