Sequent Calculus: Symmetric Proof Systems

Introduction

Sequent calculus is a proof system developed by Gerhard Gentzen that provides a symmetric, structural approach to formal reasoning. Unlike natural deduction, which treats assumptions and conclusions asymmetrically, sequent calculus treats them symmetrically through sequents. This symmetry makes sequent calculus particularly suitable for automated reasoning and theoretical analysis.

This article explores sequent calculus, its rules, and applications in logic and computation.

Historical Context

Gerhard Gentzen developed sequent calculus (LK for classical logic, LJ for intuitionistic logic) in 1934 as part of his work on proof theory. He proved the fundamental cut-elimination theorem, showing that any proof can be transformed into a cut-free proof. This result has profound implications for logic and computation. Sequent calculus has become essential in proof theory, automated reasoning, and the study of logical systems.

Core Concepts

Sequents

Definition: A sequent is an expression Γ ⊢ Δ where:

• Γ (antecedent): A sequence of formulas (assumptions)
• Δ (succedent): A sequence of formulas (conclusions)

Interpretation: From assumptions Γ, we can derive at least one formula in Δ

Notation: A₁, A₂, …, Aₙ ⊢ B₁, B₂, …, Bₘ

Intuition:

• Γ ⊢ Δ is true if: (A₁ ∧ A₂ ∧ … ∧ Aₙ) → (B₁ ∨ B₂ ∨ … ∨ Bₘ)
• Multiple conclusions represent disjunction

Axioms

Identity Axiom:

─────────
A ⊢ A

A formula proves itself

Weakening (Structural Rule):

Γ ⊢ Δ
──────────────
Γ, A ⊢ Δ

Can add assumptions without affecting conclusion

Logical Rules

Conjunction (∧)

Left Introduction (∧L):

Γ, A ⊢ Δ
──────────────
Γ, A ∧ B ⊢ Δ

If A proves Δ, then A ∧ B proves Δ

Right Introduction (∧R):

Γ ⊢ A    Γ ⊢ B
──────────────
Γ ⊢ A ∧ B

To prove A ∧ B, prove both A and B

Disjunction (∨)

Left Introduction (∨L):

Γ, A ⊢ Δ    Γ, B ⊢ Δ
──────────────────────
Γ, A ∨ B ⊢ Δ

If both A and B prove Δ, then A ∨ B proves Δ

Right Introduction (∨R):

Γ ⊢ A
──────────────
Γ ⊢ A ∨ B

To prove A ∨ B, prove A (or B)

Implication (→)

Left Introduction (→L):

Γ ⊢ A    Γ, B ⊢ Δ
──────────────────
Γ, A → B ⊢ Δ

To use A → B, prove A and assume B

Right Introduction (→R):

Γ, A ⊢ B
──────────────
Γ ⊢ A → B

To prove A → B, assume A and prove B

Negation (¬)

Left Introduction (¬L):

Γ ⊢ A
──────────────
Γ, ¬A ⊢ Δ

If A is provable, ¬A is contradictory

Right Introduction (¬R):

Γ, A ⊢
──────────────
Γ ⊢ ¬A

To prove ¬A, assume A and derive contradiction

Structural Rules

Weakening

Left Weakening (WL):

Γ ⊢ Δ
──────────────
Γ, A ⊢ Δ

Can add assumptions

Right Weakening (WR):

Γ ⊢ Δ
──────────────
Γ ⊢ Δ, A

Can add conclusions

Contraction

Left Contraction (CL):

Γ, A, A ⊢ Δ
──────────────
Γ, A ⊢ Δ

Duplicate assumptions can be merged

Right Contraction (CR):

Γ ⊢ Δ, A, A
──────────────
Γ ⊢ Δ, A

Duplicate conclusions can be merged

Exchange

Left Exchange (EL):

Γ, A, B, Γ' ⊢ Δ
──────────────────
Γ, B, A, Γ' ⊢ Δ

Order of assumptions doesn’t matter

Right Exchange (ER):

Γ ⊢ Δ, A, B, Δ'
──────────────────
Γ ⊢ Δ, B, A, Δ'

Order of conclusions doesn’t matter

Cut

Cut Rule:

Γ ⊢ A    Γ, A ⊢ Δ
──────────────────
Γ ⊢ Δ

If A is provable and A implies Δ, then Δ is provable

Significance: Cut represents transitivity of implication

Cut Elimination

Cut-Elimination Theorem

Theorem (Gentzen): Every proof in sequent calculus can be transformed into a cut-free proof

Significance:

• Provides normal form for proofs
• Enables proof analysis
• Fundamental for proof theory

Proof Transformation

Strategy: Replace cut with direct proof

Example:

Before (with cut):
Γ ⊢ A    Γ, A ⊢ Δ
──────────────────
Γ ⊢ Δ

After (cut-free):
Direct proof of Γ ⊢ Δ without intermediate A

Subformula Property

Property: In cut-free proofs, every formula in the proof is a subformula of the conclusion

Consequence: Limits the formulas that can appear in proofs

Application: Enables decision procedures for certain logics

First-Order Sequent Calculus

Universal Quantification (∀)

Left Introduction (∀L):

Γ, A[x/t] ⊢ Δ
──────────────────
Γ, ∀x A ⊢ Δ

Instantiate universal quantifier with term t

Right Introduction (∀R):

