THE LOGIC NOTES

Sequent calculus More about first order logic

Thus far, we have two contrasting presentations of first order logic: as a system of derivations governed by introduction and elimination rules for the connectives and quantifiers, and as a semantic theory with an associated technique of analysis by semantic tableaux. The aim of the present chapter is to unify these two accounts by presenting logic in yet another way: by proving sequents directly as consequences of simpler sequents rather than by producing derivations from their premises to their conclusions on the level of formulae. Not too surprisingly, logic in this form is known as the sequent calculus.

Our system of natural deduction already has a dual character: we can see the inference steps as transforming formulae into other formulae, producing derivations as advertised in Chapter 2 of these notes, or we can see them as transformations on sequents, as is convenient for stating rules that involve discharge, for instance. Consider:

SP {p IMP q,  r IMP p ⊢ r IMP q} PL {1} {1} {p IMP q} {A} PL {2} {2} {r IMP p} {A} PL {3} {3} {r} {A} PL {2,3} {4} {p} {2, 3 IMPE} PL {1,2,3} {5} {q} {1, 4 IMPE} PL {1,2} {5} {r IMP q} {5 [3] IMPI} EP

Each line of the proof in the linear format can be read as a formula with assumption numbers to record what supports it, or it can be read as a sequent whose premises are abbreviated to numerals and whose conclusion is written in full. The step at line 5 above, for example, can be seen as an inference of q from p IMP q and p, with the numbers on the left recording that assumptions 1, 2 and 3 were needed to get this far. Alternatively, it can be seen as an inference from the sequents

p IMP q   ⊢   p IMP q   (i.e. line 1)

and

r IMP p,  r   ⊢   p   (i.e. line 4)

to

p IMP q,  r IMP p,  r   ⊢   q   (i.e. line 5)

Thus natural deduction is already a kind of calculus of sequents, so it is not a large step to express it fully as such.

The most convenient sequent calculus for classical logic involves a generalisation of the notion of a sequent, to make it a relation between a set of premises and a set of conclusions. It is not essential to do this—sequent calculi are often defined with single formulae on the conclusion side—but the formulation of orthodox logic as a multiple conclusion system is easy and beautiful, so we follow that route here. An argument with a set of premises and a set of conclusions is to be regarded as valid iff it is impossible to drive a semantic wedge between the two sets: that is, iff there is no possible interpretation on which all of the premises are true and all of the conclusions are false. The notion of a consequence relation has to be extended a little to allow for multiple conclusions as well as multiple premises:

  • Reflexivity:  A ⊢ A;

  • Monotonicity: If X ⊢ Y then X,X' ⊢ Y,Y' (using the comma to represent set union as before);

  • Cut: If X, A ⊢ Y and also X ⊢ A, Y then X ⊢ Y.
Sequents in this form no longer suggest a preferred direction for inference: it may transmit truth from left to right, or falsehood from right to left, these readings standing on an equal footing.

Making sequents multiple on the right as well as the left gives the presentation of logic a beautiful symmetry. One effect of this is to bring out the duality between conjunction (AND) and disjunction (OR). In the usual natural deduction calculus, we can see that the rule ANDE is just like the rule ORI but in reverse. Each corresponds to one step of immediate consequence:

A AND B  ⊢  A dual to A  ⊢  A OR B

The ANDI rule also corresponds to a one-step inference, A, B  ⊢  A AND B but in the single-conclusion format enforced by natural deduction there is no dual one-step version of ORE. As we have seen, it has to be simulated in a more or less complicated way. However, when we allow multiple conclusions, we can say that the immediate consequence of A OR B is that one of the two formulae (A or B) is true, without having to say which one. That is:

A, B  ⊢  A AND B dual to A OR B  ⊢  A, B

So there is a simple step of immediate consequence from a disjunction, exactly as there is one to a conjunction, but in order to express it we need the more generous format of sequents which may be multiple on both sides.

