# Intuitionistic linear logic

m (→The intuitionistic fragment of linear logic: typo) |
(→The intuitionistic fragment of linear logic: Updated counter-example with 0 only) |
||

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

\LabelRule{\rulename{ax}} |
\LabelRule{\rulename{ax}} |
||

\NulRule{X\vdash X} |
\NulRule{X\vdash X} |
||

− | \LabelRule{\top R} |
+ | \LabelRule{\zero L} |

− | \NulRule{{}\vdash Y,\top} |
+ | \NulRule{\zero\vdash Y,Z} |

+ | \LabelRule{\limp R} |
||

+ | \UnaRule{{}\vdash Y,\zero\limp Z} |
||

\LabelRule{\tens R} |
\LabelRule{\tens R} |
||

− | \BinRule{X\vdash Y,X\tens\top} |
+ | \BinRule{X\vdash Y,X\tens(\zero\limp Z)} |

\LabelRule{\limp R} |
\LabelRule{\limp R} |
||

− | \UnaRule{{}\vdash X\limp Y,X\tens\top} |
+ | \UnaRule{{}\vdash X\limp Y,X\tens(\zero\limp Z)} |

\LabelRule{\zero L} |
\LabelRule{\zero L} |
||

\NulRule{\zero\vdash {}} |
\NulRule{\zero\vdash {}} |
||

\LabelRule{\limp L} |
\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} |
\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 |
\DisplayProof |
||

</math> |
</math> |

## Latest revision as of 10:31, 13 March 2017

Intuitionistic Linear Logic (*I**L**L*) is the
intuitionnistic restriction of linear logic: the sequent calculus
of *I**L**L* is obtained from the two-sided sequent calculus of
linear logic by constraining sequents to have exactly one formula on
the right-hand side: .

The connectives , and are not available anymore, but the linear implication is.

## Contents |

## [edit] Sequent Calculus

with ξ not free in Γ,*C* in the rules and .

## [edit] The intuitionistic fragment of linear logic

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

*J**L**L* is the fragment of linear logic obtained by restriction to intuitionistic formulas.

**Proposition** (From *I**L**L* to *J**L**L*)

If is provable in *I**L**L*_{012}, it is provable in *J**L**L*_{012}.

*Proof.*
*I**L**L*_{012} is included in *J**L**L*_{012}.

**Theorem** (From *J**L**L* to *I**L**L*)

If is provable in *J**L**L*_{12}, it is provable in *I**L**L*_{12}.

*Proof.*
We only prove the first order case, a proof of the full result is given in the PhD thesis of Harold Schellinx^{[1]}.

Consider a cut-free proof of in *J**L**L*_{12}, we can prove by induction on the length of such a proof that it belongs to *I**L**L*_{12}.

**Corollary** (Unique conclusion in *J**L**L*)

If is provable in *J**L**L*_{12} then Δ is a singleton.

The theorem is also valid for formulas containing or but not anymore with . is provable in *J**L**L*_{0}:

but not in *I**L**L*_{0}.

## [edit] Input / output polarities

In order to go to *L**L* without , we consider two classes of formulas: *input formulas* (*I*) and *output formulas* (*O*).

By applying the definition of the linear implication , any formula of *J**L**L* is mapped to an output formula (and the dual of a *J**L**L* formula to an input formula). Conversely, any output formula is coming from a *J**L**L* formula in this way (up to commutativity of : ).

The fragment of linear logic obtained by restriction to input/output formulas is thus equivalent to *J**L**L*, but the closure of the set of input/output formulas under orthogonal allows for a one-sided presentation.

with *A* and *B* arbitrary input or output formulas (under the condition that the composite formulas containing them are input or output formulas) and ξ not free in Γ in the rule .

**Lemma** (Output formula)

If is provable in *L**L*_{12} and contains only input and output formulas, then Γ contains exactly one output formula.

*Proof.*
Assume Γ_{O} is obtained by turning the output formulas of Γ into *J**L**L* formulas and Γ_{I} is obtained by turning the dual of the input formulas of Γ into *J**L**L* formulas, is provable in *L**L*_{12} thus in *J**L**L*_{12}. By corollary (Unique conclusion in *J**L**L*), Γ_{O} is a singleton, thus Γ contains exactly one output formula.

## [edit] References

- ↑ Schellinx, Harold.
*The Noble Art of Linear Decorating*. Dissertation series of the Dutch Institute for Logic, Language and Computation. University of Amsterdam. ILLC-Dissertation Series, 1994-1, 1994.