Sequent calculus

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Formulas: proper definition of atoms and substitution)
m (minor typos, markup improvement)
Line 140: Line 140:
 
Proofs are labelled trees of sequents, built using the following inference
 
Proofs are labelled trees of sequents, built using the following inference
 
rules:
 
rules:
 
 
* Identity group:<br><math>
 
* Identity group:<br><math>
 
\LabelRule{axiom}
 
\LabelRule{axiom}
Line 152: Line 151:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
 
 
* Multiplicative group:<br><math>
 
* Multiplicative group:<br><math>
 
\AxRule{ \vdash \Gamma, A }
 
\AxRule{ \vdash \Gamma, A }
Line 174: Line 172:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
 
 
* Additive group:<br><math>
 
* Additive group:<br><math>
 
\AxRule{ \vdash \Gamma, A }
 
\AxRule{ \vdash \Gamma, A }
Line 196: Line 193:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
 
 
* Exponential group:<br><math>
 
* Exponential group:<br><math>
 
\AxRule{ \vdash \Gamma, A }
 
\AxRule{ \vdash \Gamma, A }
Line 218: Line 214:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
 
 
* Quantifier group (in the <math>\forall</math> rule, <math>\xi</math> must not occur free in <math>\Gamma</math>):<br><math>
 
* Quantifier group (in the <math>\forall</math> rule, <math>\xi</math> must not occur free in <math>\Gamma</math>):<br><math>
 
\AxRule{ \vdash \Gamma, A[t/x] }
 
\AxRule{ \vdash \Gamma, A[t/x] }
Line 288: Line 283:
 
A \plus B \linequiv B \plus A </math> &emsp; <math>
 
A \plus B \linequiv B \plus A </math> &emsp; <math>
 
A \plus \zero \linequiv A </math>
 
A \plus \zero \linequiv A </math>
 
 
* Idempotence of additives: <br> <math>
 
* Idempotence of additives: <br> <math>
 
A \plus A \linequiv A </math>
 
A \plus A \linequiv A </math>
 
 
* Distributivity of multiplicatives over additives: <br> <math>
 
* Distributivity of multiplicatives over additives: <br> <math>
 
A \tens (B \plus C) \linequiv (A \tens B) \plus (A \tens C) </math> &emsp; <math>
 
A \tens (B \plus C) \linequiv (A \tens B) \plus (A \tens C) </math> &emsp; <math>
 
A \tens \zero \linequiv \zero </math>
 
A \tens \zero \linequiv \zero </math>
 
 
* Defining property of exponentials:<br> <math>
 
* Defining property of exponentials:<br> <math>
 
\oc(A \with B) \linequiv \oc A \tens \oc B </math> &emsp; <math>
 
\oc(A \with B) \linequiv \oc A \tens \oc B </math> &emsp; <math>
 
\oc\top \linequiv \one </math>
 
\oc\top \linequiv \one </math>
+
* Monoidal structure of exponentials, digging:
* Monoidal structure of exponentials, digging: <br> <math>
+
** <math> \oc A \otimes \oc A \linequiv \oc A </math>
\oc A \otimes \oc A \linequiv \oc A </math> &emsp; <math>
+
** <math> \oc \one \linequiv \one </math>
\oc \one \linequiv \one </math> &emsp; <math>
+
** <math> \oc\oc A \linequiv \oc A </math>
\oc\oc A \linequiv \oc A </math>
 
 
 
* Commutation of quantifiers (<math>\zeta</math> does not occur in <math>A</math>): <br> <math>
 
* Commutation of quantifiers (<math>\zeta</math> does not occur in <math>A</math>): <br> <math>
 
\exists \xi. \exists \psi. A \linequiv \exists \psi. \exists \xi. A </math> &emsp; <math>
 
\exists \xi. \exists \psi. A \linequiv \exists \psi. \exists \xi. A </math> &emsp; <math>
Line 313: Line 305:
 
The units and the additive connectives can be defined using second-order
 
The units and the additive connectives can be defined using second-order
 
quantification and exponentials, indeed the following equivalences hold:
 
quantification and exponentials, indeed the following equivalences hold:
+
* <math> \zero \linequiv \forall X.X </math>
<math> \zero \linequiv \forall X.X </math> &emsp;
+
* <math> \one \linequiv \forall X.(X \limp X) </math>
<math> \one \linequiv \forall X.(X \limp X) </math> &emsp;
+
* <math> A \plus B \linequiv \forall X.(\oc(A \limp X) \limp \oc(B \limp X) \limp X) </math>
<math> A \plus B \linequiv \forall X.(\oc(A \limp X) \limp \oc(B \limp X) \limp X) </math>
 
   
 
=== Additional equivalences ===
 
=== Additional equivalences ===
Line 331: Line 323:
   
 
== Properties of proofs ==
 
