About Sequent Calculus
Sequent calculus, introduced by Gerhard Gentzen in 1934, is a formal system for deriving valid logical sequents. A sequent has the form Γ ⊢ Δ, where Γ (the antecedent) and Δ (the consequent) are lists of formulas. Intuitively, Γ ⊢ Δ means "if all formulas in Γ are true, then at least one formula in Δ is true."
Sequent Notation
- Γ ⊢ Δ: The turnstile ⊢ separates antecedent from consequent
- Antecedent (Γ): Comma-separated formulas on the left (assumptions)
- Consequent (Δ): Comma-separated formulas on the right (conclusions)
- Empty sides: ⊢ Δ means "Δ is provable"; Γ ⊢ means "Γ is contradictory"
Structural Rules
These rules manipulate the structure of sequents without regard to logical connectives:
- Weakening: Add a formula to either side (Γ ⊢ Δ implies Γ,A ⊢ Δ)
- Contraction: Merge duplicate formulas (Γ,A,A ⊢ Δ becomes Γ,A ⊢ Δ)
- Exchange: Reorder formulas (Γ,A,B,Π ⊢ Δ becomes Γ,B,A,Π ⊢ Δ)
Logical Rules
Each logical connective has left and right introduction rules:
- ∧ Left: From Γ,A ⊢ Δ infer Γ,A∧B ⊢ Δ (similarly for B)
- ∧ Right: From Γ ⊢ Δ,A and Γ ⊢ Δ,B infer Γ ⊢ Δ,A∧B
- ∨ Left: From Γ,A ⊢ Δ and Γ,B ⊢ Δ infer Γ,A∨B ⊢ Δ
- ∨ Right: From Γ ⊢ Δ,A infer Γ ⊢ Δ,A∨B (similarly for B)
- → Left: From Γ ⊢ Δ,A and Γ,B ⊢ Δ infer Γ,A→B ⊢ Δ
- → Right: From Γ,A ⊢ Δ,B infer Γ ⊢ Δ,A→B
- ¬ Left: From Γ ⊢ Δ,A infer Γ,¬A ⊢ Δ
- ¬ Right: From Γ,A ⊢ Δ infer Γ ⊢ Δ,¬A
The Cut Rule
The cut rule is a powerful inference rule that allows intermediate lemmas:
- Cut: From Γ ⊢ Δ,A and Γ,A ⊢ Δ infer Γ ⊢ Δ
- The formula A is called the cut formula
- Cut represents "if we can prove A and use A to prove the goal, we can prove the goal directly"
- While admissible, cut can make proofs more compact but obscures the logical structure
Cut Elimination
Gentzen's Hauptsatz (main theorem) states that any provable sequent has a cut-free proof. Cut elimination has profound consequences:
- Subformula property: Cut-free proofs only use subformulas of the conclusion
- Consistency: Cut elimination proves consistency of logical systems
- Decidability: For some logics, cut-free proofs are finite and searchable
- Semantic transparency: Cut-free proofs reveal the logical structure directly
The Identity Axiom
The base case for proof trees is the identity axiom: A ⊢ A for any formula A. This represents the trivial truth that any proposition implies itself.
Reading Proof Trees
Sequent calculus proofs are trees where:
- Leaves are axioms (A ⊢ A)
- Internal nodes are sequents derived by rules
- Edges are labeled with the rule name
- Root is the sequent to be proved
Proofs are constructed bottom-up: start with the goal sequent and apply rules backward until reaching axioms.
Historical Context
Gerhard Gentzen introduced sequent calculus (Sequenzenkalküll) in 1934 alongside natural deduction. While natural deduction mirrors informal reasoning, sequent calculus is more symmetric and better suited for proof theory. Gentzen used it to prove the consistency of Peano arithmetic (relative to a stronger system) and to establish cut-elimination, which became a cornerstone of structural proof theory.
Notation Guide
Use these symbols when entering formulas:
- ∧ for conjunction (AND) - type & or AND
- ∨ for disjunction (OR) - type | or OR
- → for implication (IF...THEN) - type -> or =>
- ¬ for negation (NOT) - type ~ or NOT
Separate multiple formulas with commas: P, Q, R