Some Properties of Linear Logic Proved by Semantic Methods

To: types
Subject: Some Properties of Linear Logic Proved by Semantic Methods
From: Arnon Avron <aa%taurus.bitnet@taunivm.tau.ac.il>
Date: Tue, 03 Dec 91 17:15:16 EST
Sender: meyer@theory.lcs.mit.edu
Date: Tue, 3 Dec 91 13:57:42+020
Comments: If you have trouble reaching this host as math.tau.ac.il
        Please use the old address: user@taurus.bitnet
To: LINEAR@cs.stanford.edu

    It seems to me that most of the research on LL has up to now relied on
proof-theoretical methods. The phase semantics, for example, was never used
(as far as I know, which is not too much) for obtaining new results about
the logic which have an independent interst. This fact is strange, since
(denotational) semantical methods are used in research concrning almost any
intersting non-classical logic. One of the reasons is, perhapse, that it
is difficult to construct denotational models of LL which are sound, complete
and concrete (and so usable), Other reason, I suspect, is the young tradition
of the subject.
   Below are some examples of theorems about provability in Linear Logic that
can be proved by one simple semantical method. I like to pose  two problems
concerning them (that might be strongly related):

 1) What do these results mean in terms of proof-nets?
 2) How can these results be proved using purely proof-theoretical methods (like
cut-elimination)?

The results are (we use two-sided sequential formulation):

1) No sentences of the form "A par A" or in general "A par A par A..."
is provable in MULTIPLICATIVE linear logic (MLL) (this is not true for the
multiplicative-additive fragment). In general, if m and k are natural numbers
then there exists a provable sequent of MLL of the form
       A,A,...,A=>A,A,...,A (m A's on the left, k A's on the right)
iff m-1 is divisible by m-k (this includes the case m=k=1).

2) There are no cases in which the "mix" rule (of Girard, not that of Gentzen)
 is admissible in MLL: by mixing any n>1 provable sequents we get a sequent
which is NOT provable (again this fails with the additives).

3) A sequent of the form A_1,...,A_n=>A_1,...,A_n is provable in the additive-
multiplicative fragment of LL (without the additive constants!) iff n=1
(this of course is false with the additive constants T and 0).

    The proofs of these results is based on the following theorem

THEOREM: let c be an integer and let v an assignment of integers to sentences of
the multiplicative-additive fragment of LL (without the additive constants)
which satisfies:
   i) v(~A)=c-v(A)
  ii) v(A par B)=v(A)+v(B)
 iii) v(A&B)= min(v(A),v(B))
  iv) v(1)=c

Then if A is provable in this fragment then v(A)>=c, while if A is an instance
of a theorem of the multiplicative fragment then v(A)=c.

Notes: 1)we take the other connectives here (like tensor) as defined
connectives, but the corresponding conditions on v can easily be computed.
       2) We have here only soundness of the proposed semantics, not completenss