Uppsala University Period 1/2 Matematiska Institutionen Ht 1998 Anton Setzer

“Constructive Mathematics and Lambda Calculus”

A Sequent Version of the Natural Deduction Calculus

The natural deduction calculus has the disadvantage that it is difficult to prove proof theoretical lemmata about it in a completely formal way. Instead we will use a sequent-style version of the natural deduction calculus. The difference is only that we attach to every formula in a derivation the set of assumptions currently active.

Definition A sequent is an object of the form Γ⇒A, where Γ is a finite set of formulas, A is a formula. In the following Γ, Δ, possibly with subscripts and indices, denote finite sets of formulas. (There are classical sequent calculi, which derive objects Γ⇒Δ, which are then called sequents as well. Often, Γ is called a sequent as well). We define Γ, Δ := Γ ∪ Δ and, if A is a formula, Γ, A := Γ ∪ {A}. Note that in an expression Γ, A A might be already an element of Γ.

Definition of the rules of sequent-style natural deduction calculi. ((Ass), (Weak) (Stab), (EFQ) stand for assumption rule, weakening rule, stability rule and ex falsum quod libet; rules with I stand for introduction and rules with E for elimination rules — sometimes we write Intro instead of I, Elim instead of E; FV(Γ) is the union of the set of free variables in all formulas in Γ; ¬A is defined as A→⊥):

(Ass) A⇒A  (Weak) \frac{Γ⇒B}{Γ, A⇒B}

(∧-I)  \frac{Γ⇒A  Γ⇒B}{Γ⇒A ∧ B}  (∧-E_{1}) \frac{Γ⇒A ∧ B}{Γ⇒A}

(∧-E_{2}) \frac{Γ⇒A ∧ B}{Γ⇒B}

(∨-I_{1}) \frac{Γ⇒A}{Γ⇒A ∨ B}  (∨-I_{2}) \frac{Γ⇒B}{Γ⇒A ∨ B}

(∨-E) \frac{Γ⇒A ∨ B  Γ, A⇒C  Γ, B⇒C}{Γ⇒C}

(→-I) \frac{Γ, A⇒B}{Γ⇒A→B}  (→-E) \frac{Γ⇒A→B  Γ⇒A}{Γ⇒B}

(∀-I)  \frac{Γ⇒A}{Γ⇒∀x.A}  (x ∉ FV(Γ))

(∀-E) \frac{Γ⇒∀x.A}{Γ⇒A[x := t]}

(∃-I)  \frac{Γ⇒A[x := t]}{Γ⇒∃x.A}

(∃-E) \frac{Γ⇒∃x.A Δ, A⇒C}{Γ, Δ⇒C} (x ∉ FV(Δ) ∪ FV(C))

(Stab) \frac{Γ, ¬A⇒⊥}{Γ⇒A}  (EFQ) \frac{Γ⇒⊥}{Γ⇒A}

Definition

(a) The rules of the sequent-style natural deduction calculus for minimal logic (MQC) are all the rules before except of (Stab) and (EFQ).

(b) The rules of the sequent-style natural deduction calculus for intuitionistic logic (IQC) are the rules of minimal logic plus (EFQ).

(c) The rules of the sequent-style natural deduction calculus for classical logic (CQC) are the rules of minimal logic plus (Stab).

Lemma

(a) If in natural deduction for minimal/intuitionistic/classical logic we can derive A from assumptions Γ, then we can derive in the corresponding sequent-style calculus Γ⇒A.

(b) If in the sequent-style natural deduction calculus for minimal/inuitionistic/classical logic we can derive Γ⇒A, then from some (not necessarily all) assumption in Γ we can derive in the corresponding ordinary natural deduction calculus A.

Definition We write Γ⊢_{m}A, (Γ⊢_{i}A, Γ⊢_{c}A) for Γ⇒A is provable in minimal (intuitionistical, classical) logic.