Chapter 3: Sequent calculus for classical logic

There are many formulations of sequent calculi. Historically, Gentzen first found systems of natural deduction for intuitionistic and classical logic, denoted NJ and NK, respectively, but was not able to find a normal form for derivations in NK. To this purpose, he developed the classical sequent calculus LK that had sequences of formulas also in the succedent part. In our notation, such multisuccedent sequents are written Γ ⇒ Δ, where both Γ and Δ are multisets of formulas. Gentzen (1934–35) gives what is now called the denotational interpretation of multisuccedent sequents: The conjunction of formulas in Γ implies the disjunction of formulas in Δ. But the operational interpretation of single succedent sequents Γ ⇒ C, as expressing that from assumptions Γ, conclusion C can be derived, does not extend to multiple succedents.

Gentzen’s somewhat later explanation of the multisuccedent calculus is that it is a natural representation of the division into cases often found in mathematical proofs (1938, p. 21). Proofs by cases are met in natural deduction in disjunction elimination, where a common consequence C of the two disjuncts A and B is sought, permitting to conclude C from A∨B. There is a generalization of natural deduction into a multiple conclusion calculus that includes this mode of inference. Gentzen suggests such a multiple conclusion rule for disjunction (ibid., p. 21):

{A ∨ B \atop A B}

Disjunction elimination corresponds to arriving at the same formula C along both downward branches.

Along these lines, we may read a sequent Γ ⇒ Δ as consisting of the open assumptions Γ and the open cases Δ. Logical rules change and combine open assumptions and cases: L& replaces the open assumptions A, B by the open assumption A&B, and there will be a dual multisuccedent rule R∨ that changes the open cases A, B into the open case A ∨ B, and so on. If there is just one case, we have the situation of an ordinary conclusion from open assumptions. Finally, we can have an empty case representing impossibility, with nothing on the right of the sequent arrow.

In an axiomatic formulation, classical logic is obtained from intuitionistic logic by the addition of the principle of excluded third to the logical axioms (Gentzen 1934–35, p. 117). In natural deduction, one adds that derivations may start from instances of the law A ∨ ∼ A (Gentzen, ibid., p. 81). Alternatively, one may add either the rule \frac{∼∼A}{A} (Gentzen, ibid.) or the rule of indirect proof (Prawitz 1965, p. 20):

∼A ; ⋮ . ; ⊥ ; A

In sequent calculus, in the words of Gentzen (p. 80), “the difference is characterized by the restriction on the succedent,” that is, a calculus for intuitionistic logic is obtained from the classical calculus LK by restricting the succedent to be one formula. The essential point here is that the classical R⊃ rule,

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

becomes

{A, Γ ⇒ B \atop Γ ⇒ A ⊃ B}

An instance of the former is

{A ⇒ A, ⊥ \atop ⇒ A, A ⊃ ⊥}

By the multisuccedent R∨ rule, the cases A, A ⊃ ⊥ can be replaced by the disjunction A ∨ (A ⊃ ⊥), a derivation of the law of excluded middle that gets barred in the intuitionistic calculus.

It is, however, possible to give an operational interpretation to a restricted multisuccedent calculus corresponding precisely to intuitionistic derivability, as will be shown in Chapter 5. Therefore, it is not the feature of having a multiset as a succedent that leads to classical logic, but the unrestricted R⊃ rule. If only one formula is permitted in the succedent of its premiss, comma on the right can be interpreted as an intuitionistic disjunction.

3.1. An invertible classical calculus

We give the rules for a calculus G3cp of classical propositional logic and show that they are all invertible. Then we describe a variant of the calculus with negation as a primitive connective.

(a) The calculus G3cp: Sequents are of the form Γ ⇒ Δ where Γ and Δ are finite multisets, and Γ and Δ can be empty. In contrast to the single succedent calculus, it is possible to have sequents of form Γ ⇒ and even ⇒ . One of the admissible structural rules of the multisuccedent calculus will be right weakening, from which it follows that if Γ ⇒ is derivable, then also Γ ⇒ ⊥ is derivable.

G3cp

Logical axiom:

P, Γ ⇒ Δ, P

Logical rules:

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

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

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

