Intuitionistic Linear Logic (<math>ILL</math>) is the
[[intuitionnistic restriction]] of linear logic: the sequent calculus
of <math>ILL</math> is obtained from the [[Sequent calculus#Sequents and proofs|two-sided sequent calculus of
linear logic]] by constraining sequents to have exactly one formula on
the right-hand side: <math>\Gamma\vdash A</math>.

The connectives <math>\parr</math>, <math>\bot</math> and <math>\wn</math> are
not available anymore, but the linear implication <math>\limp</math> is.

== Sequent Calculus ==

<math>
\LabelRule{\rulename{ax}}
\NulRule{A\vdash A}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A}
\AxRule{\Delta,A\vdash C}
\LabelRule{\rulename{cut}}
\BinRule{\Gamma,\Delta\vdash C}
\DisplayProof
</math>

 

<math>
\AxRule{\Gamma\vdash A}
\AxRule{\Delta\vdash B}
\LabelRule{\tens R}
\BinRule{\Gamma,\Delta\vdash A\tens B}
\DisplayProof
\qquad
\AxRule{\Gamma,A,B\vdash C}
\LabelRule{\tens L}
\UnaRule{\Gamma,A\tens B\vdash C}
\DisplayProof
\qquad
\LabelRule{\one R}
\NulRule{{}\vdash\one}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash C}
\LabelRule{\one L}
\UnaRule{\Gamma,\one\vdash C}
\DisplayProof
</math>

 

<math>
\AxRule{\Gamma,A\vdash B}
\LabelRule{\limp R}
\UnaRule{\Gamma\vdash A\limp B}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A}
\AxRule{\Delta,B\vdash C}
\LabelRule{\limp L}
\BinRule{\Gamma,\Delta,A\limp B\vdash C}
\DisplayProof
</math>

 

<math>
\AxRule{\Gamma\vdash A}
\AxRule{\Gamma\vdash B}
\LabelRule{\with R}
\BinRule{\Gamma\vdash A\with B}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\with_1 L}
\UnaRule{\Gamma,A\with B\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma,B\vdash C}
\LabelRule{\with_2 L}
\UnaRule{\Gamma,A\with B\vdash C}
\DisplayProof
\qquad
\LabelRule{\top R}
\NulRule{\Gamma\vdash\top}
\DisplayProof
</math>

 

<math>
\AxRule{\Gamma\vdash A}
\LabelRule{\plus_1 R}
\UnaRule{\Gamma\vdash A\plus B}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash B}
\LabelRule{\plus_2 R}
\UnaRule{\Gamma\vdash A\plus B}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\AxRule{\Gamma,B\vdash C}
\LabelRule{\plus L}
\BinRule{\Gamma,A\plus B\vdash C}
\DisplayProof
\qquad
\LabelRule{\zero L}
\NulRule{\Gamma,\zero\vdash C}
\DisplayProof
</math>

 

<math>
\AxRule{\oc{\Gamma}\vdash A}
\LabelRule{\oc R}
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\oc d L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma,\oc{A},\oc{A}\vdash C}
\LabelRule{\oc c L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash C}
\LabelRule{\oc w L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
</math>

 

<math>
\AxRule{\Gamma\vdash A}
\LabelRule{\forall R}
\UnaRule{\Gamma\vdash \forall\xi A}
\DisplayProof
\qquad
\AxRule{\Gamma,A[\tau/\xi]\vdash C}
\LabelRule{\forall L}
\UnaRule{\Gamma,\forall\xi A\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A[\tau/\xi]}
\LabelRule{\exists R}
\UnaRule{\Gamma\vdash\exists\xi A}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\exists L}
\UnaRule{\Gamma,\exists\xi A\vdash C}
\DisplayProof
</math>

with <math>\xi</math> not free in <math>\Gamma,C</math> in the rules <math>\forall R</math> and <math>\exists L</math>.

== The intuitionistic fragment of linear logic ==

In order to characterize intuitionistic linear logic inside linear logic, we define the intuitionistic restriction of linear formulas:

<math>
J ::= X \mid J\tens J \mid \one \mid J\limp J \mid J\with J \mid \top \mid J\plus J \mid \zero \mid \oc{J} \mid \forall\xi J \mid \exists\xi J
</math>

