# 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:

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 pr   ⊢   p   (i.e. line 4)

to

p IMP qr IMP pr   ⊢   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 sequent XY is valid if X and Y have a member in common. In particular,  AA;
• Monotonicity: If XY then X,X'Y,Y' (using the comma to represent set union as before);
• Cut: If X, AY and also XA, Y then XY.
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 BA

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 just1 the natural deduction rule IMPI:

 X, A  ⊢  B IMPI X  ⊢  A IMP B

 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  ⊢  ⊥ NOTI X  ⊢  NOTA

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

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

 A NOTA NOTE ⊥

and its characteristic sequent:

A, NOTA   ⊢   ⊥

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

 A, NOTA   ⊢   ⊥ 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).