The logical rules display the perfect duality of left and right rules for conjunction and disjunction, of which only the duality L∨ – R& could be observed in the intuitionistic calculus. Here there is only one R∨ rule, and it is invertible, and also the L⊃ rule is invertible, with no need to repeat the principal formula in the left premiss, which has profound consequences for the structure of derivations, and for proof search.

Theorem 3.1.1: Height-preserving inversion. All rules of G3cp are invertible, with height-preserving inversion.

Proof: For L&, L∨ and the second premiss of L⊃, the proof goes through as in lemma 2.3.5, with Δ in place of C. We proceed from there with a proof by induction on height of derivation:

If the endsequent is A ⊃ B, Γ ⇒ Δ with A ⊃ B not principal, the last rule has one or two premisses A ⊃ B, Γ′ ⇒ Δ′ and A ⊃ B, Γ′′ ⇒ Δ′′, of derivation height ⩽ n, so by inductive hypothesis, Γ′ ⇒ Δ′, A and Γ′′ ⇒ Δ′′, A have derivations of height ⩽ n: Now apply the last rule to these premisses to conclude Γ ⇒ Δ, A with height of derivation ⩽ n + 1.

If A ⊃ B is principal in the last rule, the premiss Γ ⇒ Δ, A has a derivation of height ⩽ n.

We now prove invertibility of the right rules:

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.

If Γ ⇒ Δ, A ∨ B is an axiom or conclusion of L⊥, then, A ∨ B not being atomic, also Γ ⇒ Δ, A, B is an axiom or conclusion of L⊥. Assume height preserving inversion up to height n, and let ⊢_{n+1} Γ ⇒ Δ, A ∨ B. There are again 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, B and ⊢_{n} Γ′′ ⇒ Δ′′, A, B. Now apply the last rule to these premisses to conclude Γ ⇒ Δ, A, B with a height of derivation ⩽ n + 1.

If A ∨ B is principal in the last rule, the premiss Γ ⇒ Δ, A, B has a derivation of height ⩽ n.

If Γ ⇒ Δ, A ⊃ B is an axiom or conclusion of L⊥, then, A ⊃ B not being atomic, also A, Γ ⇒ Δ, B is an axiom or conclusion of L⊥. Assume height preserving inversion up to height n, and let ⊢_{n+1} Γ ⇒ Δ, A ⊃ B. As above, 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, Γ′ ⇒ Δ′, B and ⊢_{n} A, Γ′′ ⇒ Δ′′, B. Now apply the last rule to these premisses to conclude A, Γ ⇒ Δ, B with a derivation of height ⩽ n + 1.

If A ⊃ B is principal in the last rule, the premiss A, Γ ⇒ Δ, B has a derivation of height ⩽ n. QED.

Given a sequent Γ ⇒ Δ, each step of a root-first proof search is a reduction that removes a connective and it follows that proof search terminates.

The leaves are topsequents of form

⊥, …, ⊥, P_{1}, …, P_{m} ⇒ Q_{1}, …, Q_{n}, ⊥, …, ⊥

where the number of ⊥’s in the antecedent or succedent as well as m or n can be 0.

Lemma 3.1.2: The decomposition of a sequent Γ ⇒ Δ into topsequents in G3cp is unique.

Proof: By noting that successive application of any two logical rules in G3cp commutes. QED.

Root-first proof search gives a method for finding a representation of formulas of propositional logic in a certain normal form: Given a formula C, apply the decomposition to ⇒ C, and after having reduced all connectives, if among the topsequents produced a sequent has ⊥ as a formula in the antecedent, discard the sequent. If it has the same atom in the antecedent and succedent, discard it. If it has occurrences of ⊥ and atoms in the succedent, delete the ⊥’s. If the succedent is empty or has only occurrences of ⊥, write just one ⊥. Finally, delete possible repetitions of atoms in antecedent and succedent. This leaves a finite number of sequents of the following forms, where any two atoms are distinct:

1. P_{1}, …, P_{m} ⇒ Q_{1}, …, Q_{n},

2. ⇒ Q_{1}, …, Q_{n},

3. P_{1}, …, P_{m} ⇒ ⊥,

4. ⇒ ⊥.

Definition 3.1.3: A basic sequent is a sequent of form P_{1}, …, P_{m} ⇒ Q_{1}, …, Q_{n} where any two atoms are distinct, the antecedent is empty if m = 0 and the succedent is ⊥ if n = 0. The trace formula of a basic sequent is