== Properties of proofs ==
 
The fundamental property of the sequent calculus of linear logic is the cut
 
elimination property, which states that the cut rule is useless as far as
 
provability is concerned.
 
This property is exposed in the following section, together with a sketch of
 
proof.
 
   
 
=== Cut elimination and consequences ===
 
=== Cut elimination and consequences ===
   
 
{{Theorem|title=cut elimination|
 
{{Theorem|title=cut elimination|
For every sequent <math>\vdash\Gamma</math>, there is a proof of <math>\vdash\Gamma</math> if and only if there is a proof of <math>\vdash\Gamma</math> that does not use the cut rule.
+
For every sequent <math>\vdash\Gamma</math>, there is a proof of <math>\vdash\Gamma</math> if and only if there is a proof of <math>\vdash\Gamma</math> that does not use the cut rule.}}
}}
 
   
 
This property is proved using a set of rewriting rules on proofs, using
 
This property is proved using a set of rewriting rules on proofs, using
Line 357: Line 343:
 
* the immediate subformulas of <math>\exists x.A</math> are all the <math>A[t/x]</math> for all first-order terms <math>t</math>,
 
* the immediate subformulas of <math>\exists x.A</math> are all the <math>A[t/x]</math> for all first-order terms <math>t</math>,
 
* the immediate subformulas of <math>\exists X.A</math> are all the <math>A[B/X]</math> for all formulas <math>B</math>,
 
* the immediate subformulas of <math>\exists X.A</math> are all the <math>A[B/X]</math> for all formulas <math>B</math>,
* the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>.
+
* the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>.}}
}}
 
   
 
{{Theorem|title=subformula property|
 
{{Theorem|title=subformula property|
A sequent <math>\vdash\Gamma</math> is provable if and only if it is the conclusion of
+
A sequent <math>\vdash\Gamma</math> is provable if and only if it is the conclusion of a proof in which each intermediate conclusion is made of subformulas of the
a proof in which each intermediate conclusion is made of subformulas of the
+
formulas of <math>\Gamma</math>.}}
formulas of <math>\Gamma</math>.
+
{{Proof|By the cut elimination theorem, if a sequent is provable, then it is provable by a cut-free proof.
}}
 
{{Proof|By the cut elimination theorem, if a sequent <math>\vdash</math> is provable, then it
 
is provable by a cut-free proof.
 
 
In each rule except the cut rule, all formulas of the premisses are either
 
In each rule except the cut rule, all formulas of the premisses are either
 
formulas of the conclusion, or immediate subformulas of it, therefore
 
formulas of the conclusion, or immediate subformulas of it, therefore
cut-free proofs have the subformula property.
+
cut-free proofs have the subformula property.}}
}}
 
   
 
The subformula property means essentially nothing in the second-order system,
 
The subformula property means essentially nothing in the second-order system,
Line 378: Line 364:
 
{{Theorem|title=consistency|
 
{{Theorem|title=consistency|
 
The empty sequent <math>\vdash</math> is not provable.
 
The empty sequent <math>\vdash</math> is not provable.
Subsequently, it is impossible to prove both a formula <math>A</math> and its negation
+
Subsequently, it is impossible to prove both a formula <math>A</math> and its negation <math>A\orth</math>; it is impossible to prove <math>\zero</math> or <math>\bot</math>.}}
<math>A\orth</math>; it is impossible to prove <math>\zero</math> or <math>\bot</math>.
+
{{Proof|If <math>\vdash\Gamma</math> is a provable sequent, then it is the conclusion of a cut-free proof.
}}
+
In each rule except the cut rule, there is at least one formula in conclusion.
{{Proof|
 
If <math>\vdash\Gamma</math> is a provable sequent, then it is the conclusion of a
 
cut-free proof.
 
In each rule except the cut rule, there is at least one formula in
 
conclusion.
 
 
Therefore <math>\vdash</math> cannot be the conclusion of a proof.
 
Therefore <math>\vdash</math> cannot be the conclusion of a proof.
   
The other properties are immediate consequences: if <math>A</math> and <math>A\orth</math> were
+
The other properties are immediate consequences: if <math>A</math> and <math>A\orth</math> were provable, then by a cut rule one would get an empty conclusion, which is not possible.
provable, then by a cut rule one would get an empty conclusion, which is not
+
As particular cases, since <math>\one</math> and <math>\top</math> are provable, their negations <math>\bot</math> and <math>\zero</math> are not.}}
possible.
 
As particular cases, since <math>\one</math> and <math>\top</math> are provable, their negations
 
<math>\bot</math> and <math>\zero</math> are not.
 
}}
 
   
 
=== Expansion of identities ===
 