The fundamental difference between natural deduction and the sequent calculus is that in the latter sequents are only built up out of simpler ones by introducing connectives and quantifiers, whereas in the former there are also elimination rules that allow simpler sequents to be derived from more complex ones. To transform the natural deduction calculus into the sequent calculus, rules for eliminating operators on the right of sequents have to be reformulated as rules for introducing the same operators on the left.

In a sense, it is clear that elimination on the right should amount to the same thing as introduction on the left, since both are ways of saying what follows from a formula of a given form. In fact, the two forms of each rule are inter-derivable using cut. Consider conjunction, for example. The introduction rule for 'AND'

X  ⊢  A X  ⊢  B
ANDI
X  ⊢  A AND B

becomes the sequent calculus rule for 'AND' on the right, just by embedding it in the context of arbitrary parameters Y on the right side of the sequent as well as X on the left:

X  ⊢  A, Y X  ⊢  B, Y
⊢ AND
X  ⊢  A AND B, Y

There are two elimination rules, one for deriving A from A AND B and the other for deriving B. Consider the former. The fact that A is an immediate consequence of A AND B gives the primitive valid sequent

A AND B ⊢ A

For natural deduction, we wish to use this sequent as an elimination rule. In terms of rules as transformations on sequents, this means we need the A AND B to be on the right, not the left. In effect, we apply the "cut" principle to it, together with an arbitrary sequent with the conjunction on the right:

A AND B  ⊢  A X  ⊢  A AND B
cut
X  ⊢  A

In the sequent calculus, there are no elimination rules, so we wish instead to derive a rule for introducing the conjunction on the left. The above primitive sequent does have A AND B on the left as required, but it will not quite do as the left introduction rule for conjunction because of the A it introduces on the right. We therefore need to remove the A by cutting with an arbitrary sequent with A on the left:

A AND B  ⊢  A X, A  ⊢  Y
cut
X, A AND B  ⊢  Y

This is the sequent calculus rule for 'AND' on the left, allowing a conjunction A AND B to replace one of its conjuncts A on the left. There is a similar rule for putting A AND B in place of B, giving the pair of rules:

X, A  ⊢  Y AND ⊢1
X, A AND B  ⊢  Y
X, B  ⊢  Y AND ⊢2
X, A AND B  ⊢  Y

Equivalently, the two rules may be combined into one:

X, A, B  ⊢  Y AND ⊢
X, A AND B  ⊢  Y

Next consider implication. The rule for implication on the right is just the natural deduction rule IMPI:

Allowing arbitray parameters on the right is not quite such a trivial thing to do, in fact. It allows proofs of certain sequents such as (p IMP q) IMP p ⊢ p which cannot be proved in the natural deduction system using IMPI and IMPE alone (though they can be proved by taking a detour through negation).
X, A  ⊢  B IMPI
X  ⊢  A IMP B

with the additional parameters Y:

X, A  ⊢  B, Y ⊢ IMP
X  ⊢  A IMP B, Y

For implication on the left, we begin by reducing the elimination rule IMPE to its characteristic sequent:

A IMP B, A   ⊢   B

and, as before, cut to remove the A and the B:

A IMP B, A  ⊢  B X  ⊢  A, Y cut
X, A IMP B  ⊢  B, Y X, B  ⊢  Y cut
X, A IMP B  ⊢  Y

leaving the rule in the form:

X  ⊢  A, Y X, B  ⊢  Y IMP ⊢
X, A IMP B  ⊢  Y

Negation is very similar. On the right, we have the natural deduction rule NOTI:

X, A  ⊢  BAD NOTI
X  ⊢  NOTA

which, remembering that BAD,Y on the right is equivalent to Y, immediately converts into the sequent calculus rule:

X, A  ⊢  Y ⊢ NOT
X  ⊢  NOTA, Y

For the left rule, we start with NOTE

A NOTA NOTE
BAD

and its characteristic sequent:

A, NOTA   ⊢   BAD

which we may cut with an arbitrary sequent having A on the right:

A, NOTA   ⊢   BAD X  ⊢  A, Y
cut
X, NOTA  ⊢  Y