1. P_{1}& … &P_{m} ⊃ Q_{1} ∨ … ∨ Q_{n} for m, n > 0,

2. Q_{1} ∨ … ∨ Q_{n} for m = 0, n > 0,

3. ∼(P_{1}& … &P_{m}) for m > 0, n = 0,

4. ⊥ for m, n = 0.

Trace formulas are unique up to the order in the disjunctions and conjunctions. By the invertibility of the rules of G3cp, a basic sequent with trace formula C is derivable if and only if the sequent ⇒ C is derivable. It follows that a formula is equivalent to the conjunction of its trace formulas:

Theorem 3.1.4: A formula C is equivalent to the conjunction of the trace formulas of its decomposition into basic sequents.

Proof: Let the topsequents of the decomposition of ⇒ C be Γ_{1} ⇒ Δ_{1}, …, Γ_{m} ⇒ Δ_{m}, with the n first giving the trace formulas C_{1}, …, C_{n} and the rest, if m > n, having ⊥ in the antecedent or the same atom in the antecedent and succedent. We have to show that ⇒ C ⊃⊂ C_{1}& … &C_{n} is derivable. We have a derivation of ⇒ C from Γ_{1} ⇒ Δ_{1}, …, Γ_{m} ⇒ Δ_{m} using invertible rules. By adding the formula C to the antecedent of each sequent in the derivation, we obtain a derivation of C ⇒ C from C, Γ_{1} ⇒ Δ_{1}, …, C, Γ_{m} ⇒ Δ_{m} by the same invertible rules. Therefore each step in each root-first path, from C ⇒ C to C, Γ_{i} ⇒ Δ_{i}, is admissible. Since C ⇒ C is derivable, each C, Γ_{i} ⇒ Δ_{i} is derivable. It follows that for each trace formula, up to n, the sequent C ⇒ C_{i} is derivable. Therefore, by repeated application of R&, C ⇒ C_{1}& … &C_{n} is derivable, and by R⊃, ⇒ C ⊃ C_{1}& … &C_{n} is derivable.

Conversely, starting from the given derivation of ⇒ C from topsequents Γ_{1} ⇒ Δ_{1}, …, Γ_{m} ⇒ Δ_{m}, add the formulas C_{1}, …, C_{n} to the antecedent of each sequent in the derivation, to obtain a derivation of C_{1}, …, C_{n} ⇒ C from new topsequents of form C_{1}, …, C_{n}, Γ_{i} ⇒ Δ_{i}. For i > n, such sequents are axioms since they have ⊥ in the antecedent or the same atom in the antecedent and succedent. For i ⩽ n they are derivable since each C_{1}, …, C_{n} ⇒ C_{i} is derivable. Application of L& and R⊃ to C_{1}, …, C_{n} ⇒ C now gives a derivation of ⇒ C_{1}& … &C_{n} ⊃ C. QED.

As a consequence of lemma 3.1.2, the representation given by the theorem is unique up to order in the conjunction and the conjunctions and disjunctions in the trace formulas. Each trace formula P_{1}& … &P_{m} ⊃ Q_{1} ∨ … ∨ Q_{n} is classically equivalent to ∼P_{1}∨… ∨ ∼P_{m}∨Q_{1}∨…∨Q_{n}; the representation is in effect a variant of the conjunctive normal form of formulas of classical propositional logic.

(b) Negation as a primitive connective: In Gentzen’s original classical sequent calculus LK of 1934–35, negation was a primitive, with two rules that make a negation appear on the left and right part of the conclusion, respectively:

{Γ ⇒ Δ, A \atop ∼A, Γ ⇒ Δ}^{L∼}  {A, Γ ⇒ Δ \atop Γ ⇒ Δ, ∼A}^{R∼}

Now negation displays the same elegant symmetry of left and right rules as the other connectives. Five years later, Gentzen commented on this property of the multisuccedent calculus as follows (1938, p. 25): “The special role of negation, an annoying exception in the natural deduction calculus, has been completely removed, in a way approaching magic. I should be permitted to express myself thus since I was, when putting up the calculus LK for the first time, greatly surprised that it had such a property.”

Gentzen’s rules for negation, with the definition ∼ A ≡ A ⊃ ⊥, are admissible in G3cp, the first one by