=== Expansion of identities ===
Line 392: Line 378:
   
 
{{Proposition|title=<math>\eta</math>-expansion|
 
{{Proposition|title=<math>\eta</math>-expansion|
For every proof <math>\pi</math>, there is a proof <math>\pi'</math> with the same conclusion as
+
For every proof <math>\pi</math>, there is a proof <math>\pi'</math> with the same conclusion as <math>\pi</math> in which the axiom rule is only used with atomic formulas.
<math>\pi</math> in which the axiom rule is only used with atomic formulas.
+
If <math>\pi</math> is cut-free, then there is a cut-free <math>\pi'</math>.}}
If <math>\pi</math> is cut-free, then there is a cut-free <math>\pi'</math>.
+
{{Proof|It suffices to prove that for every formula <math>A</math>, the sequent
}}
 
{{Proof|
 
It suffices to prove that for every formula <math>A</math>, the sequent
 
 
<math>\vdash A\orth,A</math> has a cut-free proof in which the axiom rule is used only
 
<math>\vdash A\orth,A</math> has a cut-free proof in which the axiom rule is used only
 
for atomic formulas.
 
for atomic formulas.
 
We prove this by induction on <math>A</math>.
 
We prove this by induction on <math>A</math>.
 
Not that there is a case for each pair of dual connectives.
 
Not that there is a case for each pair of dual connectives.
 
 
* If <math>A</math> is atomic, then <math>\vdash A\orth,A</math> is an instance of the atomic axiom rule.
 
* If <math>A</math> is atomic, then <math>\vdash A\orth,A</math> is an instance of the atomic axiom rule.
 
 
* If <math>A=A_1\tens A_2</math> then we have<br><math>
 
* If <math>A=A_1\tens A_2</math> then we have<br><math>
 
\AxRule{ \pi_1 \vdash A_1\orth, A_1 }
 
\AxRule{ \pi_1 \vdash A_1\orth, A_1 }
Line 411: Line 395:
 
\DisplayProof
 
\DisplayProof
 
</math><br>where <math>\pi_1</math> and <math>\pi_2</math> exist by induction hypothesis.
 
</math><br>where <math>\pi_1</math> and <math>\pi_2</math> exist by induction hypothesis.
 
 
* If <math>A=\one</math> or <math>A=\bot</math> then we have<br><math>
 
* If <math>A=\one</math> or <math>A=\bot</math> then we have<br><math>
 
\LabelRule{ \one }
 
\LabelRule{ \one }
Line 419: Line 402:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
 
 
* If <math>A=A_1\plus A_2</math> then we have<br><math>
 
* If <math>A=A_1\plus A_2</math> then we have<br><math>
 
\AxRule{ \pi_1 \vdash A_1\orth, A_1 }
 
\AxRule{ \pi_1 \vdash A_1\orth, A_1 }
Line 431: Line 413:
 
\DisplayProof
 
\DisplayProof
 
</math><br>where <math>\pi_1</math> and <math>\pi_2</math> exist by induction hypothesis.
 
</math><br>where <math>\pi_1</math> and <math>\pi_2</math> exist by induction hypothesis.
 
 
* If <math>A=\zero</math> or <math>A=\top</math>, we have<br><math>
 
* If <math>A=\zero</math> or <math>A=\top</math>, we have<br><math>
 
\LabelRule{ \top }
 
\LabelRule{ \top }
Line 437: Line 418:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
 
 
* If <math>A=\oc B</math> then we have<br><math>
 
* If <math>A=\oc B</math> then we have<br><math>
 
\AxRule{ \pi \vdash B\orth, B }
 
\AxRule{ \pi \vdash B\orth, B }
Line 446: Line 426:
 
\DisplayProof
 
\DisplayProof
 
</math><br>where <math>\pi</math> exists by induction hypothesis.
 
</math><br>where <math>\pi</math> exists by induction hypothesis.
 
 
* If <math>A=\exists X.B</math> then we have<br><math>
 
* If <math>A=\exists X.B</math> then we have<br><math>
 
\AxRule{ \pi \vdash B\orth, B }
 
\AxRule{ \pi \vdash B\orth, B }
Line 455: Line 434:
 
\DisplayProof
 
\DisplayProof
 
</math><br>where <math>\pi</math> exists by induction hypothesis.
 
</math><br>where <math>\pi</math> exists by induction hypothesis.
+
* First-order quantification works like second-order quantification.}}
* First-order quantification works like second-order quantification.
 
}}
 
   
 
The interesting thing with <math>\eta</math>-expansion is that, we can always assume that
 
The interesting thing with <math>\eta</math>-expansion is that, we can always assume that
Line 465: Line 444:
 
{{Definition|title=reversibility|
 
{{Definition|title=reversibility|
 
A connective <math>c</math> is called ''reversible'' if
 
A connective <math>c</math> is called ''reversible'' if
 
 
* for every proof <math>\pi\vdash\Gamma,c(A_1,\ldots,A_n)</math>, there is a proof <math>\pi'</math> with the same conclusion in which <math>c(A_1,\ldots,A_n)</math> is introduced by the last rule,
 
* for every proof <math>\pi\vdash\Gamma,c(A_1,\ldots,A_n)</math>, there is a proof <math>\pi'</math> with the same conclusion in which <math>c(A_1,\ldots,A_n)</math> is introduced by the last rule,
+
* if <math>\pi</math> is cut-free then there is a cut-free <math>\pi'</math>.}}
* if <math>\pi</math> is cut-free then there is a cut-free <math>\pi'</math>.
 
}}
 
   
 
{{Proposition|
 
{{Proposition|
The connectives <math>\parr</math>, <math>\bot</math>, <math>\with</math>, <math>\top</math> and <math>\forall</math> are
+
The connectives <math>\parr</math>, <math>\bot</math>, <math>\with</math>, <math>\top</math> and <math>\forall</math> are reversible.}}
reversible.
+
{{Proof|Using the <math>\eta</math>-expansion property, we assume that the axiom rule is only applied to atomic formulas.
}}
 
{{Proof|
 
Using the <math>\eta</math>-expansion property, we assume that the axiom rule is only
 
applied to atomic formulas.
 
 
Then each top-level connective is introduced either by its associated rule
 
Then each top-level connective is introduced either by its associated rule
 
or in an instance of the <math>\top</math> rule.
 
or in an instance of the <math>\top</math> rule.
Line 526: Line 504:
 
However, if the original proof has cuts, then the final proof may have more
 
However, if the original proof has cuts, then the final proof may have more
 
cuts, since in the case of <math>\with</math> we duplicated a part of the original
 
cuts, since in the case of <math>\with</math> we duplicated a part of the original
proof.
+
proof.}}
}}
 
   
 
== Variations ==
 
== Variations ==
Line 538: Line 516:
 
connectives, then there are left and right introduction rules and a negation
 
connectives, then there are left and right introduction rules and a negation
 
rule that moves formulas between the left and right sides:
 
rule that moves formulas between the left and right sides:
+
* Negation group:<br><math>
<math>
 
 
\AxRule{ \Gamma, A \vdash \Delta }
 
\AxRule{ \Gamma, A \vdash \Delta }
 
\UnaRule{ \Gamma \vdash A\orth, \Delta }
 
\UnaRule{ \Gamma \vdash A\orth, \Delta }
Line 547: Line 525:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
+
* Identity group:<br><math>
Identity group:
 
 
<math>
 
 
\LabelRule{axiom}
 
\LabelRule{axiom}
 
\NulRule{ A \vdash A }
 
\NulRule{ A \vdash A }
Line 558: Line 536:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
+
* Multiplicative group:<br><math>
Multiplicative group:
 
 
<math>
 
 
\AxRule{ \Gamma, A, B \vdash \Delta }
 
\AxRule{ \Gamma, A, B \vdash \Delta }
 
\LabelRule{ \tens_L }
 
\LabelRule{ \tens_L }
Line 579: Line 557:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
+
* Additive group:<br><math>
Additive group:
 
 
<math>
 
 
\AxRule{ \Gamma, A \vdash \Delta }
 
\AxRule{ \Gamma, A \vdash \Delta }
 
\AxRule{ \Gamma, B \vdash \Delta }
 
\AxRule{ \Gamma, B \vdash \Delta }
Line 600: Line 578:
 
\DisplayProof
 
\DisplayProof
 
</math>
 
</math>
+
* Exponential group:<br><math>
Exponential group:
 
 
<math>
 
 
\AxRule{ \Gamma, A \vdash \Delta }
 
\AxRule{ \Gamma, A \vdash \Delta }
 
\LabelRule{ d }
 
\LabelRule{ d }

Revision as of 13:05, 7 February 2009

This article presents the language and sequent calculus of second-order propositional linear logic and the basic properties of this sequent calculus.

Contents

Formulas

Atomic formulas, written α,β,γ, are predicates of the form p(t_1,\ldots,t_n), where the ti are terms from some first-order language. The predicate symbol p may be either a predicate constant or a second-order variable. By convention we will write first-order variables as x,y,z, second-order variables as X,Y,Z, and ξ for a variable of arbitrary order (see Notations).

Formulas, represented by capital letters A, B, C, are built using the following connectives:

α atom \alpha\orth negated atom atoms
A \tens B tensor A \parr B par multiplicatives
\one one \bot bottom multiplicative units
A \plus B plus A \with B with additives
\zero zero \top top additive units
\oc A of course \wn A why not exponentials
\exists \xi.A there exists \forall \xi.A for all quantifiers

Each line corresponds to a particular class of connectives, and each class consists in a pair of connectives. Those in the left column are called positive and those in the right column are called negative. The tensor and with are conjunctions while par and plus are disjunctions. The exponential connectives are called modalities, and traditionally read of course A for \oc A and why not A for \wn A. Quantifiers may apply to first- or second-order variables.

Given a formula A, its linear negation, also called orthogonal and written A\orth, is obtained by exchanging each positive connective with the negative one of the same class and vice versa, in a way analogous to de Morgan laws in classical logic. Formally, the definition of linear negation is

 ( \alpha )\orth := \alpha\orth  ( \alpha\orth )\orth : = α
 ( A \tens B )\orth := A\orth \parr B\orth  ( A \parr B )\orth := A\orth \tens B\orth
 \one\orth := \bot  \bot\orth := \one
 ( A \plus B )\orth := A\orth \with B\orth  ( A \with B )\orth := A\orth \plus B\orth
 \zero\orth := \top  \top\orth := \zero
 ( \oc A )\orth := \wn ( A\orth )  ( \wn A )\orth := \oc ( A\orth )
 ( \exists \xi.A )\orth := \forall \xi.( A\orth )  ( \forall \xi.A )\orth := \exists \xi.( A\orth )

Note that this operation is defined syntactically, hence negation is not a connective, the only place in formulas where the symbol (\cdot)\orth occurs is for negated atoms \alpha\orth. Note also that, by construction, negation is involutive: for any formula A, it holds that A\biorth=A.

There is no connective for implication in the syntax of standard linear logic. Instead, a linear implication is defined similarly to the decomposition A\imp B=\neg A\vee B in classical logic, as A\limp B:=A\orth\parr B.

Free and bound variables and first-order substitution are defined in the standard way. Formulas are always considered up to renaming of bound names. If A is a formula, X is a second-order variable and B[x_1,\ldots,x_n] is a formula with variables xi, then the formula A[B / X] is A where every atom X(t_1,\ldots,t_n) is replaced by B[t_1,\ldots,t_n] and every atom X(t_1,\ldots,t_n)\orth is replaced by B[t_1,\ldots,t_n]\orth.

Sequents and proofs

A sequent is an expression \vdash\Gamma where Γ is a finite multiset of formulas. For a multiset \Gamma=A_1,\ldots,A_n, the notation \wn\Gamma represents the multiset \wn A_1,\ldots,\wn A_n. Proofs are labelled trees of sequents, built using the following inference rules:

  • Identity group:
    
\LabelRule{axiom}
\NulRule{ \vdash A, A\orth }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Delta, A\orth }
\LabelRule{cut}
\BinRule{ \vdash \Gamma, \Delta }
\DisplayProof
  • Multiplicative group:
    
\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Delta, B }
\LabelRule{ \tens }
\BinRule{ \vdash \Gamma, \Delta, A \tens B }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, A, B }
\LabelRule{ \parr }
\UnaRule{ \vdash \Gamma, A \parr B }
\DisplayProof
\qquad
\LabelRule{ \one }
\NulRule{ \vdash \one }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma }
\LabelRule{ \bot }
\UnaRule{ \vdash \Gamma, \bot }
\DisplayProof
  • Additive group:
    
