Intuitionistic linear logic
Intuitionistic Linear Logic (ILL) is the intuitionnistic restriction of linear logic: the sequent calculus of ILL 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.
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:
JLL is the fragment of linear logic obtained by restriction to intuitionistic formulas.
Proposition (From ILL to JLL)
Theorem (From JLL to ILL)
Corollary (Unique conclusion in JLL)
The theorem is also valid for formulas containing or but not anymore with . is provable in JLL0:
but not in ILL0.
Input / output polarities
In order to go to LL 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 JLL is mapped to an output formula (and the dual of a JLL formula to an input formula). Conversely, any output formula is coming from a JLL formula in this way (up to commutativity of : ).
The fragment of linear logic obtained by restriction to input/output formulas is thus equivalent to JLL, 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)
- ↑ 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.