\begin{matrix}Γ ⇒ Δ, A & ⊥, Γ ⇒ Δ^{L⊥} \\ A ⊃ ⊥, Γ ⇒ Δ \end{matrix}_{L⊃}

and the second one by

{A, Γ ⇒ Δ \atop A, Γ ⇒ Δ, ⊥}^{RW}

Γ ⇒ Δ, A ⊃ ⊥ R⊃

where RW is right weakening, to be proved admissible shortly.

3.2. Admissibility of structural rules

We shall prove admissibility of weakening, contraction and cut for the calculus G3cp. There will be two weakening rules, a left one for weakening in the antecedent and a right one for weakening in the succedent, and similarly for contraction. The rules are as follows:

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

The proofs of admissibility of left and right weakening are similar to the proof of height-preserving weakening for G3ip in theorem 2.3.4:

Theorem 3.2.1: Height-preserving weakening. If ⊢_{n} Γ ⇒ Δ, then ⊢_{n} A, Γ ⇒ Δ. If ⊢_{n} Γ ⇒ Δ, then ⊢_{n} Γ ⇒ Δ, A.

Proof: The addition of formula A to the antecedent and consequent, respectively, of each sequent in the derivation of Γ ⇒ Δ, will produce derivations of A, Γ ⇒ Δ and Γ ⇒ Δ, A. QED.

It follows that if a sequent Γ ⇒ with an empty succedent is derivable, the sequent Γ ⇒ ⊥ also is derivable.

Theorem 3.2.2: Height-preserving contraction. If ⊢_{n} C, C, Γ ⇒ Δ, then ⊢_{n} C, Γ ⇒ Δ. If ⊢_{n} Γ ⇒ Δ, C, C, then ⊢_{n} Γ ⇒ Δ, C.

Proof: The proof of admissibility of left and right contraction is done simultaneously, by induction on height of derivation of the premiss. For n = 0, if the premiss is an axiom or conclusion of L⊥, the conclusion also is an axiom or conclusion of L⊥ whether contraction was applied on the left or right. For the inductive case, assume height-preserving left and right contraction up to derivations of height n. As in the proof of contraction for the single succedent calculus, theorem 2.4.1, we distinguish two cases: If the contraction formula is not principal in the last rule applied, we apply the inductive hypothesis to the premisses and then the rule. If the contraction formula is principal, we have six subcases according to the last rule applied.

If the last rule is L& or L∨, the proof proceeds as in theorem 2.4.1. If the last rule is R&, the premisses are ⊢_{n} Γ ⇒ Δ, A&B, A and ⊢_{n} Γ ⇒ Δ, A&B, B. By height-preserving invertibility, we obtain ⊢_{n} Γ ⇒ Δ, A, A and ⊢_{n} Γ ⇒ Δ, B, B, and the inductive hypothesis gives ⊢_{n} Γ ⇒ Δ, A and ⊢_{n} Γ ⇒ Δ, B. The conclusion ⊢_{n+1} Γ ⇒ Δ, A&B follows by R&. If the last rule is R∨, the premiss is ⊢_{n} Γ ⇒ Δ, A ∨ B, A, B and we apply height-preserving invertibility to conclude ⊢_{n} Γ ⇒ Δ, A, B, A, B, then the inductive hypothesis twice to obtain ⊢_{n} Γ ⇒ Δ, A, B, and last R∨.

If the last rule is R⊃, the premiss is ⊢_{n} A, Γ ⇒ Δ, A ⊃ B, B and we apply height-preserving invertibility to conclude ⊢_{n} A, A, Γ ⇒ Δ, B, B, then the inductive hypothesis to conclude ⊢_{n} A, Γ ⇒ Δ, B and then R⊃. If L⊃ was applied, we have the derivation of the premiss of contraction,

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

By height-preserving inversion, we have ⊢_{n} Γ ⇒ Δ, A, A and ⊢_{n} B, B, Γ ⇒ Δ. By the inductive hypothesis, we have ⊢_{n} Γ ⇒ Δ, A and ⊢_{n} B, Γ ⇒ Δ, and obtain a derivation of A ⊃ B, Γ ⇒ Δ in at most n + 1 steps. QED.

A proof by separate induction on left and right contraction will not go through if the last rule is L⊃ or R⊃.

Theorem 3.2.3: The rule of cut,

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

Γ, Γ′ ⇒ Δ, Δ′ Cut