<math>JLL</math> is the [[fragment]] of linear logic obtained by restriction to intuitionistic formulas.

{{Proposition|title=From <math>ILL</math> to <math>JLL</math>|
If <math>\Gamma\vdash A</math> is provable in <math>ILL_{012}</math>, it is provable in <math>JLL_{012}</math>.
}}

{{Proof|
<math>ILL_{012}</math> is included in <math>JLL_{012}</math>.
}}

{{Theorem|title=From <math>JLL</math> to <math>ILL</math>|
If <math>\Gamma\vdash\Delta</math> is provable in <math>JLL_{12}</math>, it is provable in <math>ILL_{12}</math>.
}}

{{Proof|
We only prove the first order case, a proof of the full result is given in the PhD thesis of Harold Schellinx<ref>{{BibEntry|bibtype=phdthesis|author=Schellinx, Harold|title=The Noble Art of Linear Decorating|type=Dissertation series of the Dutch Institute for Logic, Language and Computation|school=University of Amsterdam|note=ILLC-Dissertation Series, 1994-1|year=1994}}</ref>.

Consider a cut-free proof of <math>\Gamma\vdash\Delta</math> in <math>JLL_{12}</math>, we can prove by induction on the length of such a proof that it belongs to <math>ILL_{12}</math>.
}}

{{Corollary|title=Unique conclusion in <math>JLL</math>|
If <math>\Gamma\vdash\Delta</math> is provable in <math>JLL_{12}</math> then <math>\Delta</math> is a singleton.
}}

The theorem is also valid for formulas containing <math>\one</math> but not anymore with <math>\top</math> and <math>\zero</math>. <math>{}\vdash((X\limp Y)\limp\zero)\limp(X\tens\top)</math> is provable in <math>JLL_0</math>:

<math>
\LabelRule{\rulename{ax}}
\NulRule{X\vdash X}
\LabelRule{\top R}
\NulRule{{}\vdash Y,\top}
\LabelRule{\tens R}
\BinRule{X\vdash Y,X\tens\top}
\LabelRule{\limp R}
\UnaRule{{}\vdash X\limp Y,X\tens\top}
\LabelRule{\zero L}
\NulRule{\zero\vdash {}}
\LabelRule{\limp L}
\BinRule{(X\limp Y)\limp\zero\vdash X\tens\top}
\LabelRule{\limp R}
\UnaRule{{}\vdash((X\limp Y)\limp\zero)\limp(X\tens\top)}
\DisplayProof
</math>

but not in <math>ILL_0</math>.

== Input / output polarities ==

In order to go to <math>LL</math> without <math>\limp</math>, we consider two classes of formulas: ''input formulas'' (<math>I</math>) and ''output formulas'' (<math>O</math>).

<math>
I ::= X\orth \mid I\parr I \mid \bot \mid I\tens O \mid O\tens I \mid I\plus I \mid \zero \mid I\with I \mid \top \mid \wn{I} \mid \exists\xi I \mid \forall\xi I
</math>
<math>
O ::= X \mid O\tens O \mid \one \mid O\parr I \mid I\parr O \mid O\with O \mid \top \mid O\plus O \mid \zero \mid \oc{O} \mid \forall\xi O \mid \exists\xi O
</math>

By applying the definition of the linear implication <math>A\limp B = A\orth\parr B</math>, any formula of <math>JLL</math> is mapped to an output formula (and the dual of a <math>JLL</math> formula to an input formula). Conversely, any output formula is coming from a <math>JLL</math> formula in this way (up to commutativity of <math>\parr</math>: <math>O\parr I = I\parr O</math>).

The [[fragment]] of linear logic obtained by restriction to input/output formulas is thus equivalent to <math>JLL</math>, but the closure of the set of input/output formulas under orthogonal allows for a one-sided presentation.

<math>
\LabelRule{\rulename{ax}}
\NulRule{\vdash O\orth,O}
\DisplayProof
\qquad
\AxRule{{}\vdash \Gamma,O}
\AxRule{{}\vdash\Delta,O\orth}
\LabelRule{\rulename{cut}}
\BinRule{{}\vdash\Gamma,\Delta}
\DisplayProof
</math>

 

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

 

