Proof Analysis

Sara Negri University of Helsinki From Natural Deduction to Sequent Calculus

Introduction rules: Given through meaning explanation of logical constants; The “BHK-conditions” (for Brouwer-Heyting-Kolmogorov) give the explanations of logical operations of propositional logic in terms of direct provability of propositions

1. A direct proof of the proposition A&B consists of proofs of the propositions A and B.

2. A direct proof of the proposition A ∨ B consists of a proof of the proposition A or a proof of the proposition B.

3. A direct proof of the proposition A ⊃ B consists of a proof of the proposition B from the assumption that there is a proof of the proposition A.

4. A direct proof of the proposition ⊥ is impossible.

Here proof is an informal notion to be gradually replaced by the formal notion of derivability in a given system of rules. The BHK-explanation justi-

fies the introduction rules:

\begin{matrix}A & B \\ A&B \end{matrix} ^{&I}
{A \atop A ∨ B} ^{∨I1}  {B \atop A ∨ B} ^{∨I2}

[A] ; ⋮ . ; B ; A ⊃ B ^{⊃I}

No introduction rule for ⊥.

Elimination rules: Found from the introduction rules through an inversion principle.

Prawitz’ inversion principle: The conclusion of an elimination rule R with major premiss A ⋆ B is already contained in the assumptions used to derive A ⋆ B from the ⋆-introduction rules, together with the minor premisses of the rule.

Therefore nothing is gained if an introduction rule is followed by an elimination rule. Prawitz’ inversion principle justifies but does not uniquely determines the elimination rules.

(Our) Inversion principle: Whatever follows from the direct grounds for deriving a proposition, must follow from that proposition.

\begin{aligned}A&B & & [A, B] ; ⋮ . ; C \\ & C \end{aligned}^{&E}

If in a derivation the premisses A and B of the introduction rule have been derived and C has been derived from A and B, the derivation

\begin{matrix}\begin{matrix}⋮ . ; A & ⋮ . ; B \\ A&B \end{matrix} ^{&I} & [A, B] ; ⋮ . ; C \\ C \end{matrix}^{&E}

converts into a derivation of C without the introduction and elimination rules,

⋮ . ; A ⋮ . ; B ; ⋮ . ; C

Therefore, if &I is followed by &E, the derivation can be simplified.

\begin{aligned}A ∨ B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ & C \end{aligned}^{∨E}

\begin{matrix}⋮ . ; A ; A ∨ B ^{∨I1} & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ C \end{matrix}^{∨E}

converts to

⋮ . ; A ; ⋮ . ; C

If C follows from B, then it already follows from A.

\begin{aligned}A ⊃ B & & A & [B] ; ⋮ . ; C \\ & C \end{aligned}^{⊃E}

\begin{matrix}[A] ; ⋮ . ; B ; A ⊃ B ^{⊃I} & ⋮ . ; A & [B] ; ⋮ . ; C \\ C \end{matrix}^{⊃E}

converts to

⋮ . ; A ; ⋮ . ; B ; ⋮ . ; C

Grounds for deriving ⊥ are empty, so as a limiting case of the inversion principle get the rule of falsity elimination (“ex falso quodlibet”):

{⊥ \atop C}^{⊥E}

Rule of assumption: Permits to begin a derivation with any formula.

The leaves of a derivation tree are the assumptions. Open assumptions are neither conclusions nor discharged by any rule. Closed assumptions are discharged assumptions. Standard elimination rules obtained as special cases from the (general) elimination rules If C = A and C = B for &E, and C = B for ⊃ E, obtain:

{A&B \atop A} ^{&E1}  {A&B \atop B} ^{&E2}  \begin{matrix}A ⊃ B & A \\ B \end{matrix}^{⊃E}  (modusponens)

Why general elimination rules? In this course we use them to justify the sequent calculus rules. Much deeper reasons will be presented by Jan von Plato next week.

By making explicit the derivability relation we can write a derivation of C from assumptions Γ as

Γ ⊢ C

thus the rules of natural deduction are formulated is a system known as Natural deduction in sequent calculus style for instance