is admissible in G3cp.

Proof: The proof is organized as that of theorem 2.4.3.

Cut with an axiom or conclusion of L⊥ as premiss: If at least one of the premisses of cut is an axiom, we distinguish two cases:

1. The left premiss Γ ⇒ Δ, D of cut is an axiom or conclusion of L⊥. There are three subcases:

1.1. The cut formula D is in Γ. In this case we derive Γ, Γ′ ⇒ Δ, Δ′ from the right premiss D, Γ′ ⇒ Δ′ by weakening.

1.2. Γ and Δ have a common atom. Then Γ, Γ′ ⇒ Δ, Δ′ is an axiom. 1.3. ⊥ is a formula in Γ. Then Γ, Γ′ ⇒ Δ, Δ′ is a conclusion of L⊥.

2. The right premiss D, Γ′ ⇒ Δ′ is an axiom or conclusion of L⊥. There are four subcases: 2.1. D is in Δ′. Then Γ, Γ′ ⇒ Δ, Δ′ follows from the first premiss by weakening. 2.2. Γ′ and Δ′ have a common atom. Then Γ, Γ′ ⇒ Δ, Δ′ is an axiom. 2.3. ⊥ is in Γ′. Then Γ, Γ′ ⇒ Δ, Δ′ is a conclusion of L⊥. 2.4. D = ⊥. Then either the first premiss is an axiom or conclusion of L⊥ and Γ, Γ′ ⇒ Δ, Δ′ follows as in case 1, or Γ ⇒ Δ, ⊥ has been derived. There are six cases according to the rule used. These are transformed into derivations with cuts of lesser cut-height. Since ⊥ is never principal in a rule, and the transformations are special cases of the transformations 3.1– 3.6 below, with D = ⊥, they need not be written out here. Cut with neither premiss an axiom: We have three cases:

3. Cut formula D is not principal in the left premiss. We have six subcases according to the rule used to derive the left premiss. For L& and L∨, the transformations are analogous to cases 3.1 and 3.2 of theorem 2.4.3. For implication, we have 3.3. L⊃, with Γ = A ⊃ B, Γ′′. The derivation

\begin{matrix}Γ′′ ⇒ Δ, D, A & B, Γ′′ ⇒ Δ, D \\ A ⊃ B, Γ′′ ⇒ Δ, D \end{matrix}^{L⊃} D, Γ′ ⇒ Δ′

A ⊃ B, Γ′′, Γ′ ⇒ Δ, Δ′ Cut

is transformed into the derivation

Γ′′ ⇒ Δ, D, A D, Γ′ ⇒ Δ′ Γ′′, Γ′ ⇒ Δ, Δ′, A^{Cut} B, Γ′′ ⇒ Δ, D D, Γ′ ⇒ Δ′ B, Γ′′, Γ′ ⇒ Δ, Δ′^{Cut}

A ⊃ B, Γ′′, Γ′ ⇒ Δ, Δ′ L⊃

with two cuts of lower cut-height. 3.4. R&, with Δ = A&B, Δ′′. The derivation

\begin{matrix}Γ ⇒ Δ′′, A, D & Γ ⇒ Δ′′, B, D \\ Γ ⇒ Δ′′, A&B, D \end{matrix}^{R&} D, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ′′, A&B, Δ′ Cut

is transformed into the derivation with two cuts of lower height

Γ ⇒ Δ′′, A, D D, Γ′ ⇒ Δ′ Γ, Γ′ ⇒ Δ′′, A, Δ′^{Cut} Γ ⇒ Δ′′, B, D D, Γ′ ⇒ Δ′ Γ, Γ′ ⇒ Δ′′, B, Δ′^{Cut}

Γ, Γ′ ⇒ Δ′′, A&B, Δ′ R&

3.5. R∨, with Δ = A ∨ B, Δ′′. The derivation

{Γ ⇒ Δ′′, A, B, D \atop Γ ⇒ Δ′′, A ∨ B, D}^{R∨} D, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ′′, A ∨ B, Δ′ Cut

is transformed into the derivation with a cut of lower cut-height

Γ ⇒ Δ′′, A, B, D D, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ′′, A, B, Δ′ Cut

Γ, Γ′ ⇒ Δ′′, A ∨ B, Δ′ R∨

3.6. R⊃, with Δ = A ⊃ B, Δ′′. The derivation

