sequent-calculus
1
SEQUENT
CALCULUS
Yoshihiro Maruyama
co-taught with Pascal Bercher
on the legacy of John Slaney
INTRODUCTION: FROM NATURAL DEDUCTION TO SEQUENT CALCULUS
Gentzen is the discoverer of natural deduction (1934; Szabo’s translation):
“We wish to set up a formalism that reflects as accurately as possible the actual logical
reasoning involved in mathematical proofs.”
Is natural deduction so natural? If so, why do we struggle with ND proofs of trivial
logical truths such as “A or not A”. If it is natural, everything should follow naturally.
2
https://prabook.com/web/gerhard.gentzen/3757132
Gerhard Gentzen (1909-1945)
Died at 35 for starvation (WWII)
Gödel died for starvation too, yet
for a different reason (mental issue)
INTRODUCTION (CONT’D)
Gentzen discovered both natural deduction and sequent calculus. Why did he need
sequent calculus in addition to natural deduction?
Five years after Gödel’s discovery of incompleteness theorems (one of which says it is
impossible to prove the consistency of a system within that system), Gentzen proved
the consistency of arithmetic via sequent calculus.
Sequent calculus is now broadly applied in logic and computer science (and even
physics) as well as for consistency proofs in foundations of mathematics.
3
INTRODUCTION (CONT’D)
“Gentzen was motivated by a desire to establish the consistency of number theory. He
was unable to prove the main result required for the consistency result, the cut
elimination theorem—the Hauptsatz—directly for natural deduction. For this reason
he introduced his alternative system, the sequent calculus, for which he proved the
Hauptsatz” (Hauptsatz in logic means cut elimination theorems in sequent calculus.)
A famous saying by Jean-Yves Girard: A logic without cut-elimination is like a car
without an engine. Girard discovered linear logic (we shall learn similar logic).
4
Quote from: https://en.wikipedia.org/wiki/Natural_deduction
https://cacm.acm.org/magazines/2010/10/99493-linear-logic/fulltexthttps://romanripa.typepad.com/.a/6a0148c792648c970c022ad3b6118d200d-popup
Cut elimination is used to define the identity of proofs, and represents
computational process (so it is important in theoretical computer science).
Natural deduction and sequent calculus can be seen as programming languages:
the proof-as-program correspondence (Curry-Howard isomorphism); based on
this you can even extract programs from proofs (constructive programming).
GOAL
5
X, A ⊢ A, Y
Axiom
X, A, B ⊢ Y
X, A ∧ B ⊢ Y
∧ ⊢
X2, B ⊢ Y2X1, A ⊢ Y1
X1, X2, A ∨ B ⊢ Y1, Y2
∨ ⊢
X ⊢ A, Y
¬ ⊢
X, ¬A ⊢ Y
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
X, A ⊢ Y
X, ∀xA ⊢ Y
∀ ⊢
X, A ⊢ Y
X, ∃xA ⊢ Y
∃ ⊢x does not appear as
a free variable in X,Y
X2 ⊢ B, Y2X1 ⊢ A, Y1
X1, X2 ⊢ A ∧ B, Y1, Y2
⊢ ∧
X ⊢ A, B, Y
X ⊢ A ∨ B, Y
⊢ ∨
X, A ⊢ Y
⊢ ¬
X ⊢ ¬A, Y
X, A ⊢ B, Y
X ⊢ A → B, Y
⊢ →
X ⊢ A, Y
X ⊢ ∀xA, Y
⊢ ∀ x does not appear as a free variable in X,Y
X ⊢ A, Y
X ⊢ ∃xA, Y
⊢ ∃
X2, A ⊢ Y2X1 ⊢ A, Y1
X1, X2 ⊢ Y1, Y2
Cut
X, ⊥ ⊢ Y
⊥ ⊢
X ⊢ ⊤ , Y
⊢ ⊤
It may look complex,
but actually easier to
prove in SC than in ND
Assumptions and
conclusions are
symmetric.
The rules are
symmetric too.
SEQUENT
Definition
In natural deduction, a sequent consisted of a set of formulae called its assumptions and a
single formula called its conclusion: .
In sequent calculus, sequents are defined to have a set of conclusions: . Both X and
Y are sets; if we have two C’s in X or Y, we can delete one of them; it’s called contraction.
*Sequents in some non-classical logics, especially substructural logics such as relevant logic or some
fuzzy logics may have more complex structures in place of sets.
X ⊢ A
X ⊢ Y
6
COMMAS IN SEQUENT CALCULUS
We use commas to put multiple premises and conclusions together. In particular,
commas represent set unions. For instance, X, A, B is the set:
Importantly, comma on the left (of ) between premises should read as and while
comma on the right between conclusions should read as or. X, Y usually represent sets
(potentially singletons or even empty sets) and A, B represent single formulae as in:
X ∪ {A, B}
⊢
X, A ⊢ B, Y
7
HOW TO READ RULES
Consider, e.g., the right conjunction rule:
The way to prove in sequent calculus is usually upwards. In this case, read it as follows:
When you have to prove , it suffices to prove and .
To derive or any alternative conclusion in the set Y from the set of premises X, it
suffices to derive A or anything else in Y from X AND B or anything else in Y from X.
Simple proof:
X ⊢ A ∧ B, Y X ⊢ A, Y X ⊢ B, Y
A ∧ B
8
X ⊢ B, YX ⊢ A, Y
X ⊢ A ∧ B, Y
⊢ ∧
A, B ⊢ BA, B ⊢ A
⊢ ∧
A, B ⊢ A ∧ B
Axiom Axiom
SIMPLE EXAMPLE
The commutativity of conjunction:
Proof:
9
A ∧ B ⊢ B ∧ A
A ∧ B ⊢ AA ∧ B ⊢ B
⊢ ∧
A ∧ B ⊢ B ∧ A
∧ ⊢
Ax. Ax.
∧ ⊢
A, B ⊢ B A, B ⊢ A
MODUS PONENS
10
A, A → B ⊢ B
→ ⊢
A ⊢ A, B A, B ⊢ B
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
Ax Ax
DOUBLE NEGATION ELIMINATION
With rule, rule and rule we can prove the double negation elimination
and its converse:
You don’t have to assume the double negation elimination as an additional rule.
Negation works more naturally in sequent calculus than in classical natural deduction.
⊢ ¬ ¬ ⊢ ⊢ →
11
⊢ ¬¬A → A
⊢ →
¬¬A ⊢ A
¬ ⊢
⊢ A, ¬A
⊢ ¬
A ⊢ A
⊢ A → ¬¬A
⊢ →
A ⊢ ¬¬A
⊢ ¬
A, ¬A ⊢
¬ ⊢
A ⊢ A
Ax Ax
MORE PROOFS
12
⊢ A ∨ ¬A
⊢ ∨
⊢ A, ¬A
A ⊢ A
⊢ ¬
Ax
⊢ →
⊢ →
Ax
⊢ →
→ ⊢
⊢ ¬ ¬ ⊢
A ⊢ A
Ax
B ⊢ B
Ax
⊢ A → (B → A)
A ⊢ B → A
A, B ⊢ A
¬B → ¬A ⊢ A → B
A, ¬B → ¬A ⊢ B
¬A, A ⊢⊢ ¬B, B
LEM (the law of excluded middle; ) can be proven much more easily in SC than in ND.A ∨ ¬A
ELIMINATION AND LEFT RULES
The elimination of a connective on the right in natural deduction corresponds to the
introduction of it on the left in sequent calculus:
13
X ⊢ A
X, Y ⊢ B
→E
Y ⊢ A → B
⇔
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
Elimination
Introduction
14
X, A ⊢ A, Y
Axiom
X, A, B ⊢ Y
X, A ∧ B ⊢ Y
∧ ⊢
X2, B ⊢ Y2X1, A ⊢ Y1
X1, X2, A ∨ B ⊢ Y1, Y2
∨ ⊢
X ⊢ A, Y
¬ ⊢
X, ¬A ⊢ Y
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
X, A ⊢ Y
X, ∀xA ⊢ Y
∀ ⊢
X, A ⊢ Y
X, ∃xA ⊢ Y
∃ ⊢x does not appear as
a free variable in X,Y
X2 ⊢ B, Y2X1 ⊢ A, Y1
X1, X2 ⊢ A ∧ B, Y1, Y2
⊢ ∧
X ⊢ A, B, Y
X ⊢ A ∨ B, Y
⊢ ∨
X, A ⊢ Y
⊢ ¬
X ⊢ ¬A, Y
X, A ⊢ B, Y
X ⊢ A → B, Y
⊢ →
X ⊢ A, Y
X ⊢ ∀xA, Y
⊢ ∀ x does not appear as a free variable in X,Y
X ⊢ A, Y
X ⊢ ∃xA, Y
⊢ ∃
X2, A ⊢ Y2X1 ⊢ A, Y1
X1, X2 ⊢ Y1, Y2
Cut
X, ⊥ ⊢ Y
⊥ ⊢
X ⊢ ⊤ , Y
⊢ ⊤
There is a proof of iff
there is a cut-free proof of it
X ⊢ YThe cut rule is not really necessary,
thanks to the cut elimination thm.:
THE SUBFORMULA PROPERTY OF SEQUENT CALCULUS WITHOUT CUT
15
⊢ A ∨ ¬A
⊢ ∨
⊢ A, ¬A
A ⊢ A
⊢ ¬
Ax
⊢ →
⊢ →
Ax
⊢ →
→ ⊢
⊢ ¬ ¬ ⊢
A ⊢ A
Ax
B ⊢ B
Ax
⊢ A → (B → A)
A ⊢ B → A
A, B ⊢ A
¬B → ¬A ⊢ A → B
A, ¬B → ¬A ⊢ B
¬A, A ⊢⊢ ¬B, B
Notice that formulae only become more complex when you infer from the above to the below, i.e.,
any formula in the above sequent is a subformula in the below sequent: the subformula property.
The cut rule is the only exception in
which a formula in the above sequent
does not appear in the below sequent.
Any proof in sequent calculus has the
subformula property if it does not use
the cut rule (useful but redundant).
16
➤ Reflexivity: is provable.
➤ Monotonicity: If is provable, then is provable.
➤ To prove this, use the cut rule twice with axioms and .
➤ Cut: If and are provable, then is provable.
➤ Cut is actually redundant due to the cut elimination theorem (see the logic notes).
A ⊢ A
A ⊢ B A, X ⊢ B, Y
X, B ⊢ B A ⊢ A, Y
X1 ⊢ A, Y1 X2, A ⊢ Y2 X1, X2 ⊢ Y1, Y2
THREE PROPERTIES AS LOGICAL CONSEQUENCE RELATION
17
➤ Some logicians argue any logic must satisfy these three properties, but some logics
actually don’t, esp. resource-sensitive ones (which are concerned, e.g., with how many
times you use assumptions, and do matter in computer science and elsewhere).
➤ Resource-sensitive logics are also called substructural logics, since they lack so-called
structural rules, such as weakening (monotonicity), contraction (delete one of the same
formulae in either side of sequents), exchange (change the order of formulae).
➤ Implicit in regarding both sides of sequents as sets (rather than lists) and in axioms.
➤ Relevant logic and some fuzzy logics are substructural; we shall learn them later on.
STRUCTURAL RULES AND SUBSTRUCTURAL LOGICS
18
➤ Assume that a contradiction is provable.
➤ Then, the empty sequent is provable, since
➤ Thus: if the empty sequent is not provable, the contradiction is not provable.
➤ So, to give a consistency proof, it suffices to show the empty sequent is not provable.
➤ We shall come back to this below. For now, it suffices to understand that the empty
sequent basically means a contradiction.
⊢ A ∧ ¬A
⊢
THE EMPTY SEQUENT AS A CONTRADICTION
⊢ A ∧ ¬A A ∧ ¬A ⊢
A, ¬A ⊢
A ⊢ A
⊢
Cut
∧ ⊢
¬ ⊢
NATURAL DEDUCTION AND SEQUENT CALCULUS (THE CASES ARE SIMILAR)∨
Natural deduction is equivalent to sequent calculus. Consider conjunction. The intro.
rule is equivalent to the right rule (assuming all the other rules are available):
∧I ⊢ ∧
19
X2 ⊢ BX1 ⊢ A
X1, X2 ⊢ A ∧ B
∧I ⇔
X2 ⊢ B, Y2X1 ⊢ A, Y1
X1, X2 ⊢ A ∧ B, Y1, Y2
⊢ ∧
ND AND SC (CONT’D; THE DISJUNCTION CASES ARE SIMILAR)
20
⇔
X, A, B ⊢ Y
X, A ∧ B ⊢ Y
∧ ⊢and
The elim. rule is equivalent to the left rule .∧E1 ∧ ⊢
X ⊢ A ∧ B
X ⊢ A
∧E1
X ⊢ A ∧ B
X ⊢ B
∧E2
ND AND SC (CONT’D; THE DISJUNCTION CASES ARE SIMILAR)
21
A ∧ B ⊢ A ∧ B
A ∧ B ⊢ A ∧ B
X, A ∧ B, B ⊢ Y
∧E1
A ∧ B ⊢ A
A ∧ B ⊢ B
∧E2
Ax.
Ax.
X, A, B ⊢ Y
cut
cut
X, A ∧ B ⊢ Y
Let us prove the left conj. rule from the conj. elim.:
ND AND SC (CONT’D; THE DISJUNCTION CASES ARE SIMILAR)
The other direction: let us prove the conj. elim. rule from the left conj. rule:
We have shown . The proof for is similar; just start with .∧E1 ∧E1 A, B ⊢ B
22
A ∧ B ⊢ A
∧ ⊢
Ax.
A, B ⊢ A
X ⊢ A
X ⊢ A ∧ B cut
NATURAL DEDUCTION AND SEQUENT CALCULUS (CONT’D)
The implication introduction rule →I is equiv. to the right implication rule ⊢→:
23
X, A ⊢ B
X ⊢ A → B
→I ⇔
X, A ⊢ B, Y
X ⊢ A → B, Y
⊢ →
NATURAL DEDUCTION AND SEQUENT CALCULUS (CONT’D)
The imp. elim. rule →E implies the left imp. rule:
24
X1 ⊢ A
X1, X2 ⊢ B
→E
X2 ⊢ A → B
⇒
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
NATURAL DEDUCTION AND SEQUENT CALCULUS (CONT’D)
The converse: the left imp. rule implies the imp. elim. rule →E:
25
X1 ⊢ A
X1, X2 ⊢ B
→E
X2 ⊢ A → B
⇐
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
ND AND SC (CONT’D; THE EXISTENTIAL CASES ARE SIMILAR)
The intro. rule for universal quantifier is essentially already in sequent calculus form:
26
X ⊢ A
X ⊢ ∀xA
∀I ⇔
X ⊢ A, Y
X ⊢ ∀xA, Y
⊢ ∀
ND AND SC (CONT’D; THE EXISTENTIAL CASES ARE SIMILAR)
Applying cut rule once gives the equivalence between the elim. rule and the left rule:
27
X ⊢ ∀xA
X ⊢ A
∀E ⇔
X, A ⊢ Y
X, ∀xA ⊢ Y
∀ ⊢
NATURAL DEDUCTION AND SEQUENT CALCULUS (CONT’D)
The negation introduction rule is equivalent to the right negation rule:
Note: we have monotonicity; on the right of the sequent is equivalent to Y.⊥ , Y
28
X, A ⊢ ⊥
X ⊢ ¬A
¬I ⇔
X, A ⊢ Y
⊢ ¬
X ⊢ ¬A, Y
NATURAL DEDUCTION AND SEQUENT CALCULUS (CONT’D)
In the same way, the negation elimination rule is equivalent to the left negation rule:
29
X1 ⊢ A
X1, X2 ⊢ ⊥
¬E
X2 ⊢ ¬A
⇔
X ⊢ A, Y
¬ ⊢
X, ¬A ⊢ Y
PROOF-THEORETIC DUALITY
In natural deduction, ∧E looks dual to ∨I:
dual to
They are both one-step inferences.
Although ∧I:
is a one-step inference, there is no dual one-step version of ∨E.
A ∧ B ⊢ A A ⊢ A ∨ B
A, B ⊢ A ∧ B
30
PROOF-THEORETIC DUALITY (CONT’D)
When we allow multiple conclusions, we can say that the immediate consequence of
is that one of the two formulae (A or B) is true, without having to say which
one. That is:
dual to
Similar dualities appear for all logical connectives (and quantifiers) in sequent calculus.
A ∨ B
A, B ⊢ A ∧ B A ∨ B ⊢ A, B
31
SEQUENT CALCULUS
32
X, A ⊢ A, Y
Axiom
X, A, B ⊢ Y
X, A ∧ B ⊢ Y
∧ ⊢
X2, B ⊢ Y2X1, A ⊢ Y1
X1, X2, A ∨ B ⊢ Y1, Y2
∨ ⊢
X ⊢ A, Y
¬ ⊢
X, ¬A ⊢ Y
X1 ⊢ A, Y1
X1, X2, A → B ⊢ Y1, Y2
→ ⊢
X2, B ⊢ Y2
X, A ⊢ Y
X, ∀xA ⊢ Y
∀ ⊢
X, A ⊢ Y
X, ∃xA ⊢ Y
∃ ⊢
x does not appear as
a free variable in X,Y
X2 ⊢ B, Y2X1 ⊢ A, Y1
X1, X2 ⊢ A ∧ B, Y1, Y2
⊢ ∧
X ⊢ A, B, Y
X ⊢ A ∨ B, Y
⊢ ∨
X, A ⊢ Y
⊢ ¬
X ⊢ ¬A, Y
X, A ⊢ B, Y
X ⊢ A → B, Y
⊢ →
X ⊢ A, Y
X ⊢ ∀xA, Y
⊢ ∀ x does not appear as a free variable in X,Y
X ⊢ A, Y
X ⊢ ∃xA, Y
⊢ ∃
X2, A ⊢ Y2X1 ⊢ A, Y1
X1, X2 ⊢ Y1, Y2
Cut
X, ⊥ ⊢ Y
⊥ ⊢
X ⊢ ⊤ , Y
⊢ ⊤
COMPLEX EXAMPLE
33
∀x∀y(Rxy → Sxy), ∀x∃y(Fy ∧ ¬Sxy) ⊢ ∀x∃y(Fy ∧ ¬Rxy)
⊢ ∀
∀x∀y(Rxy → Sxy), ∀x∃y(Fy ∧ ¬Sxy) ⊢ ∃y(Fy ∧ ¬Rxy)
∀ ⊢
∀x∀y(Rxy → Sxy), ∃y(Fy ∧ ¬Sxy) ⊢ ∃y(Fy ∧ ¬Rxy)
∃ ⊢
∀x∀y(Rxy → Sxy), Fy ∧ ¬Sxy ⊢ ∃y(Fy ∧ ¬Rxy)
∀ ⊢
∀y(Rxy → Sxy), Fy ∧ ¬Sxy ⊢ ∃y(Fy ∧ ¬Rxy)
∀ ⊢
Rxy → Sxy, Fy ∧ ¬Sxy ⊢ ∃y(Fy ∧ ¬Rxy)
Rxy → Sxy, Fy ∧ ¬Sxy ⊢ Fy ∧ ¬Rxy
⊢ ∃
⊢ ∧
Rxy → Sxy, Fy ∧ ¬Sxy ⊢ Fy Rxy → Sxy, Fy ∧ ¬Sxy ⊢ ¬Rxy
∧ ⊢
Rxy → Sxy, Fy, ¬Sxy ⊢ Fy
→ ⊢
Fy ∧ ¬Sxy ⊢ Rxy, ¬Rxy Fy ∧ ¬Sxy, Sxy ⊢ ¬Rxy
⊢ ¬
Rxy, Fy ∧ ¬Sxy ⊢ Rxy
∧ ⊢
Fy, ¬Sxy, Sxy ⊢ ¬Rxy
¬ ⊢
Fy, Sxy ⊢ ¬Rxy, Sxy
34
➤ Assume there is a proof of .
➤ The cut elimination theorem: any proof can be made cut-free.
➤ So there must be a cut-free proof of .
➤ Any cut-free proof in sequent calculus must have the subformula property.
➤ But any cut-free proof of cannot have the subformula property (since any axiom
include at least one formula, which cannot be a subformula in because it includes no
formula).
➤ Hence: there cannot be a proof of .
➤ Thus: the logic is consistent. Cut elim. and subform. prop. give a consistency proof.
➤ It’s a standard method to prove unprovability of sequnets including the empty one.
⊢
⊢
⊢
⊢
⊢
FINITARY CONSISTENCY PROOF
TWO TRADITIONS IN PROOF THEORY
➤ Natural Deduction: A proof system with introduction and elimination rules which
operate on formulae (cf. categorical judgements in philosophy).
➤ Sequent Calculus: A proof system with left and right rules which operate on
sequents (cf. hypothetical judgments in philosophy) rather than formulae.
➤ Sequent calculus works better for classical logic (the logic you have learned so far).
➤ If you are interested in the ND vs. SC debate in philosophy of logic, see: P. Schroeder-
Heister, The categorical and the hypothetical, Synthese, vol. 187, pp. 925-942, 2012.
➤ It is based on the inferentialist idea that meaning is inherent within a proof system.
Aka. proof-theoretic semantics. Proof theory gives inferentialist semantics.
35
http://www.swedishcollegium.se/subfolders/Fellows/Invited_Fellows/2019-20/schroeder-heister.html
Peter Schroeder-Heister
coined the term “substructural logic”