<math>
\AxRule{{}\vdash\Gamma,A}
\AxRule{{}\vdash\Gamma,B}
\LabelRule{\with}
\BinRule{{}\vdash\Gamma,A\with B}
\DisplayProof
\qquad
\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
\LabelRule{\top}
\NulRule{{}\vdash\Gamma,\top}
\DisplayProof
</math>

 

<math>
\AxRule{{}\vdash\wn{\Gamma},O}
\LabelRule{\oc}
\UnaRule{{}\vdash\wn{\Gamma},\oc{O}}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,I}
\LabelRule{\wn d}
\UnaRule{{}\vdash\Gamma,\wn{I}}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,\wn{I},\wn{I}}
\LabelRule{\wn c}
\UnaRule{{}\vdash\Gamma,\wn{I}}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma}
\LabelRule{\wn w}
\UnaRule{{}\vdash\Gamma,\wn{I}}
\DisplayProof
</math>

 

<math>
\AxRule{{}\vdash\Gamma,A}
\LabelRule{\forall}
\UnaRule{{}\vdash\Gamma,\forall\xi A}
\DisplayProof
\qquad
\AxRule{{}\vdash\Gamma,A[\tau/\xi]}
\LabelRule{\exists}
\UnaRule{{}\vdash\Gamma,\exists\xi A}
\DisplayProof
</math>

with <math>A</math> and <math>B</math> arbitrary input or output formulas (under the condition that the composite formulas containing them are input or output formulas) and <math>\xi</math> not free in <math>\Gamma</math> in the rule <math>\forall</math>.

{{Lemma|title=Output formula|
If <math>{}\vdash\Gamma</math> is provable in <math>LL_{12}</math> and contains only input and output formulas, then <math>\Gamma</math> contains exactly one output formula.
}}

{{Proof|
Assume <math>\Gamma_O</math> is obtained by turning the output formulas of <math>\Gamma</math> into <math>JLL</math> formulas and <math>\Gamma_I</math> is obtained by turning the dual of the input formulas of <math>\Gamma</math> into <math>JLL</math> formulas, <math>\Gamma_I\vdash\Gamma_O</math> is provable in <math>LL_{12}</math> thus in <math>JLL_{12}</math>. By corollary (Unique conclusion in <math>JLL</math>), <math>\Gamma_O</math> is a singleton, thus <math>\Gamma</math> contains exactly one output formula.
}}

== References ==
<references />

Positive formula

2013-10-28T17:49:42Z

Olivier Laurent: /* Generalized structural rules */ Link to wikipedia:comoind