The rule for the universal quantifier on the right

X  ⊢  A, Y ⊢ ALL
X  ⊢  ALLvAvm, Y

is essentially the same as ALLI and is subject to the same condition that m should not occur in any formula in X or Y. For the universal on the left, note that ALLE amounts to the provability of the sequent

ALLv A   ⊢   Atv

from which we obtain on the usual way:

ALLv A   ⊢   Atv X, Atv ⊢  Y
cut
X, ALLv A  ⊢  Y

Finally, the elimination rules for disjunction and the existential quantifier, ORE and SOMEE, are essentialy already in the form of sequent calculus rules followed by cuts, so there is little to do to adapt them for the sequent calculus.

The full set of rules is given in the Reference section.

So the sequent calculus is in essence the natural deduction calculus generalised a little to allow for multiple conclusions and rewritten to use left and right introduction rules instead of introduction and elimination rules. It does, however, sustain another reading. If we think of a provable sequent as saying that there is no way to make its premises true and its conclusions false, then each of the rules takes the form of a justification of such a claim, in effect saying why the sequent is valid: becuse if its premises were true and its conclusions false, the same would have to hold of one or more of the simpler sequents from which it is immediately derived. Hence the sequent calculus can be viewed as a form of semantic reasoning rather than as reasoning about the existence of derivations.

t: A AND B
t: A,   t: B
f: A AND B
f: A f: B
X, A, B ⊢ Y
X, A AND B ⊢ Y
X ⊢ A, Y X ⊢ B, Y
X ⊢ A AND B, Y
:   Upside down? Rules for AND in
semantic tableaux and sequent calculus

We have seen such reasoning before: it is reminiscent of the reasoning captured in semantic tableaux. On closer examination, indeed, it turns out to be exactly the reasoning captured in semantic tableaux. At each node of a tableau is a set of formulae labelled as true and a set labelled as false; we may think of these as the left side (premises) and the right side (conclusions) of a sequent. Then the tableau rule for analysing a formula with the label t is nothing but the sequent calculus rule for introducing that formula on the left, and the tableau rule for analysing a formula with the label f is the sequent calculus rule for introducing it on the right. The only difference is that in a tableau rule the complex formula is written above the line and the simpler one(s) below, whereas in the sequent calculus rule it is the other way around. It follows that a closed tableau is, but for some trivial differences of notation, just a sequent calculus proof upside down (or the proof is the tableau upside down if you prefer).

Click here for an example illustrating the last point.

Thus the sequent calculus is a unifying theory, bringing the semantic and the deduction-theoretic accounts of logic together in a coherent way. It is also a beautiful system in its own right, bringing out the dualities and intrinsic symmetry of classical logic in a way that is hidden by the natural deduction treatment. It also has other useful features, notably the subformula property: in every rule of the system, every formula occurring above the line is (up to substitution of terms for variables) a subformula of one occurring below the line. It follows that every formula occurring in a sequent calculus proof is a subformula of one in the sequent being proved. This fact gives us a great deal of control over the form of possible proofs, and a systematic method of searching for them.

There is, however, a catch. The structural rule of cut, which is essential if the sequent calculus is to match the natural deduction one—or indeed if it is to define a consequence relation at all—does not share the subformula property. We therefore do not want to take cut as a primitive rule of the system (though we would have no problem in regarding reflexivity and monotonicity as primitives). This leads to a problem: we have to show somehow that, although the sequent calculus is formulated without stipulating it, cut holds anyway. That is, we must show that the addition of a cut rule to the sequent calculus would not change anything: any sequent which could be proved in the calculus using cut as an additional rule can already be proved in the calculus as it stands, without appeal to cut. This is the cut elimination problem and it arises for all sequent calculi. By the equivalence just noted, it also arises for tableaux, of course.

We shall not prove cut elimination in the this chapter. Those who wish to pursue it can find a readable version of the classic proof here. For now, we simply note that cut does hold, and that this fact requires a non-trivial proof.