\begin{matrix}Γ ⊢ A & Δ ⊢ B \\ Γ ∪ Δ ⊢ A&B \end{matrix} ^{&I}

\begin{aligned}Γ ⊢ A ∨ B & Δ ∪ \{A\} ⊢ C & Θ ∪ \{B\} ⊢ C \\ & Γ ∪ Δ ∪ Θ ⊢ C \end{aligned} ^{∨E}

Sequent calculus^{a} has notation for keeping track of open assumptions; rules are local: Each formula C has the open assumptions Γ it depends on listed on the same line

Γ ⇒ C

Sequent calculus = formal theory of the derivability relation. In Γ ⇒ C, the left side Γ is called the antecedent and C the succedent. In Gentzen’s original formulation of 1934–35, the assumptions Γ, Δ, Θ were finite sequences, or lists as we would now say. Gentzen had rules permitting the exchange of order of formulas in a sequence.

aUse of the word “sequent” as a noun was begun by Kleene. His Introduction to Metamathematics of 1952 (p.

441) explains the origin of the term as follows:“Gentzen says ‘Sequenz’, which we translate as ‘sequent’, because we have already used ‘sequence’ for any succession of objects, where the German is ‘Folge’.” This is the standard terminology now; Kleene’s usage has even been adopted to some other languages. But Mostowski (1965) for example uses the literal translation “sequence.”

We consider assumptions finite multisets, that is, lists with multiplicity but no order. Rules of natural deduction only show the active formulas, remaining open assumptions are left implicit. Assumptions can be made explicit, instead of

\begin{matrix}A & B \\ A&B \end{matrix} ^{&I}

write

\begin{matrix}Γ ⋮ . ; A & Δ ⋮ . ; B \\ A&B \end{matrix}^{&I}

but the dots are informal.

The introduction rules of natural deduction become right rules of sequent calculus, where a comma replaces set-theoretical union:

\begin{matrix}Γ ⇒ A & Δ ⇒ B \\ Γ, Δ ⇒ A&B \end{matrix} ^{R&}
{A, Γ ⇒ B \atop Γ ⇒ A ⊃ B} ^{R⊃}
{Γ ⇒ A \atop Γ ⇒ A ∨ B} ^{R∨_{1}}
{Γ ⇒ B \atop Γ ⇒ A ∨ B} ^{R∨_{2}}

The formula with the connective in a rule is the principal formula of that rule and its components in the premisses the active formulas. The Greek letters denote possible additional assumptions that are not active in a rule; They are called the contexts of the rules.

The elimination rules of natural deduction correspond to left rules of sequent calculus.

{A, B, Γ ⇒ C \atop A&B, Γ ⇒ C} ^{L&}
\begin{matrix}A, Γ ⇒ C & B, Δ ⇒ C \\ A ∨ B, Γ, Δ ⇒ C \end{matrix} ^{L∨}
\begin{matrix}Γ ⇒ A & B, Δ ⇒ C \\ A ⊃ B, Γ, Δ ⇒ C \end{matrix} ^{L⊃}

Is this enough? No! Rules of natural deduction do not give complete instructions to draw derivations. In particular:

1. The same formula can act as assumption and conlcusion in a derivation

[A]^{1.} ; A ⊃ A^{⊃I,1.}

2. It is possible to discharge assumptions which have been not made (vacuous discharge)

\begin{matrix}[A]^{1.} ; B ⊃ A & ⊃I \\ A ⊃ (B ⊃ A) \end{matrix}^{⊃I,1.}

3. It is possible to discharge more occurrences of the same formula at once (multiple discharge)

\begin{matrix}\begin{matrix}\begin{matrix}[A ⊃ (A ⊃ B)]^{2.} & [A]^{1.} \\ A ⊃ B \end{matrix}^{⊃E} & [A]^{1.} \\ B \end{matrix} & ⊃E \\ A ⊃ B \end{matrix}_{⊃I,1.} ; (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)_{⊃I,2.}

4. It is possible to replace an assumption in a derivation with a derivation of that formula and obtain a derivation (substitution)

Γ, Δ ⋮ . ; A ; ⋮ . ; C