A ''positive formula'' is a formula <math>P</math> such that <math>P\limp\oc P</math> (thus a [[Wikipedia:F-coalgebra|coalgebra]] for the [[Wikipedia:Comonad|comonad]] <math>\oc</math>). As a consequence <math>P</math> and <math>\oc P</math> are [[Sequent calculus#Equivalences|equivalent]].

A formula <math>P</math> is positive if and only if <math>P\orth</math> is [[Negative formula|negative]].

== Positive connectives ==

A connective <math>c</math> of arity <math>n</math> is ''positive'' if for any positive formulas <math>P_1</math>,...,<math>P_n</math>, <math>c(P_1,\dots,P_n)</math> is positive.

{{Proposition|title=Positive connectives|
<math>\tens</math>, <math>\one</math>, <math>\plus</math>, <math>\zero</math>, <math>\oc</math> and <math>\exists</math> are positive connectives.
}}

{{Proof|
<math>
\AxRule{P_2\vdash\oc{P_2}}
\AxRule{P_1\vdash\oc{P_1}}
\LabelRule{\rulename{ax}}
\NulRule{P_1\vdash P_1}
\LabelRule{\rulename{ax}}
\NulRule{P_2\vdash P_2}
\LabelRule{\tens R}
\BinRule{P_1,P_2\vdash P_1\tens P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_1},P_2\vdash P_1\tens P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_1},\oc{P_2}\vdash P_1\tens P_2}
\LabelRule{\oc R}
\UnaRule{\oc{P_1},\oc{P_2}\vdash\oc{(P_1\tens P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_1,\oc{P_2}\vdash\oc{(P_1\tens P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_1,P_2\vdash\oc{(P_1\tens P_2)}}
\LabelRule{\tens L}
\UnaRule{P_1\tens P_2\vdash\oc{(P_1\tens P_2)}}
\DisplayProof
</math>

 

<math>
\LabelRule{\one R}
\NulRule{\vdash\one}
\LabelRule{\oc R}
\UnaRule{\vdash\oc{\one}}
\LabelRule{\one L}
\UnaRule{\one\vdash\oc{\one}}
\DisplayProof
</math>

 

<math>
\AxRule{P_1\vdash\oc{P_1}}
\LabelRule{\rulename{ax}}
\NulRule{P_1\vdash P_1}
\LabelRule{\plus_1 R}
\UnaRule{P_1\vdash P_1\plus P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_1}\vdash P_1\plus P_2}
\LabelRule{\oc R}
\UnaRule{\oc{P_1}\vdash\oc{(P_1\plus P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_1\vdash\oc{(P_1\plus P_2)}}
\AxRule{P_2\vdash\oc{P_2}}
\LabelRule{\rulename{ax}}
\NulRule{P_2\vdash P_2}
\LabelRule{\plus_2 R}
\UnaRule{P_2\vdash P_1\plus P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_2}\vdash P_1\plus P_2}
\LabelRule{\oc R}
\UnaRule{\oc{P_2}\vdash\oc{(P_1\plus P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_2\vdash\oc{(P_1\plus P_2)}}
\LabelRule{\plus L}
\BinRule{P_1\plus P_2\vdash\oc{(P_1\plus P_2)}}
\DisplayProof
</math>

 

<math>
\LabelRule{\zero L}
\NulRule{\zero\vdash\oc{\zero}}
\DisplayProof
</math>

 

<math>
\LabelRule{\rulename{ax}}
\NulRule{\oc{P}\vdash\oc{P}}
\LabelRule{\oc R}
\UnaRule{\oc{P}\vdash\oc{\oc{P}}}
\DisplayProof
</math>

 

<math>
\AxRule{P\vdash\oc{P}}
\LabelRule{\rulename{ax}}
\NulRule{P\vdash P}
\LabelRule{\exists R}
\UnaRule{P\vdash \exists\xi P}
\LabelRule{\oc d L}
\UnaRule{\oc{P}\vdash \exists\xi P}
\LabelRule{\oc R}
\UnaRule{\oc{P}\vdash\oc{\exists\xi P}}
\LabelRule{\rulename{cut}}
\BinRule{P\vdash\oc{\exists\xi P}}
\LabelRule{\exists L}
\UnaRule{\exists\xi P\vdash\oc{\exists\xi P}}
\DisplayProof
</math>
}}

More generally, <math>\oc A</math> is positive for any formula <math>A</math>.

The notion of positive connective is related with but different from the notion of [[asynchronous connective]].

== Generalized structural rules ==

Positive formulas admit generalized left structural rules corresponding to a structure of [[Wikipedia:Comonoid|<math>\tens</math>-comonoid]]: <math>P\limp P\tens P</math> and <math>P\limp\one</math>. The following rule is derivable:

<math>
\AxRule{\Gamma,P,P\vdash\Delta}
\LabelRule{+ c L}
\UnaRule{\Gamma,P\vdash\Delta}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash\Delta}
\LabelRule{+ w L}
\UnaRule{\Gamma,P\vdash\Delta}
\DisplayProof
</math>

{{Proof|
<math>
\AxRule{P\vdash\oc{P}}
\AxRule{\Gamma,P,P\vdash\Delta}
\LabelRule{\oc L}
\UnaRule{\Gamma,P,\oc P\vdash\Delta}
\LabelRule{\oc L}
\UnaRule{\Gamma,\oc P,\oc P\vdash\Delta}
\LabelRule{\oc c L}
\UnaRule{\Gamma,\oc P\vdash\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\Gamma,P\vdash\Delta}
\DisplayProof
</math>

 

<math>
\AxRule{P\vdash\oc{P}}
\AxRule{\Gamma\vdash\Delta}
\LabelRule{\oc w L}
\UnaRule{\Gamma,\oc P\vdash\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\Gamma,P\vdash\Delta}
\DisplayProof
</math>
}}

Positive formulas are also acceptable in the left-hand side context of the promotion rule. The following rule is derivable:

<math>
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
\LabelRule{+ \oc R}
\UnaRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}
\DisplayProof
</math>

{{Proof|
<math>
\AxRule{P_1\vdash\oc{P_1}}
\AxRule{P_n\vdash\oc{P_n}}
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
\LabelRule{\oc L}
\UnaRule{\oc\Gamma,P_1,\dots,P_{n-1},\oc{P_n}\vdash A,\wn\Delta}
\VdotsRule{}{\oc\Gamma,P_1,\oc{P_2},\dots,\oc{P_n}\vdash A,\wn\Delta}
\LabelRule{\oc L}
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash A,\wn\Delta}
\LabelRule{\oc R}
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_{n-1}},P_n\vdash \oc{A},\wn\Delta}
\VdotsRule{}{\oc\Gamma,\oc{P_1},P_2,\dots,P_n\vdash \oc{A},\wn\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}
\DisplayProof
</math>
}}

Positive formula

2013-10-28T17:43:54Z

Olivier Laurent: Added link to negative formulas

A ''positive formula'' is a formula <math>P</math> such that <math>P\limp\oc P</math> (thus a [[Wikipedia:F-coalgebra|coalgebra]] for the [[Wikipedia:Comonad|comonad]] <math>\oc</math>). As a consequence <math>P</math> and <math>\oc P</math> are [[Sequent calculus#Equivalences|equivalent]].

A formula <math>P</math> is positive if and only if <math>P\orth</math> is [[Negative formula|negative]].

== Positive connectives ==

A connective <math>c</math> of arity <math>n</math> is ''positive'' if for any positive formulas <math>P_1</math>,...,<math>P_n</math>, <math>c(P_1,\dots,P_n)</math> is positive.

{{Proposition|title=Positive connectives|
<math>\tens</math>, <math>\one</math>, <math>\plus</math>, <math>\zero</math>, <math>\oc</math> and <math>\exists</math> are positive connectives.
}}

{{Proof|
<math>
\AxRule{P_2\vdash\oc{P_2}}
\AxRule{P_1\vdash\oc{P_1}}
\LabelRule{\rulename{ax}}
\NulRule{P_1\vdash P_1}
\LabelRule{\rulename{ax}}
\NulRule{P_2\vdash P_2}
\LabelRule{\tens R}
\BinRule{P_1,P_2\vdash P_1\tens P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_1},P_2\vdash P_1\tens P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_1},\oc{P_2}\vdash P_1\tens P_2}
\LabelRule{\oc R}
\UnaRule{\oc{P_1},\oc{P_2}\vdash\oc{(P_1\tens P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_1,\oc{P_2}\vdash\oc{(P_1\tens P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_1,P_2\vdash\oc{(P_1\tens P_2)}}
\LabelRule{\tens L}
\UnaRule{P_1\tens P_2\vdash\oc{(P_1\tens P_2)}}
\DisplayProof
</math>

 

<math>
\LabelRule{\one R}
\NulRule{\vdash\one}
\LabelRule{\oc R}
\UnaRule{\vdash\oc{\one}}
\LabelRule{\one L}
\UnaRule{\one\vdash\oc{\one}}
\DisplayProof
</math>

 

<math>
\AxRule{P_1\vdash\oc{P_1}}
\LabelRule{\rulename{ax}}
\NulRule{P_1\vdash P_1}
\LabelRule{\plus_1 R}
\UnaRule{P_1\vdash P_1\plus P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_1}\vdash P_1\plus P_2}
\LabelRule{\oc R}
\UnaRule{\oc{P_1}\vdash\oc{(P_1\plus P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_1\vdash\oc{(P_1\plus P_2)}}
\AxRule{P_2\vdash\oc{P_2}}
\LabelRule{\rulename{ax}}
\NulRule{P_2\vdash P_2}
\LabelRule{\plus_2 R}
\UnaRule{P_2\vdash P_1\plus P_2}
\LabelRule{\oc d L}
\UnaRule{\oc{P_2}\vdash P_1\plus P_2}
\LabelRule{\oc R}
\UnaRule{\oc{P_2}\vdash\oc{(P_1\plus P_2)}}
\LabelRule{\rulename{cut}}
\BinRule{P_2\vdash\oc{(P_1\plus P_2)}}
\LabelRule{\plus L}
\BinRule{P_1\plus P_2\vdash\oc{(P_1\plus P_2)}}
\DisplayProof
</math>

 

<math>
\LabelRule{\zero L}
\NulRule{\zero\vdash\oc{\zero}}
\DisplayProof
</math>

 

<math>
\LabelRule{\rulename{ax}}
\NulRule{\oc{P}\vdash\oc{P}}
\LabelRule{\oc R}
\UnaRule{\oc{P}\vdash\oc{\oc{P}}}
\DisplayProof
</math>

 

<math>
\AxRule{P\vdash\oc{P}}
\LabelRule{\rulename{ax}}
\NulRule{P\vdash P}
\LabelRule{\exists R}
\UnaRule{P\vdash \exists\xi P}
\LabelRule{\oc d L}
\UnaRule{\oc{P}\vdash \exists\xi P}
\LabelRule{\oc R}
\UnaRule{\oc{P}\vdash\oc{\exists\xi P}}
\LabelRule{\rulename{cut}}
\BinRule{P\vdash\oc{\exists\xi P}}
\LabelRule{\exists L}
\UnaRule{\exists\xi P\vdash\oc{\exists\xi P}}
\DisplayProof
</math>
}}

More generally, <math>\oc A</math> is positive for any formula <math>A</math>.

The notion of positive connective is related with but different from the notion of [[asynchronous connective]].

== Generalized structural rules ==

Positive formulas admit generalized left structural rules corresponding to a structure of <math>\tens</math>-comonoid: <math>P\limp P\tens P</math> and <math>P\limp\one</math>. The following rule is derivable:

<math>
\AxRule{\Gamma,P,P\vdash\Delta}
\LabelRule{+ c L}
\UnaRule{\Gamma,P\vdash\Delta}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash\Delta}
\LabelRule{+ w L}
\UnaRule{\Gamma,P\vdash\Delta}
\DisplayProof
</math>

{{Proof|
<math>
\AxRule{P\vdash\oc{P}}
\AxRule{\Gamma,P,P\vdash\Delta}
\LabelRule{\oc L}
\UnaRule{\Gamma,P,\oc P\vdash\Delta}
\LabelRule{\oc L}
\UnaRule{\Gamma,\oc P,\oc P\vdash\Delta}
\LabelRule{\oc c L}
\UnaRule{\Gamma,\oc P\vdash\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\Gamma,P\vdash\Delta}
\DisplayProof
</math>

 

<math>
\AxRule{P\vdash\oc{P}}
\AxRule{\Gamma\vdash\Delta}
\LabelRule{\oc w L}
\UnaRule{\Gamma,\oc P\vdash\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\Gamma,P\vdash\Delta}
\DisplayProof
</math>
}}

Positive formulas are also acceptable in the left-hand side context of the promotion rule. The following rule is derivable:

<math>
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
\LabelRule{+ \oc R}
\UnaRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}
\DisplayProof
</math>

{{Proof|
<math>
\AxRule{P_1\vdash\oc{P_1}}
\AxRule{P_n\vdash\oc{P_n}}
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
\LabelRule{\oc L}
\UnaRule{\oc\Gamma,P_1,\dots,P_{n-1},\oc{P_n}\vdash A,\wn\Delta}
\VdotsRule{}{\oc\Gamma,P_1,\oc{P_2},\dots,\oc{P_n}\vdash A,\wn\Delta}
\LabelRule{\oc L}
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash A,\wn\Delta}
\LabelRule{\oc R}
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_{n-1}},P_n\vdash \oc{A},\wn\Delta}
\VdotsRule{}{\oc\Gamma,\oc{P_1},P_2,\dots,P_n\vdash \oc{A},\wn\Delta}
\LabelRule{\rulename{cut}}
\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}
\DisplayProof
</math>
}}

