IL -- LU -- LL

To: linear@cs.stanford.edu
Subject: IL -- LU -- LL
From: hars@logique.jussieu.fr
Date: Sun, 16 May 93 14:19:48 +0200
Approved: types@dcs.gla.ac.uk


In his message to the Linear mbox of Thu, 13 May 93, Sanjiva Prasad writes:

  "I seem to have evermore questions as I learn more about proof theory,
   linear logic and LU.
   [ ............. ]
   I would appreciate any information on the connections between LU's
   intuitionistic fragment and usual calculi for intuitionistic logic"

The paper "On the linear decoration of intuitionistic derivations" (joint
work of V.Danos, J.B. Joinet and myself) might be of help in gaining some
insight. It is available by anonymous ftp from "gentzen.logique.jussieu.fr".
You will find it in the directory pub/scratch as `Noble1.dvi'. There's
also a compressed file, `Noble1.dvi.Z'.
In the paper we mention e.g. how one can transform a given derivation in
the (implicational fragment of) usual sequent calculus for intuitionistic
logic into a derivation in the (neutral) intuitionistic fragment of LU.

A general hint: if you have some experience with linear logic, think of the
intuitionistic/classical LU-fragments via their `linear interpretation':
write !p for positive atoms p, ?n for negative atoms n, x for neutral atoms x,
and use the linear definitions of the connectives (you then will find that
"formula F is positive" corresponds to "its linear interpretation [F] has
the property that [F] <=> ![F] is provable in linear logic", and, dually, for
"formula F is negative" we have "[F] <=> ?[F] is provable in LL").

Harold Schellinx

(NB.: You might also be interested in a second paper, related to the one
mentioned above. It is called "The Structure of Exponentials: Uncovering
the Dynamics of Linear Logic Proofs", and can be found in the same
ftp-directory as `StrucExp.dvi(.Z)' .)