\AxRule{ \vdash \Gamma, A }
\LabelRule{ \plus_1 }
\UnaRule{ \vdash \Gamma, A \plus B }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, B }
\LabelRule{ \plus_2 }
\UnaRule{ \vdash \Gamma, A \plus B }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Gamma, B }
\LabelRule{ \with }
\BinRule{ \vdash, \Gamma, A \with B }
\DisplayProof
\qquad
\LabelRule{ \top }
\NulRule{ \vdash \Gamma, \top }
\DisplayProof
  • Exponential group:
    
\AxRule{ \vdash \Gamma, A }
\LabelRule{ d }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma }
\LabelRule{ w }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, \wn A, \wn A }
\LabelRule{ c }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof
\qquad
\AxRule{ \vdash \wn\Gamma, B }
\LabelRule{ \oc }
\UnaRule{ \vdash \wn\Gamma, \oc B }
\DisplayProof
  • Quantifier group (in the \forall rule, ξ must not occur free in Γ):
    
\AxRule{ \vdash \Gamma, A[t/x] }
\LabelRule{ \exists^1 }
\UnaRule{ \vdash \Gamma, \exists x.A }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, A[B/X] }
\LabelRule{ \exists^2 }
\UnaRule{ \vdash \Gamma, \exists X.A }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma, A }
\LabelRule{ \forall }
\UnaRule{ \vdash \Gamma, \forall \xi.A }
\DisplayProof

