Intuitionistic linear logic - Revision history

Olivier Laurent: /* The intuitionistic fragment of linear logic */ Updated counter-example with 0 only

2017-03-13T08:31:31Z

‎The intuitionistic fragment of linear logic: Updated counter-example with 0 only

Olivier Laurent: /* The intuitionistic fragment of linear logic */ typo

2017-03-09T10:04:29Z

‎The intuitionistic fragment of linear logic: typo

Laurent Regnier: Link to the LL sequent calculus

2009-03-14T10:47:07Z

Link to the LL sequent calculus

Olivier Laurent: /* Input / output polarities */ use of \rulename

2009-02-12T22:07:57Z

‎Input / output polarities: use of \rulename

Olivier Laurent: /* The intuitionistic fragment of linear logic */ use of \rulename

2009-02-12T22:06:58Z

‎The intuitionistic fragment of linear logic: use of \rulename

Olivier Laurent: /* Sequent Calculus */ use of \rulename

2009-02-12T22:04:48Z

‎Sequent Calculus: use of \rulename

Olivier Laurent: \alpha -> \xi

2009-01-17T20:52:06Z

\alpha -> \xi

Olivier Laurent: input/output polarities

2009-01-11T19:51:24Z

input/output polarities

Olivier Laurent: /* The intuitionistic fragment of linear logic */ refined statements

2009-01-11T19:46:14Z

‎The intuitionistic fragment of linear logic: refined statements

Olivier Laurent: Definition of ILL and embedding into LL (two-sided presentation)

2009-01-07T21:03:39Z

Definition of ILL and embedding into LL (two-sided presentation)

New page

Intuitionistic Linear Logic (<math>ILL</math>) is the
[[intuitionnistic restriction]] of linear logic: the sequent calculus
of <math>ILL</math> is obtained from the 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{\textit{ax}}
\NulRule{A\vdash A}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A}
\AxRule{\Delta,A\vdash C}
\LabelRule{\textit{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\alpha A}
\DisplayProof
\qquad
\AxRule{\Gamma,A[\tau/\alpha]\vdash C}
\LabelRule{\forall L}
\UnaRule{\Gamma,\forall\alpha A\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash A[\tau/\alpha]}
\LabelRule{\exists R}
\UnaRule{\Gamma\vdash\exists\alpha A}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\LabelRule{\exists L}
\UnaRule{\Gamma,\exists\alpha A\vdash C}
\DisplayProof
</math>

with <math>\alpha</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\alpha J \mid \exists\alpha J
</math>

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

{{Theorem|title=<math>JLL</math> and <math>ILL</math>|
<math>\Gamma\vdash A</math> is provable in <math>ILL_1</math> if and only if it is provable in <math>JLL_1</math>.
}}

{{Proof|
The first direction is immediate since <math>ILL_1</math> is included in <math>JLL_1</math>.

For the second direction, we consider a cut-free proof of <math>\Gamma\vdash A</math> in <math>JLL_1</math>. We prove by induction on the length of such a proof that it belongs to <math>ILL_1</math>.
}}

This result is still valid with units from <math>ILL_1</math> into <math>JLL_1</math>. In the opposite direction, it holds with <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_1</math>:

<math>
\LabelRule{\textit{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_1</math>.

@@ Line 191: / Line 191: @@
 }}
-The theorem is still valid with 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>:
+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>

@@ Line 229: / Line 229: @@
 <math>
-\LabelRule{\textit{ax}}
+\LabelRule{\rulename{ax}}
 \NulRule{\vdash O\orth,O}
 \DisplayProof
@@ Line 235: / Line 235: @@
 \AxRule{{}\vdash \Gamma,O}
 \AxRule{{}\vdash\Delta,O\orth}
-\LabelRule{\textit{cut}}
+\LabelRule{\rulename{cut}}
 \BinRule{{}\vdash\Gamma,\Delta}
 \DisplayProof

← Older revision		Revision as of 19:51, 11 January 2009
Line 212:		Line 212:

	but not in <math>ILL_0</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\alpha I \mid \forall\alpha 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\alpha O \mid \exists\alpha 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{\textit{ax}}
		+	\NulRule{\vdash O\orth,O}
		+	\DisplayProof
		+	\qquad
		+	\AxRule{{}\vdash \Gamma,O}
		+	\AxRule{{}\vdash\Delta,O\orth}
		+	\LabelRule{\textit{cut}}
		+	\BinRule{{}\vdash\Gamma,\Delta}
		+	\DisplayProof
		+	</math>
		+
		+	<br>
		+
		+	<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>
		+
		+	<br>
		+
		+	<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>
		+
		+	<br>
		+
		+	<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>
		+
		+	<br>
		+
		+	<math>
		+	\AxRule{{}\vdash\Gamma,A}
		+	\LabelRule{\forall}
		+	\UnaRule{{}\vdash\Gamma,\forall\alpha A}
		+	\DisplayProof
		+	\qquad
		+	\AxRule{{}\vdash\Gamma,A[\tau/\alpha]}
		+	\LabelRule{\exists}
		+	\UnaRule{{}\vdash\Gamma,\exists\alpha 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>\alpha</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 ==

@@ Line 191: / Line 191: @@
 }}
-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>:
+The theorem is also valid for formulas containing <math>\one</math> or <math>\top</math> but not anymore with <math>\zero</math>. <math>{}\vdash((X\limp Y)\limp\zero)\limp(X\tens(\zero\limp Z))</math> is provable in <math>JLL_0</math>:
 <math>
 \LabelRule{\rulename{ax}}
 \NulRule{X\vdash X}
-\LabelRule{\top R}
+\LabelRule{\zero L}
-\NulRule{{}\vdash Y,\top}
+\NulRule{\zero\vdash Y,Z}
 \LabelRule{\tens R}
-\BinRule{X\vdash Y,X\tens\top}
+\BinRule{X\vdash Y,X\tens(\zero\limp Z)}
 \LabelRule{\limp R}
-\UnaRule{{}\vdash X\limp Y,X\tens\top}
+\UnaRule{{}\vdash X\limp Y,X\tens(\zero\limp Z)}
 \LabelRule{\zero L}
 \NulRule{\zero\vdash {}}
 \LabelRule{\limp L}
-\BinRule{(X\limp Y)\limp\zero\vdash X\tens\top}
+\BinRule{(X\limp Y)\limp\zero\vdash X\tens(\zero\limp Z)}
 \LabelRule{\limp R}
-\UnaRule{{}\vdash((X\limp Y)\limp\zero)\limp(X\tens\top)}
+\UnaRule{{}\vdash((X\limp Y)\limp\zero)\limp(X\tens(\zero\limp Z))}
 \DisplayProof
 </math>

@@ Line 1: / Line 1: @@
 Intuitionistic Linear Logic (<math>ILL</math>) is the
 [[intuitionnistic restriction]] of linear logic: the sequent calculus
-of <math>ILL</math> is obtained from the two-sided sequent calculus of
+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
+linear logic]] by constraining sequents to have exactly one formula on
 the right-hand side: <math>\Gamma\vdash A</math>.

@@ Line 138: / Line 138: @@
 \AxRule{\Gamma\vdash A}
 \LabelRule{\forall R}
-\UnaRule{\Gamma\vdash \forall\alpha A}
+\UnaRule{\Gamma\vdash \forall\xi A}
 \DisplayProof
 \qquad
-\AxRule{\Gamma,A[\tau/\alpha]\vdash C}
+\AxRule{\Gamma,A[\tau/\xi]\vdash C}
 \LabelRule{\forall L}
-\UnaRule{\Gamma,\forall\alpha A\vdash C}
+\UnaRule{\Gamma,\forall\xi A\vdash C}
 \DisplayProof
 \qquad
-\AxRule{\Gamma\vdash A[\tau/\alpha]}
+\AxRule{\Gamma\vdash A[\tau/\xi]}
 \LabelRule{\exists R}
-\UnaRule{\Gamma\vdash\exists\alpha A}
+\UnaRule{\Gamma\vdash\exists\xi A}
 \DisplayProof
 \qquad
 \AxRule{\Gamma,A\vdash C}
 \LabelRule{\exists L}
-\UnaRule{\Gamma,\exists\alpha A\vdash C}
+\UnaRule{\Gamma,\exists\xi A\vdash C}
 \DisplayProof
 </math>
-with <math>\alpha</math> not free in <math>\Gamma,C</math> in the rules <math>\forall R</math> and <math>\exists L</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 ==
@@ Line 164: / Line 164: @@
 <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\alpha J \mid \exists\alpha J
+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>
@@ Line 218: / Line 218: @@
 <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\alpha I \mid \forall\alpha I
+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\alpha O \mid \exists\alpha O
+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>
@@ Line 317: / Line 317: @@
 \AxRule{{}\vdash\Gamma,A}
 \LabelRule{\forall}
-\UnaRule{{}\vdash\Gamma,\forall\alpha A}
+\UnaRule{{}\vdash\Gamma,\forall\xi A}
 \DisplayProof
 \qquad
-\AxRule{{}\vdash\Gamma,A[\tau/\alpha]}
+\AxRule{{}\vdash\Gamma,A[\tau/\xi]}
 \LabelRule{\exists}
-\UnaRule{{}\vdash\Gamma,\exists\alpha A}
+\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>\alpha</math> not free in <math>\Gamma</math> in the rule <math>\forall</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|

@@ Line 169: / Line 169: @@
 <math>JLL</math> is the [[fragment]] of linear logic obtained by restriction to intuitionistic formulas.
-{{Theorem|title=<math>JLL</math> and <math>ILL</math>|
+{{Proposition|title=From <math>ILL</math> to <math>JLL</math>|
-<math>\Gamma\vdash A</math> is provable in <math>ILL_1</math> if and only if it is provable in <math>JLL_1</math>.
+If <math>\Gamma\vdash A</math> is provable in <math>ILL_{012}</math>, it is provable in <math>JLL_{012}</math>.
 }}
 {{Proof|
-The first direction is immediate since <math>ILL_1</math> is included in <math>JLL_1</math>.
+<math>ILL_{012}</math> is included in <math>JLL_{012}</math>.
-For the second direction, we consider a cut-free proof of <math>\Gamma\vdash A</math> in <math>JLL_1</math>. We prove by induction on the length of such a proof that it belongs to <math>ILL_1</math>.
+{{Theorem|title=From <math>JLL</math> to <math>ILL</math>|
 }}
-This result is still valid with units from <math>ILL_1</math> into <math>JLL_1</math>. In the opposite direction, it holds with <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_1</math>:
+The theorem is still valid with 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>
@@ Line 200: / Line 209: @@
 </math>
-but not in <math>ILL_1</math>.
+but not in <math>ILL_0</math>.