{Γ, A ⇒ Δ′′, B, D \atop Γ ⇒ Δ′′, A ⊃ B, D}^{R⊃} D, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ′′, A ⊃ B, Δ′ Cut

is transformed into the derivation with a cut of lower cut-height

\begin{matrix}Γ, A ⇒ Δ′′, B, D & D, Γ′ ⇒ Δ′ \\ Γ, Γ′, A ⇒ Δ′′, B \end{matrix}^{Cut}

Γ, Γ′ ⇒ Δ′′, A ⊃ B, Δ′ R⊃

4. Cut formula D is principal in the left premiss only, and the derivation is transformed in one with a cut of lower cut-height according to derivation of the right premiss. We have six subcases according to the rule used. Only the cases of L⊃ and R∨ are significantly different from the cases of theorem 2.4.3:

4.3. L⊃, with Δ = A ⊃ B, Δ′. The derivation and its transformation are similar to the previous case 3.3.

4.5. R∨, with Δ = A ∨ B, Δ′′. The derivation

Γ ⇒ Δ, D {D, Γ′ ⇒ A, B, Δ \atop D, Γ′ ⇒ A ∨ B, Δ′′} ^{R∨}

Γ, Γ′ ⇒ Δ, A ∨ B, Δ′′ Cut

is transformed into the derivation with a cut of lower cut-height

Γ ⇒ Δ, D D, Γ′ ⇒ A, B, Δ′′

Γ, Γ′ ⇒ Δ, A, B, Δ′′ Cut

Γ, Γ′ ⇒ Δ, A ∨ B, Δ′′ R∨

5. Cut formula D is principal in both premisses, and we have three subcases, of which conjunction is very similar to case 5.1 of theorem 2.4.3. 5.2. D = A ∨ B, and the derivation

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

Γ, Γ′ ⇒ Δ, Δ′ Cut

is transformed into

Γ ⇒ Δ, A, B A, Γ′ ⇒ Δ′ Γ, Γ′ ⇒ Δ, Δ′, B^{Cut} B, Γ′ ⇒ Δ′

Γ, Γ′, Γ′ ⇒ Δ, Δ′, Δ′ Cut

Γ, Γ′ ⇒ Δ, Δ′ Ctr

with two cuts of lower cut-height. 5.3. D = A ⊃ B, and the derivation

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

Γ, Γ′ ⇒ Δ, Δ′ Cut

is transformed into the derivation with two cuts of lower cut-heights

Γ′ ⇒ Δ′, A A, Γ ⇒ Δ, B Γ, Γ′ ⇒ Δ, Δ′, B^{Cut} B, Γ′ ⇒ Δ′

Γ, Γ′, Γ′ ⇒ Δ, Δ′, Δ′ Cut

Γ, Γ′ ⇒ Δ, Δ′ Ctr

QED. We obtain, just as for the calculus G3ip, the subformula property, Corollary 3.2.4: Each formula in the derivation of Γ ⇒ Δ in G3cp is a subformula of Γ, Δ.

It follows in particular that the sequent ⇒ is not derivable. We concluded from the admissibility of weakening that if Γ ⇒ is derivable, then also Γ ⇒ ⊥ is derivable. The converse is now obtained by applying cut to Γ ⇒ ⊥ and ⊥ ⇒ , thus, an empty succedent behaves like ⊥.

In intuitionistic logic, all connectives are needed, but in classical logic, negation and one of &, ∨, ⊃ can express the remaining two. How does the interdefinability of connectives affect proof analysis? Gentzen says that one could replace some rules by others in classical sequent calculus, but that if this were done, the cut elimination theorem would not be provable anymore (1934–35, III. 2.1).

If we consider the ⊃, ⊥ fragment of G3cp, the cut elimination theorem remains valid. Conjunction and disjunction can be defined in terms of implication and falsity, thus, for any formula A there is a translated formula A^{∗} in the fragment classically equivalent to it. Similarly, sequents Γ ⇒ Δ of G3cp have translations Γ^{∗} ⇒ Δ^{∗} derivable in the fragment if and only if the original sequent is derivable in G3cp. By the admissibility of cut, the derivation uses only the logical rules for implication and falsity.