The rules for exponentials are called dereliction, weakening, contraction and promotion, respectively. Note the fundamental fact that there are no contraction and weakening rules for arbitrary formulas, but only for the formulas starting with the \wn modality. This is what distinguishes linear logic from classical logic: if weakening and contraction were allowed for arbitrary formulas, then \tens and \with would be identified, as well as \plus and \parr, \one and \top, \zero and \bot. By identified, we mean here that replacing a \tens with a \with or vice versa would preserve provability.

Note that this system contains only introduction rules and no elimination rule. Moreover, there is no introduction rule for the additive unit \zero, the only ways to introduce it at top level are the axiom rule and the \top rule.

Sequents are considered as multisets, in other words as sequences up to permutation. An equivalent presentation would be to define a sequent as a finite sequence of formulas and to add the exchange rule:


\AxRule{ \vdash \Gamma, A, B, \Delta }
\LabelRule{exchange}
\UnaRule{ \vdash \Gamma, B, A, \Delta }
\DisplayProof

Equivalences and definability

Two formulas A and B are (linearly) equivalent, written A\linequiv B, if both implications A\limp B and B\limp A are provable. Equivalently, A\linequiv B if both \vdash A\orth,B and \vdash B\orth,A are provable. Another formulation of A\linequiv B is that, for all Γ, \vdash\Gamma,A is provable if and only if \vdash\Gamma,B is provable. Note that, because of the definition of negation, an equivalence A\linequiv B holds if and only if the dual equivalence A\orth\linequiv B\orth holds.