Provable formulas

2013-10-28T15:02:09Z

Olivier Laurent: /* Monoidality of exponential */ Duals added

List of equivalences

2013-10-28T14:57:46Z

Olivier Laurent: Exponentials added

Each [[List of isomorphisms|isomorphism]] gives an equivalence of formulas.
The following equivalences are not isomorphisms.

== Additives ==

<math>
\begin{array}{rclcrcl}
A \with A &\linequiv& A \\
A \plus A &\linequiv& A \\
\\
A \with (A \plus B) &\linequiv& A &\quad& A \plus \top &\linequiv& \top \\
A \plus (A \with B) &\linequiv& A &\quad& A \with \zero &\linequiv& \zero
\end{array}
</math>

== Quantifiers ==

<math>
\begin{array}{rcll}
\forall X.A &\linequiv& A &\quad (X\notin A) \\
\exists X.A &\linequiv& A &\quad (X\notin A)
\end{array}
</math>

== Exponentials ==

<math>
\begin{array}{rclcrcl}
\oc A &\linequiv& \oc A\tens\oc A &\quad&
\wn A &\linequiv& \wn A\parr\wn A\\
\oc A &\linequiv& \oc\oc A &\quad& \wn A &\linequiv& \wn\wn A\\
\oc\wn A &\linequiv& \oc\wn\oc\wn A &\quad& \wn\oc A &\linequiv& \wn\oc\wn\oc A\\
\end{array}
</math>