Gentzen’s statement about losing the cut elimination theorem is probably based on considerations of the following kind: According to Hilbert’s program, logic and mathematics had to be represented as formal manipulations of concrete signs. In propositional logic, the signs are the connectives, atomic formulas, and parentheses. Once these are given, there is no question of defining one sign by another. But it is permitted to reduce or change the set of formal axioms and rules by which the signs are manipulated. Thus, one gets along in propositional logic with just one rule, modus ponens. The axioms for conjunction and disjunction in Hilbert-style, in Section 2.5(b) above, could in classical logic be replaced by the axioms A ∨ B ⊃ (∼ A ⊃ B), (∼ A ⊃ B) ⊃ A ∨ B and A&B ⊃ ∼ (B ⊃ ∼ A), ∼ (B ⊃ ∼ A) ⊃ A&B. If these axioms are added to the fragment of G3cp in the same way as in Section 2.5(b), as sequents with empty antecedents, they can only be put to use by the rule of cut, and it is this phenomenon that Gentzen seems to have had in mind.

Later on Gentzen admitted, however, the possibility of “dispensing with the sign ⊃ in the classical calculus LK by considering A ⊃ B as an abbreviation for ∼ A ∨ B; it is easy to prove that the rules R⊃ and L⊃ can be replaced by the rules for ∨ and ∼” (1934–35, III. 2.41).^{1}

1The text has “NK” (also in the English translation) that is Gentzen’s name for classical natural deduction, but this must be a misprint since he expressly refers to rules of sequent calculus.

3.3. Completeness

The decomposability of formulas in G3cp can be turned into a proof of completeness of the calculus. For this purpose, we have to define the basic semantical concepts of classical propositional logic:

Definition 3.3.1: A valuation is a function v from formulas of propositional logic to the set {0, 1} such that

v(⊥) = 0,

v(A&B) = min(v(A), v(B)),

v(A ∨ B) = max(v(A), v(B)),

v(A ⊃ B) = max(1 − v(A), v(B)).

Observe that, by definition of v, v(A ⊃ B) = 1 if and only if v(A) ⩽ v(B). Valuations are extended to multisets Γ by taking conjunctions ⋀(Γ) and disjunctions ⋁(Γ) of formulas in Γ, with ⋀( ) = ⊥ and ⋁( ) = ⊤ for the empty multiset, and by setting

v ⋀(Γ) ≡ min(v(C)) for formulas C in Γ,

v ⋁(Γ) ≡ max(v(C)) for formulas C in Γ.

Definition 3.3.2: A sequent Γ ⇒ Δ is refutable if there is a valuation v such that v ⋀(Γ) > v ⋁(Δ). Sequent Γ ⇒ Δ is valid if it is not refutable.

It follows that Γ ⇒ Δ is valid if for all valuations v, v ⋀(Γ) ⩽ v ⋁(Δ). For proving the soundness of G3cp, we need the following lemma about valuations:

Lemma 3.3.3: For a valuation v, min(v(A), v(B)) ⩽ v(C) if and only if v(A) ⩽ v(B ⊃ C).

Proof: If v(A) = 0 the claim trivially holds. Else min(v(A), v(B)) = v(B), thus min(v(A), v(B)) ⩽ v(C) if and only if v(B) ⩽ v(C), if and only if v(B ⊃ C) = 1, i.e., v(A) ⩽ v(B ⊃ C). QED.

Corollary 3.3.4: min(v(A ⊃ B), v(A)) ⩽ v(B).

Proof: Immediate by lemma 3.3.3. QED.

Theorem 3.3.5: Soundness. If a sequent Γ ⇒ Δ is derivable in G3cp, it is valid.

Proof: Assume Γ ⇒ Δ derivable. We prove by induction on height of derivation that it is valid. If it is an axiom or conclusion of L⊥ it is valid since we always have v ⋀(P, Γ) ⩽ v ⋁(Δ, P) and v ⋀(⊥, Γ) ⩽ v ⋁(Δ).

If the last rule is L&, we have by inductive hypothesis for all valuations v that v ⋀(A, B, Γ) ⩽ v ⋁(Δ), and v ⋀(A&B, Γ) ⩽ v ⋁(Δ) follows by v ⋀(A&B, Γ) = v ⋀(A, B, Γ). The case for R∨ is dual to this. For L∨, we have v ⋀(A, Γ) ⩽ v ⋁(Δ) and v ⋀(B, Γ) ⩽ v ⋁(Δ). Then

