Embedding CLL in ILL

• To: types@dcs.gla.ac.uk
• Subject: Embedding CLL in ILL
• From: christo@www.nextsolution.co.jp (Frank Christoph)
• Date: Thu, 12 Dec 1996 12:32:48 +0900

  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?

  I am also interested in knowing if anyone has presented a "reverse" embedding
of classical linear logic into classical logic.  Maybe this sounds useless, but
it would give rise to the embedding above by composition:
 
     <-?-
   CL ---> CLL
   |
   v
   IL ---> ILL

---
Frank Christoph                 Next Solution Co.      Tel: 0424-98-1811
christo@nextsolution.co.jp                             Fax: 0424-98-1500

• Re: Embedding CLL in ILL
• From: Francois Lamarche <Francois.Lamarche@loria.fr>

• Prev: call for papers: FIFTH MEETING ON THE MATHEMATICS OF LANGUAGE (MOL5)
• Next: deadlock-free process calculus
• Index(es):
  • Main
  • Thread