Some of these equivalences are related with the [[lattice of exponential modalities]].

== Polarities ==

{|
| <math> \wn N \linequiv N </math>
|   (N [[Negative formula|negative]])
|-
| <math> \oc P \linequiv P </math>
|   (P [[Positive formula|positive]])
|-
| <math> \wn\oc R \linequiv R </math>
|   (R [[Regular formula|regular]])
|-
| <math> \oc\wn L \linequiv L </math>
|   (L [[Co-regular formula|co-regular]])
|}

== Second order encodings ==

<math>
\begin{array}{rclcrcl}
A &\linequiv &\forall X . (A \tens X\orth) \parr X \\
A &\linequiv &\exists X . (A \parr X\orth) \tens X \\
\\
A \with B &\linequiv& \exists X . \oc{(A \parr X\orth)} \tens \oc{(B \parr X\orth)} \tens X &\quad& \top &\linequiv& \exists X . X \\
A \plus B &\linequiv& \forall X . \wn{(A \tens X\orth)} \parr \wn{(B \tens X\orth)} \parr X &\quad& \zero &\linequiv& \forall X . X \\
\\
\bot &\linequiv& \exists X . X\tens X\orth \\
\one &\linequiv& \forall X . X\orth\parr X \\
\\
\forall \xi . A &\linequiv& \exists X . (\forall \xi . (A \parr X\orth)) \tens X \\
\exists \xi . A &\linequiv& \forall X . (\exists \xi . (A \tens X\orth)) \parr X
\end{array}
</math>

