[Prev][Next][Index][Thread]
Re: Embedding CLL in ILL
Frank Christoph wrote:
>
>
> The embedding of classical logic in intuitionistic logic is well-known (for
> example, Goedel et al.'s using triple-negation, or Girard's translation using
> polarities). Is there a similar embedding of classical linear logic into
> intuitionistic linear logic? Could someone give me a reference for this?
>
There is a double-negation translation of classical linear logic into
the *,-o,&,!,1 fragment of intuitionistic linear logic that can be found
in my 1995 LICS paper, Games Semantics for Full Propositional Linear
Logic. One detail of note for potential readers is that in this paper
intuitionistic linear logic is given a one-sided-sequent presentation,
using a system of polarities which obeys the Danos-Regnier rules, not
those seen in Girard's LC paper. In other words the above fragment of
ILL is embedded into CLL and these polarities are used to define the
image of this embedding, for which full CLL is a conservative extension
(this was first done by J. van de Wiele, it seems). Naturally one can
also get a direct translation of CLL into ordinary two-sided-sequent
ILL, but I find things less perspicuous when done that way; people may
disagree.
The translation given there is certainly not the only possible one. Ph.
de Groote has found variations for the additives, and there surely are
translations based on different starting points.
As for the second question (CLL into Classical Logic), since full CLL
(and also ILL) is undecidable, there cannot be a useful translation of
the first into the second. Here a system like LU is needed to make both
logics coexist nicely. The fragments of LL where such a translation
might be viable are those, like MLL and IMLL, whose decision problem is
PTIME or less. Naturally a good translation must act well on proofs as
much as on provability.
Francois Lamarche
References: