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.
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:
JLL is the fragment of linear logic obtained by restriction to intuitionistic formulas.
Proposition (From ILL to JLL)
If is provable in ILL012, it is provable in JLL012.
Proof. ILL012 is included in JLL012.
Theorem (From JLL to ILL)
If is provable in JLL12, it is provable in ILL12.
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 JLL12, we can prove by induction on the length of such a proof that it belongs to ILL12.
Corollary (Unique conclusion in JLL)
If is provable in JLL12 then Δ is a singleton.
The theorem is also valid for formulas containing but not anymore with and . 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)
If is provable in LL12 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 JLL formulas and ΓI is obtained by turning the dual of the input formulas of Γ into JLL formulas, is provable in LL12 thus in JLL12. By corollary (Unique conclusion in JLL), Γ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.