Sequent Calculus

The sequent calculus is a fundamental framework in mathematical logic that provides a systematic way to represent and manipulate logical deductions. Developed by Gerhard Gentzen in the 1930s, it serves as one of the cornerstone formalisms in proof theory.

Core Concepts

Sequents

A sequent is the basic unit of reasoning in sequent calculus, typically written as:

Γ ⊢ Δ

where:

• Γ (antecedent) is a set of formulas representing assumptions
• ⊢ is the turnstile symbol indicating logical entailment
• Δ (succedent) is a set of formulas representing conclusions

Inference Rules

The calculus is built around two types of rules:

1. Structural Rules

   • Weakening
   • Contraction
   • Cut Rule

2. Logical Rules

   • Left rules (operating on antecedent)
   • Right rules (operating on succedent)

Properties

Cut Elimination

One of the most significant results in proof theory is Gentzen's Cut Elimination Theorem, which shows that the cut rule is admissible in sequent calculus. This has important implications for:

• Proof Normalization
• Decidability of logical systems
• Consistency proofs

Symmetry

The sequent calculus exhibits a remarkable symmetry between:

• Introduction and elimination rules
• Left and right rules
• Classical Logic and Intuitionistic Logic

Applications

1. Automated Theorem Proving

   • Foundation for Resolution-based proof search
   • Basis for Logic Programming languages

2. Type Theory

   • Connections to Curry-Howard Correspondence
   • Implementation of Type Inference algorithms

3. Programming Language Theory

   • Substructural Logic
   • Linear Logic

Historical Context

The development of sequent calculus was motivated by Gentzen's search for a more natural proof system than Hilbert System calculi. It has since become a central tool in:

• Proof Theory
• Mathematical Logic
• Computational Logic

Variants

Several important variants have been developed:

• G3 Calculus
• Linear Sequent Calculus
• Modal Sequent Calculus
• Intuitionistic Sequent Calculus

Relationship to Other Systems

Sequent calculus maintains important connections to:

• Natural Deduction (through systematic translations)
• Lambda Calculus (via Curry-Howard)
• Category Theory (through categorical semantics)

The system continues to influence modern developments in logic, computer science, and the foundations of mathematics, serving as a bridge between syntactic and semantic approaches to logical reasoning.