Two related notions are isomorphism (stronger than equivalence) and equiprovability (weaker than equivalence).

Fundamental equivalences

  • Associativity, commutativity, neutrality:
    
A \tens (B \tens C) \linequiv (A \tens B) \tens C 
A \tens B \linequiv B \tens A 
A \tens \one \linequiv A
    
A \plus (B \plus C) \linequiv (A \plus B) \plus C 
A \plus B \linequiv B \plus A 
A \plus \zero \linequiv A
  • Idempotence of additives:
    
A \plus A \linequiv A
  • Distributivity of multiplicatives over additives:
    
A \tens (B \plus C) \linequiv (A \tens B) \plus (A \tens C) 
A \tens \zero \linequiv \zero
  • Defining property of exponentials:
    
\oc(A \with B) \linequiv \oc A \tens \oc B 
\oc\top \linequiv \one
  • Monoidal structure of exponentials, digging:
    •  \oc A \otimes \oc A \linequiv \oc A
    •  \oc \one \linequiv \one
    •  \oc\oc A \linequiv \oc A
  • Commutation of quantifiers (ζ does not occur in A):
    
\exists \xi. \exists \psi. A \linequiv \exists \psi. \exists \xi. A 
\exists \xi.(A \plus B) \linequiv \exists \xi.A \plus \exists \xi.B 
\exists \zeta.(A\tens B) \linequiv A\tens\exists \zeta.B 
\exists \zeta.A \linequiv A

Definability

The units and the additive connectives can be defined using second-order quantification and exponentials, indeed the following equivalences hold:

  •  \zero \linequiv \forall X.X
  •  \one \linequiv \forall X.(X \limp X)
  •  A \plus B \linequiv \forall X.(\oc(A \limp X) \limp \oc(B \limp X) \limp X)

Additional equivalences

 \oc\wn\oc\wn A \linequiv \oc\wn A  \oc\wn \one \linequiv \one

Any pair of connectives that has the same rules as \tens/\parr is equivalent to it, the same holds for additives, but not for exponentials.

Positive/negative commutation

\exists\forall\limp\forall\exists, A\tens(B\parr C)\limp(A\tens B)\parr C

Properties of proofs

Cut elimination and consequences

Theorem (cut elimination)

For every sequent \vdash\Gamma, there is a proof of \vdash\Gamma if and only if there is a proof of \vdash\Gamma that does not use the cut rule.

This property is proved using a set of rewriting rules on proofs, using appropriate termination arguments (see the specific articles on cut elimination for detailed proofs), it is the core of the proof/program correspondence.

It has several important consequences:

Definition (subformula)

The subformulas of a formula A are A and, inductively, the subformulas of its immediate subformulas:

  • the immediate subformulas of A\tens B, A\parr B, A\plus B, A\with B are A and B,
  • the only immediate subformula of \oc A and \wn A is A,
  • \one, \bot, \zero, \top and atomic formulas α and \alpha\orth have no immediate subformula,
  • the immediate subformulas of \exists x.A are all the A[t / x] for all first-order terms t,
  • the immediate subformulas of \exists X.A are all the A[B / X] for all formulas B,
  • the only immediate subformula of \forall\xi.A is A.

Theorem (subformula property)

A sequent \vdash\Gamma is provable if and only if it is the conclusion of a proof in which each intermediate conclusion is made of subformulas of the formulas of Γ.

Proof. By the cut elimination theorem, if a sequent is provable, then it is provable by a cut-free proof. In each rule except the cut rule, all formulas of the premisses are either formulas of the conclusion, or immediate subformulas of it, therefore cut-free proofs have the subformula property.

