Sequent calculus

2009-01-18T23:34:11Z

Paolo Tranquilli: /* Sequents and proofs */ edited a minor typo

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

== Formulas ==

Formulas are built on a set of atoms, written <math>\alpha,\beta,\ldots</math>, that can
be either propositional variables <math>X,Y,Z\ldots</math> or atomic formulas
<math>p(t_1,\ldots,t_n)</math>, where the <math>t_i</math> are terms from some first-order language and <math>p</math> is a predicate symbol.
Formulas, represented by capital letters <math>A</math>, <math>B</math>, <math>C</math>, are built using the
following connectives:

{| style="border-spacing: 2em 0"
|-
| <math>\alpha</math>
| atom
| <math>\alpha\orth</math>
| negated atom
| atoms
|-
| <math>A \tens B</math>
| tensor
| <math>A \parr B</math>
| par
| multiplicatives
|-
| <math>\one</math>
| one
| <math>\bot</math>
| bottom
| multiplicative units
|-
| <math>A \plus B</math>
| plus
| <math>A \with B</math>
| with
| additives
|-
| <math>\zero</math>
| zero
| <math>\top</math>
| top
| additive units
|-
| <math>\oc A</math>
| of course
| <math>\wn A</math>
| why not
| exponentials
|-
| <math>\exists \xi.A</math>
| there exists
| <math>\forall \xi.A</math>
| for all
| quantifiers (<math>\xi</math> is a first or second order variable)
|}

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 <math>A</math>'' for <math>\oc A</math> and ''why not <math>A</math>'' for <math>\wn A</math>.
Quantifiers may apply to first- or second-order variables.

Given a formula <math>A</math>, its linear negation, also called ''orthogonal'' and
written <math>A\orth</math>, 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

{|
|-
|align="right"| <math> ( \alpha )\orth </math>
| <math>:= \alpha\orth </math>
|width=30|
|align="right"| <math> ( \alpha\orth )\orth </math>
| <math>:= \alpha </math>
|-
|align="right"| <math> ( A \tens B )\orth </math>
| <math>:= A\orth \parr B\orth </math>
|
|align="right"| <math> ( A \parr B )\orth </math>
| <math>:= A\orth \tens B\orth </math>
|-
|align="right"| <math> \one\orth </math>
| <math>:= \bot </math>
|
|align="right"| <math> \bot\orth </math>
| <math>:= \one </math>
|-
|align="right"| <math> ( A \plus B )\orth </math>
| <math>:= A\orth \with B\orth </math>
|
|align="right"| <math> ( A \with B )\orth </math>
| <math>:= A\orth \plus B\orth </math>
|-
|align="right"| <math> \zero\orth </math>
| <math>:= \top </math>
|
|align="right"| <math> \top\orth </math>
| <math>:= \zero </math>
|-
|align="right"| <math> ( \oc A )\orth </math>
| <math>:= \wn ( A\orth ) </math>
|
|align="right"| <math> ( \wn A )\orth </math>
| <math>:= \oc ( A\orth ) </math>
|-
|align="right"| <math> ( \exists \xi.A )\orth </math>
| <math>:= \forall \xi.( A\orth ) </math>
|
|align="right"| <math> ( \forall \xi.A )\orth </math>
| <math>:= \exists \xi.( A\orth ) </math>
|}

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

There is no connective for implication in the syntax of standard linear logic.
Instead, a ''linear implication'' is defined similarly to the decomposition
<math>A\imp B=\neg A\vee B</math> in classical logic:

<math>
A \limp B := A\orth \parr B
</math>

Free and bound variables are defined in the standard way, as well as
substitution.
Formulas are always considered up to renaming of bound names.
If <math>A</math> and <math>B</math> are formulas and <math>X</math> is a propositional variable, the formula
<math>A[B/X]</math> is <math>A</math> where all atoms <math>X</math> are replaced (without capture) by <math>B</math> and
all atoms <math>X\orth</math> are replaced by the formula <math>B\orth</math>.

== Sequents and proofs ==

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

* Identity group: <math>
\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
</math>

* Multiplicative group: <math>
\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
</math>

* Additive group: <math>
\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
</math>

* Exponential group: <math>
\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
</math>

* Quantifier group (in the <math>\forall</math> rule, <math>\xi</math> must not occur free in <math>\Gamma</math>): <math>
\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
</math>

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 <math>\wn</math>
modality.
This is what distinguishes linear logic from classical logic: if weakening and
contraction were allowed for arbitrary formulas, then <math>\tens</math> and <math>\with</math>
would be identified, as well as <math>\plus</math> and <math>\parr</math>, <math>\one</math> and <math>\top</math>,
<math>\zero</math> and <math>\bot</math>.
By ''identified'', we mean here that replacing a <math>\tens</math> with a <math>\with</math> 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 <math>\zero</math>, the
only ways to introduce it at top level are the axiom rule and the <math>\top</math> 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:

<math>
\AxRule{ \vdash \Gamma, A, B, \Delta }
\LabelRule{exchange}
\UnaRule{ \vdash \Gamma, B, A, \Delta }
\DisplayProof
</math>

== Equivalences and definability ==

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

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

=== Fundamental equivalences ===

* Associativity, commutativity, neutrality: <math>
A \tens (B \tens C) \equiv (A \tens B) \tens C </math> &emsp; <math>
A \tens B \equiv B \tens A </math> &emsp; <math>
A \tens \one \equiv A </math> <math>
A \plus (B \plus C) \equiv (A \plus B) \plus C </math> &emsp; <math>
A \plus B \equiv B \plus A </math> &emsp; <math>
A \plus \zero \equiv A </math>

* Idempotence of additives: <math>
A \plus A \equiv A </math>