v ⋀(A ∨ B, Γ) = max(v ⋀(A, Γ), v ⋀(B, Γ)) ⩽ v ⋁(Δ).

The case of R& is dual to this. If the last rule is L⊃, suppose

v ⋀(Γ) ⩽ max(v ⋁(Δ), v(A)) and min(v(B), v ⋀(Γ)) ⩽ v ⋁(Δ).

There are two cases: If v ⋁(Δ) = 1, then the conclusion is trivial. If v ⋁(Δ) = 0, then v ⋀(Γ) ⩽ v(A) and min(v(B), v ⋀(Γ)) ⩽ 0. From the former follows

min(v(A ⊃ B), v ⋀(Γ)) ⩽ min(min(v(A ⊃ B), v(A)), v ⋀(Γ))

and therefore, using corollary 3.3.4,

min(v(A ⊃ B), v ⋀(Γ)) ⩽ min(v(B), v ⋀(Γ)) ⩽ 0.

If the last rule is R⊃, we have

min(v(A), v ⋀(Γ)) ⩽ max(v ⋁(Δ), v(B))

and there are two cases: If v ⋁(Δ) = 1, then the conclusion is trivial. Else we have min(v(A), v ⋀(Γ)) ⩽ v(B), hence by lemma 3.3.3, v ⋀(Γ) ⩽ v(A ⊃ B) and a fortiori v ⋀(Γ) ⩽ max(v ⋁(Δ), v(A ⊃ B)). QED.

Theorem 3.3.6: Completeness. If a sequent Γ ⇒ Δ is valid, it is derivable in G3cp.

Proof: Apply root-first the rules of G3cp to the sequent Γ ⇒ Δ, obtaining leaves that are either axioms, conclusions of L⊥, or basic sequents. We prove that if Γ ⇒ Δ is valid, then the set of basic sequents is empty, and therefore Γ ⇒ Δ is derivable. Suppose that the set of basic sequents consists of Γ_{1} ⇒ Δ_{1}, …, Γ_{n} ⇒ Δ_{n}, with n > 0, and let C_{i} be their corresponding trace formulas. We have, by theorem 3.1.4, ⇒ C ⊃⊂ C_{1}& … &C_{n}, where C is ⋀(Γ) ⊃ ⋁(Δ). Since Γ ⇒ Δ is valid, then by definition v(C) = 1 for every valuation v, and since C ⇒ C_{1}& … &C_{n}, by soundness v(C) ⩽ v(C_{1}& … &C_{n}), which gives v(C_{i}) = 1 for each C_{i} and every valuation v. No C_{i} is ⊥, since no valuation validates it. No C_{i} is ¬(P_{1}& … &P_{m}) since the valuation with v(P_{j}) = 1 for all j ⩽ m does not validate it. Finally no C_{i} is P_{1}& … &P_{m} ⊃ Q_{i} ∨ … ∨ Q_{r} or Q_{i} ∨ … ∨ Q_{r} since it is refuted by the valuation with v(P_{j}) = 1 for all j ⩽ m and v(Q_{k}) = 0 for all k ⩽ r. QED.

Decomposition into basic sequents gives a syntactic decision method for formulas of classical propositional logic: A formula C is valid if and only if no top sequent is a basic sequent.

Notes to Chapter 3:

The logical rules of the calculus G3cp first appear in Ketonen (1944, p. 14), the main results of whom were made known through the long review by Bernays (1945). Negation is a primitive connective, derivations start with axioms of form A ⇒ A, and only cut is eliminated, the proof being similar to that of Gentzen. Invertibility is proved by using structural rules.

Direct proofs of invertibility were given by Schütte (1950) and Curry (1963). The proofs of admissibility of structural rules we give follow the method of Dragalin, similarly to the intuitionistic calculus. Normal form via decomposition through invertible rules and the related completeness theorem are due to Ketonen (1944). He seems to have found his calculus by making systematic the necessity that anyone trying root-first proof search experiences, namely, that one has to repeat the contexts of the conclusion in both premisses of two-premiss rules. In an earlier expository paper, he gives an example of proof search and states that, due to invertibility of the propositional rules, the making of derivations consists of purely mechanical decomposition (1943, pp. 138–139).

The idea of validity as a negative notion, as in definition 3.3.2, was introduced in Negri and von Plato (1998a).