== Miscellaneous ==

<math>
\begin{array}{rcl}
\oc{\wn{(\oc{A}\with\oc{B})}} &\linequiv& \oc{(\wn{\oc{A}}\with\wn{\oc{B}})} \\
\wn{\oc{(\wn{A}\plus\wn{B})}} &\linequiv& \wn{(\oc{\wn{A}}\plus\oc{\wn{B}})}
\end{array}
</math>

2013-04-25T19:56:44Z

Olivier Laurent: Added formules from Semantics page

{{stub}}

In many of the cases below the [[Non provable formulas|converse implication does not hold]].

== Distributivities ==

<math>A\plus (B\with C) \limp (A\plus B)\with (A\plus C)</math>

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

== Factorizations ==

<math>(A\with B)\plus (A\with C) \limp A\with (B\plus C)</math>

== Additive structure ==

<math>
\begin{array}{rcl}
A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\
(C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\
A &\longrightarrow& A\with A\\
A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\
(A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\
A\plus A &\longrightarrow& A\\
\end{array}
</math>

== Exponential structure ==

Provable formulas involving exponential connectives only provide us with the [[lattice of exponential modalities]].

<math>
\begin{array}{rclcrcl}
\oc A &\longrightarrow& A &\quad& A&\longrightarrow&\wn A\\
\oc A &\longrightarrow& 1 &\quad& \bot &\longrightarrow& \wn A\\
\oc A &\longrightarrow& \oc A\tens\oc A &\quad&
\wn A\parr\wn A &\longrightarrow& \wn A\\
\oc A &\longrightarrow& \oc\oc A &\quad& \wn\wn A &\longrightarrow& \wn A\\
\end{array}
</math>

== Monoidality of exponential ==

<math>
\begin{array}{rclcrcl}
\oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&
\one &\longrightarrow& \oc\one\\
\end{array}
</math>

Semantics

2013-04-25T19:51:24Z

Olivier Laurent: Removed isomorphisms

Linear Logic has numerous semantics some of which are described in details in the next sections. We give here an overview of the common properties that one may find in most of these models. We will denote by <math>A\longrightarrow B</math> the fact that there is a canonical morphism from <math>A</math> to <math>B</math> and by <math>A\cong B</math> the fact that there is a canonical isomorphism between <math>A</math> and <math>B</math>. By "canonical" we mean that these (iso)morphisms are natural transformations.

== Multiplicative semi-distributivity ==

<math>
\begin{array}{rcl}
A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\
\end{array}
</math>

== Additive structure ==

<math>
\begin{array}{rcl}
A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\
(C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\
A &\longrightarrow& A\with A\\
A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\
(A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\
A\plus A &\longrightarrow& A\\
\end{array}
</math>

== Exponential structure ==

<math>
\begin{array}{rclcrcl}
\oc A &\longrightarrow& A &\quad& A&\longrightarrow&\wn A\\
\oc A &\longrightarrow& 1 &\quad& \bot &\longrightarrow& \wn A\\
\oc A &\longrightarrow& \oc A\tens\oc A &\quad&
\wn A\parr\wn A &\longrightarrow& \wn A\\
\oc A &\longrightarrow& \oc\oc A &\quad& \wn\wn A &\longrightarrow& \wn A\\
\end{array}
</math>

== Monoidality of exponential ==

<math>
\begin{array}{rclcrcl}
\oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&
\one &\longrightarrow& \oc\one\\
\end{array}
</math>

List of isomorphisms

2013-04-25T19:48:16Z

Olivier Laurent: First list

Isomorphism

2013-04-25T19:38:11Z

Olivier Laurent: Link to list of isomorphisms

{{stub}}

Two formulas <math>A</math> and <math>B</math> are isomorphic (denoted <math>A\cong B</math>), when there are two proofs <math>\pi</math> of <math>A \vdash B</math> and <math>\rho</math> of <math>B \vdash A</math> such that eliminating the cut on <math>A</math> in

<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{B\vdash B}\DisplayProof</math>

leads to an [[Sequent_calculus#Expansion_of_identities|<math>\eta</math>-expansion]] of

<math>\LabelRule{\rulename{ax}}\NulRule{B\vdash B}\DisplayProof</math>,

and eliminating the cut on <math>B</math> in

<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{A\vdash A}\DisplayProof</math>

leads to an [[Sequent_calculus#Expansion_of_identities|<math>\eta</math>-expansion]] of

<math>\LabelRule{\rulename{ax}}\NulRule{A\vdash A}\DisplayProof</math>.

Linear logic admits [[List of isomorphisms|many isomorphisms]], but it is not known wether all of them have been discovered or not.

Isomorphism

2013-04-25T19:34:31Z

Olivier Laurent: notation for isomorphisms

{{stub}}

Two formulas <math>A</math> and <math>B</math> are isomorphic (denoted <math>A\cong B</math>), when there are two proofs <math>\pi</math> of <math>A \vdash B</math> and <math>\rho</math> of <math>B \vdash A</math> such that eliminating the cut on <math>A</math> in

<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{B\vdash B}\DisplayProof</math>

leads to an [[Sequent_calculus#Expansion_of_identities|<math>\eta</math>-expansion]] of

<math>\LabelRule{\rulename{ax}}\NulRule{B\vdash B}\DisplayProof</math>,

and eliminating the cut on <math>B</math> in

<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{A\vdash A}\DisplayProof</math>

leads to an [[Sequent_calculus#Expansion_of_identities|<math>\eta</math>-expansion]] of

<math>\LabelRule{\rulename{ax}}\NulRule{A\vdash A}\DisplayProof</math>.

Some well known isomorphisms of linear logic are the following ones:
* <math>A\tens B \limp C \cong A\limp B \limp C</math>
* …