Polarities for intuitionistic linear logic formulas inside classical linear logic (without linear implication)

Question

In the article on intuitionistic linear logic on the LLWiki, it is stated that a polarization of formulas in classical linear logic is enough to make it equivalent to intuitionistic linear logic, without requiring the linear implication operator ($⊸$) as a primitive. The syntactic classes given for output and input formulas are respectively as follows:

$$O ::= X\ |\ O \otimes O\ |\ 1\ |\ O \mathrel{⅋} I\ |\ I \mathrel{⅋} O\ |\ O \mathrel{\&} O\ |\ \top\ |\ O \oplus O\ |\ 0\ |\ !O$$

$$I ::= X^\bot\ |\ I \mathrel{⅋} I\ |\ \bot\ |\ I \otimes O\ |\ O \otimes I\ |\ I \oplus I\ |\ 0\ |\ I \mathrel{\&} I\ |\ \top\ |\ ?I$$

However, I couldn't find more information about this, although proving this seems straightforward. So, my question: is this correct? If so, is there a reference for this particular characterization of intuitionistic linear logic inside of classical linear logic?

Answer 1

This restricted grammar is discussed here:

François Lamarche. Proof nets for intuitionistic linear logic: Essential nets. Research report , INRIA, 2008. https://inria.hal.science/inria-00347336

Lamarche states that he thinks it was Jacques van Wiele "who first made the remark that this system of polarities, first introduced in order to get a translation of the untyped lambda calculus into linear logic, should be seen as a discipline that restricts classical linear logic to the intuitionistic fragment."

Indeed, one may formulate ILL as a one sided system using IO formulas.