Natural Deduction and Sequent Calculus

Notes for CS 358, Spring 1995

April 10–12 Lectures

1 Natural Deduction Rules

In natural deduction, a proof is a finite tree, with leaves labeled by logic formulas and internal nodes labeled by instances of proof rules (including the antecedent and consequent formulas). In writing the rules, we use the notation

⋮ ; A

to indicate a deduction of formula A, i.e., a proof tree with A at the root.

A leaf of a proof tree may be an active or discharged assumption. The word hypothesis is sometimes used for “active assumption.” We have fully proved a formula A only when we have constructed a proof tree with A at the root and all assumptions discharged.

The (→ Intro) rule is written

(→ Intro)  \frac{[A] ; ⋮ ; B}{A → B}

where the square brackets [ ] around the hypothesis mean that one effect of the rule is to change A from an active to discharged assumption. In other words, while the proof

[A] ; ⋮ ; B

depends on active assumption A, the proof of A → B using (→ Intro) does not rely on the assumption of A. For example, here is a complete proof of the formula A → A:

\frac{[A]}{A → A}

This proof is constructed by assuming A. Then we discharge the assumption to get a proof of A → A.

There are various conventions that we might adopt regarding hypotheses that do are not used in the proof (and therefore wouldn’t appear as part of a connected tree-shaped graph) and multiple occurrences of the same formula as hypotheses. For concreteness, let us agree that any formula could be considered as vacuously appearing in any proof, and that discharging an assumption A means that we may simultaneously discharge as many assumptions of A as desired. For example, we can discharge the “non-occurring” assumption of B as follows to get a proof of B → A depending on the hypothesis A.

\frac{A}{B → A}

If we then discharge the assumption A, we have a proof of A → B → A.

Natural deduction rules for →, ∧, ∀

Hypothesis  A

Introduction  \frac{⋮ ; A ⋮ ; B}{A ∧ B}  \frac{[A] ; ⋮ ; B}{A → B}  \frac{⋮ ; A}{∀x. A}

Elimination  \frac{⋮ ; A ∧ B}{A}  \frac{⋮ ; A ∧ B}{B}  \frac{⋮ ; A → B ⋮ ; A}{B}  \frac{⋮ ; ∀x. A}{[t/x]A}

Exercise: Write a proof of (A → B) → A → A → B.

2 Sequent Calculus

A sequent is an expression Γ ⊢ Σ, where Γ and Σ are finite lists of formulas, Γ = A_{1}, …, A_{k}, Σ = B_{1}, …, B_{ℓ}. Intuitively, A_{1}, …, A_{k} ⊢ B_{1}, …, B_{ℓ} means that the conjunction A_{1} ∧ … ∧ A_{k} implies the disjunction B_{1} ∨ … ∨ B_{ℓ}. However, the exact form of conjunction, disjunction and implication involved will depend on the kind of logic we are defining. In a sequent calculus presentation of classical logic, Γ ⊢ Σ may be understood using classical conjunction, disjunction and implication, while in linear logic, we must use “linear” forms of conjunction, disjunction and implication.

Structural and identity rules

Exch. Left \frac{Γ_{1}, A, B, Γ_{2} ⊢ Σ}{Γ_{1}, B, A, Γ_{2} ⊢ Σ}  \frac{Γ ⊢ Σ_{1}, A, B, Σ_{2}}{Γ ⊢ Σ_{1}, B, A, Σ_{2}}  Exch. Right

Weak. Left  \frac{Γ ⊢ Σ}{Γ, A ⊢ Σ}  \frac{Γ ⊢ Σ}{Γ ⊢ Σ, B}  Weak. Right

Contr. Left  \frac{Γ, A, A ⊢ Σ}{Γ, A ⊢ Σ}  \frac{Γ ⊢ Σ, B, B}{Γ ⊢ Σ, B}  Contr. Right

Identity  \overline{A ⊢ A}  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2}, A ⊢ Σ_{2}}{Γ_{1}, Γ_{2} ⊢ Σ_{1}, Σ_{2}} Cut

Intuitionistic case

