Embedding of classical into intuitionistic linear logic

Question

Following on from this recent question, there is another construction that is well-known, but I don’t know a good primary source for: the Kolmogorov-style double-negation embedding of classical into intuitionistic linear logic (where the translation of a sequent is intuitionistically provable iff the original was classically provable). I would be very happy to learn of suitable references for this, too.

I’d rather not specify a specific theorem, because I’d be interested to learn about any early published result of this sort.

Answer 1

There are actually many negative translations of classical linear logic into intuitionistic linear logic, just as there are many negative translations of classical logic into intuitionistic/minimal logic (by Kolmogorov, Gentzen, Gödel, Kuroda, etc.). A good way of understanding this is in terms of polarities, which were introduced into linear logic by Girard in the early 1990s, following Andreoli's work on focusing proof search. Polarized linear logic can be seen as a refinement of classical linear logic, in the sense that there is a forgetful translation $$|{-}| : \text{polarized } LL \to CLL$$ which erases polarities. On the other hand, there is also a deterministic translation $$(-)^\dagger : \text{polarized } LL \to ILL$$ that interprets polarized formulas into a negative fragment of intuitionistic linear logic. This fragment of ILL has been called tensorial logic by Melliès, and is essentially equivalent to polarized linear logic but in an asymmetric presentation. Then, different negative translations of CLL into ILL can be understood as the composition of an ad hoc polarization

$$(-)^* : CLL \to \text{polarized } LL$$

(which must be a section of $|{-}|$, i.e., the equivalence $A \Leftrightarrow |A^*|$ holds for all CLL formulas $A$) followed by the deterministic translation $(-)^\dagger$.

Unfortunately, I don't know of a place in the literature where this is all explained very clearly. The early work on focusing and polarities includes

• Jean-Marc Andreoli, Logic Programming with Focusing Proofs, JLC 2(3), 1992.

• Jean-Yves Girard, "On the unity of logic", APAL 59(3), 1993.

A more recent paper discussing polarities from the point of view of negative translation (and linear continuations) is

• Paul-André Melliès and Nicolas Tabareau, Resource modalities in tensor logic, APAL 161(5), 2009.