The subformula property means essentially nothing in the second-order system, since any formula is a subformula of a quantified formula where the quantified variable occurs. However, the property is very meaningful if the sequent Γ does not use second-order quantification, as it puts a strong restriction on the set of potential proofs of a given sequent. In particular, it implies that the first-order fragment without quantifiers is decidable.

Theorem (consistency)

The empty sequent \vdash is not provable. Subsequently, it is impossible to prove both a formula A and its negation A\orth; it is impossible to prove \zero or \bot.

Proof. If \vdash\Gamma is a provable sequent, then it is the conclusion of a cut-free proof. In each rule except the cut rule, there is at least one formula in conclusion. Therefore \vdash cannot be the conclusion of a proof.

The other properties are immediate consequences: if A and A\orth were provable, then by a cut rule one would get an empty conclusion, which is not possible. As particular cases, since \one and \top are provable, their negations \bot and \zero are not.

Expansion of identities

Let us write \pi\vdash\Gamma to signify that π is a proof with conclusion \vdash\Gamma.

Proposition (η-expansion)

For every proof π, there is a proof π' with the same conclusion as π in which the axiom rule is only used with atomic formulas. If π is cut-free, then there is a cut-free π'.

Proof. It suffices to prove that for every formula A, the sequent \vdash A\orth,A has a cut-free proof in which the axiom rule is used only for atomic formulas. We prove this by induction on A. Not that there is a case for each pair of dual connectives.

  • If A is atomic, then \vdash A\orth,A is an instance of the atomic axiom rule.
  • If A=A_1\tens A_2 then we have
    
\AxRule{ \pi_1 \vdash A_1\orth, A_1 }
\AxRule{ \pi_2 \vdash A_2\orth, A_2 }
\LabelRule{ \tens }
\BinRule{ \vdash A_1\orth, A_2\orth, A_1 \tens A_2 }
\LabelRule{ \parr }
\UnaRule{ \vdash A_1\orth \parr A_2\orth, A_1 \tens A_2 }
\DisplayProof
    where π1 and π2 exist by induction hypothesis.
  • If A=\one or A=\bot then we have
    
\LabelRule{ \one }
\NulRule{ \vdash \one }
\LabelRule{ \bot }
\UnaRule{ \vdash \one, \bot }
\DisplayProof
  • If A=A_1\plus A_2 then we have
    
\AxRule{ \pi_1 \vdash A_1\orth, A_1 }
\LabelRule{ \plus_1 }
\UnaRule{ \vdash A_1\orth, A_1 \plus A_2 }
\AxRule{ \pi_2 \vdash A_2\orth, A_2 }
\LabelRule{ \plus_2 }
\UnaRule{ \vdash A_2\orth, A_1 \plus A_2 }
\LabelRule{ \with }
\BinRule{ \vdash A_1\orth \with A_2\orth, A_1 \plus A_2 }
\DisplayProof
    where π1 and π2 exist by induction hypothesis.
  • If A=\zero or A=\top, we have
    
\LabelRule{ \top }
\NulRule{ \vdash \top, \zero }
\DisplayProof
  • If A=\oc B then we have
    
\AxRule{ \pi \vdash B\orth, B }
\LabelRule{ d }
\UnaRule{ \pi \vdash \wn B\orth, B }
\LabelRule{ \oc }
\UnaRule{ \pi \vdash \wn B\orth, \oc B }
\DisplayProof
    where π exists by induction hypothesis.
  • If A=\exists X.B then we have
    
\AxRule{ \pi \vdash B\orth, B }
\LabelRule{ \exists }
\UnaRule{ \vdash B\orth, \exists X.B }
\LabelRule{ \forall }
\UnaRule{ \vdash \forall X.B\orth, \exists X.B }
\DisplayProof
    where π exists by induction hypothesis.
  • First-order quantification works like second-order quantification.

The interesting thing with η-expansion is that, we can always assume that each connective is explicitly introduced by its associated rule (except in the case where there is an occurrence of the \top rule).

Reversibility

Definition (reversibility)

A connective c is called reversible if

  • for every proof \pi\vdash\Gamma,c(A_1,\ldots,A_n), there is a proof π' with the same conclusion in which c(A_1,\ldots,A_n) is introduced by the last rule,
  • if π is cut-free then there is a cut-free π'.

Proposition

The connectives \parr, \bot, \with, \top and \forall are reversible.

Proof. Using the η-expansion property, we assume that the axiom rule is only applied to atomic formulas. Then each top-level connective is introduced either by its associated rule or in an instance of the \top rule.

For \parr, consider a proof \pi\vdash\Gamma,A\parr B. If A\parr B is introduced by a \parr rule, then if we remove this rule we get a proof of \vdash\Gamma,A,B (this can be proved by a straightforward induction). If it is introduced in the contect of a \top rule, then this rule can be changed so that A\parr B is replaced by A,B. In either case, we can apply a final \parr rule to get the expected proof.