Structural rules: sequent calculus rules corresponding to the natural deduction construction principles 2–4 (sometimes also 1 is included) Weakening introduces an extra assumption in the antecedent:

{Γ ⇒ C \atop A, Γ ⇒ C}^{Wk}

Example 2 in sequent calculus becomes:

\begin{matrix}{A ⇒ A \atop A, B ⇒ A} & Wk \\ A ⇒ B ⊃ A \end{matrix}_{R⊃} ; ⇒ A ⊃ (B ⊃ A)_{R⊃}

Corresponds to vacuous discharge in natural deduction Contraction:

{A, A, Γ ⇒ C \atop A, Γ ⇒ C}^{Ctr}

\begin{matrix}A ⇒ A & \begin{matrix}A ⇒ A & B ⇒ B \\ A ⊃ B, A ⇒ B \end{matrix} ^{L⊃} \\ A ⊃ (A ⊃ B), A, A ⇒ B \end{matrix}_{L⊃} ; A ⊃ (A ⊃ B), A ⇒ B_{Ctr} ; A ⊃ (A ⊃ B) ⇒ A ⊃ B_{R⊃} ; ⇒ (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)_{R⊃}

Corresponds to multiple discharge in natural deduction If assumptions are treated as sets instead of multisets, contraction built into the system and cannot be expressed as a distinct rule.

Cut:

\begin{matrix}Γ ⇒ A & A, Δ ⇒ C \\ Γ, Δ ⇒ C \end{matrix}^{Cut}

Explanation: substitution and non-normal instances of elimination rules in natural deduction; breaking proofs into lemmas. The sequent calculus G0i is now completely determined.

Classical propositional logic is obtained by adding to the rules of intuitionistic logic a rule of excluded middle

\begin{aligned}[A] ; ⋮ . ; C & & [∼A] ; ⋮ . ; C \\ & C \end{aligned}^{Em}

Both A and ∼ A are discharged at the inference. The law of excluded middle, A∨ ∼ A, is derivable with the rule:

\begin{matrix}{[A] \atop A∨ ∼A}^{∨I1} & {[∼A] \atop A∨ ∼A}^{∨I2} \\ A∨ ∼A \end{matrix}_{Em}

The rule of excluded middle is a generalization of the rule of indirect proof (“reductio ad absurdum”),

[∼A] ; ⋮ . ; ⊥ ; A^{Raa}

Sequent Calculus and Proof Search

Rules of sequent calculus can have independent or shared contexts. For instance the right rule for conjunction with independent contexts is

\begin{matrix}Γ ⇒ A & Δ ⇒ B \\ Γ, Δ ⇒ A&B \end{matrix}

The two styles are equivalent in the presence of the structural rules (exercise). Shared contexts add determinism to proof search. With the cut rule the subformula property is no longer guaranteed. Thus one of the main tasks of structural proof theory is the design of sequent where cut is an eliminable or admissible rule. Contraction can be as “bad” as cut, as concerns a root-first search for a derivation of a given sequent: Formulas in antecedents can be multiplied with no end.

Weakening is easily avoided: modify the axiom A ⇒ A to the form A, Γ ⇒ A. Classical logic: The rule

\begin{matrix}A, Γ ⇒ C & ∼ A, Γ ⇒ C \\ Γ ⇒ C \end{matrix}

is not good for proof search purposes. Alternatively can extend notion of sequent to multisuccedent (thus moving away from the intuition of natural deduction) Sequents are expression of the form

Γ ⇒ Δ

where Γ and Δ are both multisets of formulas. Excluded middle is derivable

{A ⇒ A, ⊥ \atop ⇒ A, ∼ A} ; ⇒ A∨ ∼ A

Intuitionistic system obtained as a special case of the classical system (uniform formalism) by restriction on the context in implication rules.

