# Embedding of classical into intuitionistic linear logic

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.

• Troesltra's Lectures on Linear Logic. Apr 1, 2015 at 16:03
• Thanks Sylvain! It’s the last thing in Chapter 5, Section 5.12. Troelstra calls it “nothing but a variant of the well known Kolmogorov translation”, and doesn’t give a reference, so this seems a reasonable source if no one has an earlier. Would you like to turn your comment into an answer? Apr 1, 2015 at 16:09

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