The sequent rules for intuitionistic logic are obtained from the classical ones by restricting the list of formulas on the right to a single formula. This makes it impossible to apply structural rules on the right.

Logical rules for negation, conjunction and disjunction

¬ Left  \frac{Γ ⊢ Σ, B}{Γ, ¬B ⊢ Σ}  \frac{Γ, A ⊢ Σ}{Γ ⊢ ¬AΣ_{2}}  ¬ Right

∧ Left \frac{Γ, A ⊢ Σ}{Γ, A ∧ B ⊢ Σ} \frac{Γ, B ⊢ Σ}{Γ, A ∧ B ⊢ Σ}  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2} ⊢ B, Σ_{2}}{Γ_{1}, Γ_{2} ⊢ (A ∧ B), Σ_{1}, Σ_{2}}  ∧ Right

∨ Left \frac{Γ_{1}, A ⊢ Σ_{1}  Γ_{2}, B ⊢ Σ_{2}}{Γ_{1}, Γ_{2}, (A ∨ B) ⊢ Σ_{1}, Σ_{2}}  \frac{Γ ⊢ A, Σ}{Γ ⊢ (A ∨ B), Σ}  \frac{Γ ⊢ B, Σ}{Γ ⊢ (A ∨ B), Σ} ∨ Right

In the intuitionistic case, we need to reformulate ∨ Left so the rule does not produce a sequent with more than one formula on the right.

∨ Left \frac{Γ_{1}, A ⊢ C  Γ_{2}, B ⊢ C}{Γ_{1}, Γ_{2}, (A ∨ B) ⊢ C}

Implication

→ Left \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2}, B ⊢ Σ_{2}}{Γ_{1}, Γ_{2}, (A → B) ⊢ Σ_{1}, Σ_{2}}  \frac{Γ, A ⊢ B, Σ}{Γ ⊢ (A → B), Σ} → Right

Quantification

∀ Left \frac{Γ, [t/x]A ⊢ Σ}{Γ, ∀x. A ⊢ Σ}  \frac{Γ ⊢ A, Σ}{Γ ⊢ ∀x. A, Σ} ∀ Right

∃ Left \frac{Γ, A ⊢ Σ}{Γ, ∃x. A ⊢ Σ}  \frac{Γ ⊢ [t/x]A, Σ}{Γ ⊢ ∃x. A, Σ} ∃ Right

In ∀ Right and ∃ Left, the variable x must not be free in Γ of Σ.

Proof strategy

Sequent calculus lends itself to both “forward-directed” proofs, starting from axioms and deriving consequences, and “backward-directed” proof search. The places where “guessing” is involved in proof search are (i) guessing which formula in a sequent is to be manipulated (analyzed), (ii) guessing whether Cut is to be used, since this is independent of the form of any formulas in the sequent, (iii) guessing the cut-formula, if Cut is assumed to be the last rule in the proof, (iv) guessing terms to substitute for quantified variable in rules ∀ Left and ∃ Right.

Cut elimination

There is a proof-transformation procedure that takes any proof and successively re-orders rules so that all occurrences of cut are eventually removed. This procedure may increase the size of the proof very exponentially. However, the increase in proof size may be traced to the use of contraction.

For every rule except Cut, the formulas in the premise are subformulas of the formulas in the conclusion (assuming we regard [t/x]A as a subformula of ∃x. A and ∀x. A). Since every provable formula has a Cut-free proof, this subformula property gives us a way of analyzing the set of provable formulas. This idea was used by Gentzen in the 1930’s to prove the consistency of Peano arithmetic and other systems.

Example Here is part of a proof of Pearce’s Law, ((A → B) → A) → A, in classical sequent calculus.

\underline{⊢ A → B, A  A ⊢ A} (→ Left)
\underline{(A → B) → A ⊢ A, A} (Contr. Right)
\underline{(A → B) → A ⊢ A} (→ Right)
((A → B) → A) → A

Exercises

1. Complete the proof above by proving ⊢ A → B, A.

2. Use the fact that every provable formula has a cut-free proof to show that Pearce’s Law is not provable in the intuitionistic sequent calculus.