[Prev][Next][Index][Thread]
Interpreting 1st order logic in linear logic
Date: Tue, 2 Jun 92 14:36:58 +0200
Some days ago I posted a question about Linear Logic. I got several replies
of people interested to the question, but only two answers. I mail
them for sake of completness.
S. Berardi
Date: Mon, 25 May 92 15:55:54 +0200
A quick question to linear people:
what is the simplest interpretation of First Order Classical Logic in Linear
Logic known up to now?
Of course I heard of several of them, but I found all of them a bit tricky.
I consider only complete interpretations, i.e. mapping:
Phi: {First Order Classical Formulas} -> {First Order Linear Formulas}
such that A is a classical theorem iff Phi(A) is a linear theorem.
Please answer me, not to the net, since I suppose the argument be widely
known, except by me!
S. Berardi
>From murthy@margaux.inria.fr Wed May 27 14:52:24 1992
Hi, Stefano,
Every interpretation of CL into CLL that I know of factors THRU a
translation of CL into IL. Thus, if one wants to know what equations
between classical proofs are enforced by a particular translation into
CLL, it suffices to consider the equational theory of the translation
into IL.
Essentially, any translation is going to end up sequentializing the
program completely, so one might as well just stick with CPS.
(omissis)
C. Murthy
>From reddy@cs.uiuc.edu Thu May 28 20:06:45 1992
Hi, The only translation I know of is Girard's in his paper on LC.
(MSCS, 1991, 255-296). Are there others? I would be interested to
know what you find out.
Cheers,
Uday Reddy
Dear Prof. Reddy,
you asked me which translation of Classical Logic inside Linear Logic I
was thinking about in my message to the net.
I was considering three of them:
(1) compose any (sound & complete) embedding of Classical Logic inside
Intuitionistic Logic with the canonical embedding of Intuitionistic Logic
inside Linear Logic.
(2) The first Girard's translation:
phi(Atom) = ?!Atom
phi(A v B) = phi(A) par phi(B)
phi(not A) = ?(dual of phi(A))
phi(ForAll x A) = ?!(Any x phi(A))
(3) The second Girard's translation:
p(Atom) = Atom
n(Atom) = Atom
p(A v B) = p(A) plus p(B)
n(A v B) = ! n(A) par ! n(B)
p(not A) = dual of n(A)
n(not A) = dual of p(A)
p(ForAll x A) = Any x ?p(A)
n(ForAll x A) = Any x n(A)
a sequent A1 ... An |- B1 ... Bm is translated as:
|- n(A1) ... n(An) ... p(B1) ... p(Bm)
These three translations agree on one point:
they all give a very tricky interpretation
of Cut Rule, i.e. to the application of
a function to an argument. This makes unpratical the use of Linear Logic in
extracting the constructive content of Classical proofs.
Constructive content of proofs is my actual research field.
Does anyone know better translations?
Best Regards,
S. Berardi
Torino, 2 Giugno 1992