Γ ⊢ A[x/a]
──────────────────
Γ ⊢ ∀x A

Prove for arbitrary variable a (not in Γ or Δ)

Existential Quantification (∃)

Left Introduction (∃L):

Γ, A[x/a] ⊢ Δ
──────────────────
Γ, ∃x A ⊢ Δ

Assume for arbitrary variable a

Right Introduction (∃R):

Γ ⊢ A[x/t]
──────────────────
Γ ⊢ ∃x A

Prove with specific term t

Proof Examples

Example 1: Modus Ponens

Goal: Prove B from {A → B, A}

Proof:

A ⊢ A          B ⊢ B
─────────────────────  (→L)
A → B, A ⊢ B

Example 2: Hypothetical Syllogism

Goal: Prove A → C from {A → B, B → C}

Proof:

A ⊢ A          B ⊢ B          C ⊢ C
─────────────────────────────────────  (→L)
A → B, A ⊢ B    B → C, B ⊢ C
─────────────────────────────────────  (→L)
A → B, B → C, A ⊢ C
─────────────────────────────────────  (→R)
A → B, B → C ⊢ A → C

Example 3: De Morgan’s Law

Goal: Prove ¬(A ∧ B) ⊢ ¬A ∨ ¬B

Proof:

A ⊢ A    B ⊢ B
─────────────────  (∧R)
A, B ⊢ A ∧ B
─────────────────  (¬L)
¬(A ∧ B), A, B ⊢
─────────────────  (¬R)
¬(A ∧ B), A ⊢ ¬B
─────────────────  (∨R)
¬(A ∧ B), A ⊢ ¬A ∨ ¬B
─────────────────  (¬L)
¬(A ∧ B) ⊢ ¬A ∨ ¬B

Comparison with Other Systems

Sequent Calculus vs Natural Deduction

Sequent Calculus vs Resolution

Applications

Proof Theory

Cut Elimination: Fundamental theorem in proof theory Consistency Proofs: Proving consistency of formal systems Proof Analysis: Understanding structure of proofs

Automated Reasoning

Proof Search: Systematic search for proofs Theorem Provers: Some use sequent calculus Logic Programming: Related to SLD resolution

Computational Logic

Type Theory: Sequent calculus for type systems Linear Logic: Sequent calculus for resource-aware reasoning Modal Logic: Sequent calculus for modal logics

Glossary

Antecedent: Left side of sequent (assumptions)

Cut: Inference rule using intermediate formula

Cut Elimination: Removing cuts from proofs

Sequent: Expression Γ ⊢ Δ

Structural Rule: Rule about structure (weakening, contraction, exchange)

Subformula Property: Formulas in proof are subformulas of conclusion

Succedent: Right side of sequent (conclusions)

Practice Problems

Problem 1: Prove A ∧ B ⊢ B ∧ A using sequent calculus.

Solution:

A ⊢ A    B ⊢ B
─────────────────  (∧L)
A ∧ B ⊢ A    A ∧ B ⊢ B
─────────────────────────  (∧R)
A ∧ B ⊢ B ∧ A

Problem 2: Prove ⊢ A ∨ ¬A (law of excluded middle) using sequent calculus.

Solution:

A ⊢ A
─────────────────  (¬R)
⊢ A, ¬A
─────────────────  (∨R)
⊢ A ∨ ¬A

Problem 3: Prove A → (B → C) ⊢ (A ∧ B) → C using sequent calculus.

Solution:

A → (B → C), A, B ⊢ C
─────────────────────────  (→L)
A → (B → C), A ∧ B ⊢ C
─────────────────────────  (→R)
A → (B → C) ⊢ (A ∧ B) → C

Related Resources

• Sequent Calculus: https://en.wikipedia.org/wiki/Sequent_calculus
• Proof Theory: https://plato.stanford.edu/entries/proof-theory/
• Cut Elimination: https://en.wikipedia.org/wiki/Cut-elimination_theorem
• Gentzen: https://en.wikipedia.org/wiki/Gerhard_Gentzen
• Natural Deduction: https://en.wikipedia.org/wiki/Natural_deduction
• Formal Logic: https://plato.stanford.edu/entries/logic-classical/
• Structural Rules: https://en.wikipedia.org/wiki/Structural_rule
• Subformula Property: https://en.wikipedia.org/wiki/Subformula_property
• Linear Logic: https://en.wikipedia.org/wiki/Linear_logic
• Intuitionistic Logic: https://plato.stanford.edu/entries/logic-intuitionistic/
• Modal Logic: https://plato.stanford.edu/entries/logic-modal/
• Type Theory: https://plato.stanford.edu/entries/type-theory/
• Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant
• Automated Reasoning: https://en.wikipedia.org/wiki/Automated_reasoning
• Formal Verification: https://en.wikipedia.org/wiki/Formal_verification

Conclusion

Sequent calculus provides a symmetric, structural approach to formal reasoning that is particularly suited for theoretical analysis and automated reasoning. The cut-elimination theorem and subformula property provide powerful tools for understanding the nature of proofs and logical systems.

Understanding sequent calculus is essential for anyone working in proof theory, automated reasoning, or formal verification. Its elegant structure and theoretical properties make it a fundamental tool in mathematical logic and computer science.

The symmetry of sequent calculus—treating assumptions and conclusions uniformly—reveals deep insights into the nature of logical reasoning and computation.