* Distributivity of multiplicatives over additives: <math>
A \tens (B \plus C) \equiv (A \tens B) \plus (A \tens C) </math> &emsp; <math>
A \tens \zero \equiv \zero </math>

* Defining property of exponentials: <math>
\oc(A \with B) \equiv \oc A \tens \oc B </math> &emsp; <math>
\oc\top \equiv \one </math>

* Monoidal structure of exponentials, digging: <math>
\oc A \otimes \oc A \equiv \oc A </math> &emsp; <math>
\oc \one \equiv \one </math> &emsp; <math>
\oc\oc A \equiv \oc A </math>

* Commutation of quantifiers (<math>\zeta</math> does not occur in <math>A</math>): <math>
\exists \xi. \exists \psi. A \equiv \exists \psi. \exists \xi. A </math> &emsp; <math>
\exists \xi.(A \plus B) \equiv \exists \xi.A \plus \exists \xi.B </math> &emsp; <math>
\exists \zeta.(A\tens B) \equiv A\tens\exists \zeta.B </math> &emsp; <math>
\exists \zeta.A \equiv A </math>

=== Definability ===

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

<math> \zero \equiv \forall X.X </math> &emsp;
<math> \one \equiv \forall X.(X \limp X) </math> &emsp;
<math> A \plus B \equiv \forall X.(\oc(A \limp X) \limp \oc(B \limp X) \limp X) </math>

=== Additional equivalences ===

<math> \oc\wn\oc\wn A \equiv \oc\wn A </math> &emsp;
<math> \oc\wn \one \equiv \one </math>

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

=== Positive/negative commutation ===

<math>\exists\forall\limp\forall\exists</math>,
<math>A\tens(B\parr C)\limp(A\tens B)\parr C</math>

== 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 ===

{{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.
}}

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|title=subformula|
The subformulas of a formula <math>A</math> are <math>A</math> and, inductively, the subformulas of its immediate subformulas:
* the immediate subformulas of <math>A\tens B</math>, <math>A\parr B</math>, <math>A\plus B</math>, <math>A\with B</math> are <math>A</math> and <math>B</math>,
* the only immediate subformula of <math>\oc A</math> and <math>\wn A</math> is <math>A</math>,
* <math>\one</math>, <math>\bot</math>, <math>\zero</math>, <math>\top</math> and atomic formulas <math>\alpha</math> and <math>\alpha\orth</math> have no immediate subformula,
* the immediate subformulas of <math>\exists x.A</math> and <math>\forall 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> and <math>\forall X.A</math> are all the <math>A[B/X]</math> for all formulas <math>B</math>.
}}

{{Theorem|title=subformula property|
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
formulas of <math>\Gamma</math>.
}}
{{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
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 <math>\Gamma</math> 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|title=consistency|
The empty sequent <math>\vdash</math> is not provable.
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>.
}}
{{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.

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.
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 ===

Let us write <math>\pi\vdash\Gamma</math> to signify that <math>\pi</math> is a proof with
conclusion <math>\vdash\Gamma</math>.

{{Proposition|title=<math>\eta</math>-expansion|
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.
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
<math>\vdash A\orth,A</math> has a cut-free proof in which the axiom rule is used only
for atomic formulas.
We prove this by induction on <math>A</math>.
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=A_1\tens A_2</math> then we have <math>
\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
</math> 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 <math>
\LabelRule{ \one }
\NulRule{ \vdash \one }
\LabelRule{ \bot }
\UnaRule{ \vdash \one, \bot }
\DisplayProof
</math>

* If <math>A=A_1\plus A_2</math> then we have <math>
\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
</math> 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 <math>
\LabelRule{ \top }
\NulRule{ \vdash \top, \zero }
\DisplayProof
</math>

* If <math>A=\oc B</math> then we have <math>
\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
</math> where <math>\pi</math> exists by induction hypothesis.

* If <math>A=\exists X.B</math> then we have <math>
\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
</math> where <math>\pi</math> exists by induction hypothesis.

* First-order quantification works like second-order quantification.
}}

The interesting thing with <math>\eta</math>-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 <math>\top</math> rule).

=== Reversibility ===

{{Definition|title=reversibility|
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,

* if <math>\pi</math> is cut-free then there is a cut-free <math>\pi'</math>.
}}

{{Proposition|
The connectives <math>\parr</math>, <math>\bot</math>, <math>\with</math>, <math>\top</math> and <math>\forall</math> are
reversible.
}}
{{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
or in an instance of the <math>\top</math> rule.

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

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

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

<math>
\AxRule{ \pi_1 \vdash \Delta, A }
\AxRule{ \pi_2 \vdash \Delta, B }
\LabelRule{ \with }
\BinRule{ \vdash \Delta, A \with B }
\DisplayProof
</math>

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

For <math>\top</math> the result is trivial: just choose <math>\pi'</math> as an instance of the
<math>\top</math> rule with the appropriate conclusion.

For <math>\forall</math> at second order, consider a proof <math>\pi\vdash\Gamma,\forall X.A</math>.
Up to renaming, we can assume that <math>X</math> occurs free only above the rule that
introduces the quantifier.
If the quantifier is introduced by a <math>\forall</math> rule, then if we remove this
rule, we can check that we get a proof of <math>\vdash\Gamma,A</math> on which we can
finally apply the <math>\forall</math> rule.
The case when the <math>\forall</math> was introduced in a <math>\top</math> 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 <math>\with</math> 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 <math>\Gamma\vdash\Delta</math>, 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:

<math>
\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
</math>

Identity group:

<math>
\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
</math>

Multiplicative group:

<math>
\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
</math>

Additive group:

<math>
\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
</math>

Exponential group:

<math>
\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
</math>

LLWiki - User contributions [en]

Sequent calculus