# Intuitionistic linear logic

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 |

## Sequent Calculus

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

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

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

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