For \bot, the same technique applies: if it is introduced by a \bot rule, then remove this rule to get a proof of \vdash\Gamma, if it is introduced by a \top rule, remove the \bot from this rule, then apply the \bot rule at the end of the new proof.

For \with, consider a proof \pi\vdash\Gamma,A\with B. If the connective is introduced by a \with rule then this rule is applied in a context like


\AxRule{ \pi_1 \vdash \Delta, A }
\AxRule{ \pi_2 \vdash \Delta, B }
\LabelRule{ \with }
\BinRule{ \vdash \Delta, A \with B }
\DisplayProof

Since the formula A\with B is not involved in other rules (except as context), if we replace this step by π1 in π we finally get a proof \pi'_1\vdash\Gamma,A. If we replace this step by π2 we get a proof \pi'_2\vdash\Gamma,B. Combining π1 and π2 with a final \with rule we finally get the expected proof. The case when the \with was introduced in a \top rule is solved as before.

For \top the result is trivial: just choose π' as an instance of the \top rule with the appropriate conclusion.

For \forall at second order, consider a proof \pi\vdash\Gamma,\forall X.A. Up to renaming, we can assume that X occurs free only above the rule that introduces the quantifier. If the quantifier is introduced by a \forall rule, then if we remove this rule, we can check that we get a proof of \vdash\Gamma,A on which we can finally apply the \forall rule. The case when the \forall was introduced in a \top rule is solved as before. First-order quantification is similar.

Note that, in each case, if the proof we start from is cut-free, our transformations do not introduce a cut rule. However, if the original proof has cuts, then the final proof may have more cuts, since in the case of \with we duplicated a part of the original proof.

Variations

Two-sided sequent calculus

The sequent calculus of linear logic can also be presented using two-sided sequents \Gamma\vdash\Delta, with any number of formulas on the left and right. In this case, it is customary to provide rules only for the positive connectives, then there are left and right introduction rules and a negation rule that moves formulas between the left and right sides:

  • Negation group:
    
\AxRule{ \Gamma, A \vdash \Delta }
\UnaRule{ \Gamma \vdash A\orth, \Delta }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash A, \Delta }
\UnaRule{ \Gamma, A\orth \vdash \Delta }
\DisplayProof
  • Identity group:
    
\LabelRule{axiom}
\NulRule{ A \vdash A }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash A, \Delta }
\AxRule{ \Gamma', A \vdash \Delta' }
\LabelRule{cut}
\BinRule{ \Gamma, \Gamma' \vdash \Delta, \Delta' }
\DisplayProof
  • Multiplicative group:
    
\AxRule{ \Gamma, A, B \vdash \Delta }
\LabelRule{ \tens_L }
\UnaRule{ \Gamma, A \tens B \vdash \Delta }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash A, \Delta }
\AxRule{ \Gamma' \vdash B, \Delta' }
\LabelRule{ \tens_R }
\BinRule{ \Gamma, \Gamma' \vdash A \tens B, \Delta, \Delta' }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash \Delta }
\LabelRule{ \one_L }
\UnaRule{ \Gamma, \one \vdash \Delta }
\DisplayProof
\qquad
\LabelRule{ \one_R }
\NulRule{ \vdash \one }
\DisplayProof
  • Additive group:
    
\AxRule{ \Gamma, A \vdash \Delta }
\AxRule{ \Gamma, B \vdash \Delta }
\LabelRule{ \plus_L }
\BinRule{ \Gamma, A \plus B \vdash \Delta }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash A, \Delta }
\LabelRule{ \plus_{R1} }
\UnaRule{ \Gamma \vdash A \plus B, \Delta }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash B, \Delta }
\LabelRule{ \plus_{R2} }
\UnaRule{ \Gamma \vdash A \plus B, \Delta }
\DisplayProof
\qquad
\LabelRule{ \zero_L }
\NulRule{ \Gamma, \zero \vdash \Delta }
\DisplayProof
  • Exponential group:
    
\AxRule{ \Gamma, A \vdash \Delta }
\LabelRule{ d }
\UnaRule{ \Gamma, \oc A \vdash \Delta }
\DisplayProof
\qquad
\AxRule{ \Gamma \vdash \Delta }
\LabelRule{ w }
\UnaRule{ \Gamma, \oc A \vdash \Delta }
\DisplayProof
\qquad
\AxRule{ \Gamma, \oc A, \oc A \vdash \Delta }
\LabelRule{ c }
\UnaRule{ \Gamma, \oc A \vdash \Delta }
\DisplayProof
\qquad
\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B }
\LabelRule{ \oc_R }
\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B }
\DisplayProof
Personal tools