Gentzen (1934–35): denotational interpretation of multisuccedent sequents: The conjunction of formulas in Γ implies the disjunction of formulas in Δ. Operational interpretation of single succedent sequents Γ ⇒ C (from assumptions Γ, conclusion C can be derived) does not extend to multiple succedents. Gentzen (1938): Multisuccedent calculus = natural representation of the division into cases often found in mathematical proofs. Γ open assumptions, Δ open cases. Logical rules change and combine open assumptions and cases: L& replaces the open assumptions A, B by the open assumption A&B; dual multisuccedent rule R∨ changes the open cases A, B into the open case A ∨ B, ... One case = ordinary conclusion from open assumptions. Γ ⇒ = empty case = impossibility.

Invertible rules are needed for decomposing root first a sequent to be proved. So, for instance, the single rule

{A, B, Γ ⇒ Δ \atop A&B, Γ ⇒ Δ}

is better than the two equivalent rules

{A, Γ ⇒ Δ \atop A&B, Γ ⇒ Δ}  {B, Γ ⇒ Δ \atop A&B, Γ ⇒ Δ}

Summing up the desiderata for our sequent calculus are: multi-succedent, with context sharing rules, admissible structural rules, invertible logical rules. The calculus G3c.

Theorem: Height-preserving inversion. All rules of G3cp are invertible, with height-preserving inversion. E.g.: If ⊢_{n} Γ ⇒ Δ, A&B, then ⊢_{n} Γ ⇒ Δ, A and ⊢_{n} Γ ⇒ Δ, B. Proof by induction on n: If Γ ⇒ Δ, A&B is an axiom or conclusion of L⊥, then, A&B not being atomic, also Γ ⇒ Δ, A and Γ ⇒ Δ, B are axioms or conclusions of L⊥. Assume height preserving inversion up to height n, and let ⊢_{n+1} Γ ⇒ Δ, A&B. There are two cases: If A&B is not principal in the last rule, it has one or two premisses Γ′ ⇒ Δ′, A&B and Γ′′ ⇒ Δ′′, A&B, of derivation height ⩽ n, so by inductive hypothesis, ⊢_{n} Γ′ ⇒ Δ′, A and ⊢_{n} Γ′ ⇒ Δ′, B and ⊢_{n} Γ′′ ⇒ Δ′′, A and ⊢_{n} Γ′′ ⇒ Δ′′, B. Now apply the last rule to these premisses to conclude Γ ⇒ Δ, A and Γ ⇒ Δ, B with a height of derivation ⩽ n + 1. If A&B is principal in the last rule, the premisses Γ ⇒ Δ, A and Γ ⇒ Δ, B have derivations of height ⩽ n.

Admissibility of structural rules

{Γ ⇒ Δ \atop A, Γ ⇒ Δ}^{LW} {Γ ⇒ Δ \atop Γ ⇒ Δ, A}^{RW}
{A, A, Γ ⇒ Δ \atop A, Γ ⇒ Δ}^{LC} {Γ ⇒ Δ, A, A \atop Γ ⇒ Δ, A}^{RC}

Theorem: Height-preserving weakening. If ⊢_{n} Γ ⇒ Δ, then ⊢_{n} A, Γ ⇒ Δ. If ⊢_{n} Γ ⇒ Δ, then ⊢_{n} Γ ⇒ Δ, A. Theorem: Height-preserving contraction. If ⊢_{n} C, C, Γ ⇒ Δ, then ⊢_{n} C, Γ ⇒ Δ. If ⊢_{n} Γ ⇒ Δ, C, C, then ⊢_{n} Γ ⇒ Δ, C. Proof by simultaneus induction on the height of the derivation for left and right contraction, using height-preserving invertivility of the rules.

Theorem The rule of cut,

Γ ⇒ Δ, D D, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ, Δ′ Cut

is admissible in G3cp. Details of the proof in the book. Advantage of a contraction-free calculus: no need of multicut. (However see Jan von Plato’s Cut elimination without multicut).

Corollary Each formula in the derivation of Γ ⇒ Δ in G3cp is a subformula of Γ, Δ.

Corollary: Consistence The sequent ⇒ is not derivable. By admissibility of weakening, if Γ ⇒ is derivable, then also Γ ⇒ ⊥ is derivable. The converse is obtained by applying cut to Γ ⇒ ⊥ and ⊥ ⇒ , thus, an empty succedent behaves like ⊥.