Xref: utzoo sci.math:17609 sci.logic:1292 comp.theory:2027
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!news.uu.net!mcsun!unido!ecrc!remo
From: remo@ecrc.de (Remo Pareschi)
Newsgroups: sci.math,sci.logic,comp.theory
Subject: Re: Linear Logic
Keywords: Linear Logic
Message-ID: <1991May22.105842.21179@ecrc.de>
Date: 22 May 91 10:58:42 GMT
References: <3023@puck.sw.mcc.com> <1991May16.232218.8032@newshost.anu.edu.au> <1991May21.222324.12820@cs.ubc.ca>
Sender: news@ecrc.de
Reply-To: remo@ecrc.de (Remo Pareschi)
Organization: European Computer-Industry Research Centre, Munich
Lines: 53

In article 1991May21.222324.12820@cs.ubc.ca 
Jamie Andrews (andrews@cs.ubc.ca) writes:

>     I think it's important to note, in this discussion, that
>linear logic is (or should be) part of a wider field of study.
>Linear logic is what Peter Schroeder-Heister calls a
>"sub-structural" logic:  it's a logic with a proof system which
>has restricted structural rules.

      .................

>     I have seen several papers in which people studied logical
>systems weaker than linear logic and claimed that they were
>doing linear logic.  But systems weaker than LL are also weaker
>than classical logic; five years ago, these people could have
>written exactly the same paper and claimed they were doing
>classical logic!  It might be better to say that they are doing
>sub-structural logic inspired by some of Girard's ideas.

However, doesn't Linear Logic offer a comprehensive framework
which subsumes all other "sub-structural" as well "structural"
logics?   In fact,  Linear Logic drops both  Contraction and 
Weakening, but at the same reintroduces them in a "controlled" 
fashion by means  of the so called  exponentials  (in his TCS 
paper,  Girard provides  translations in  Linear Logic  of a
"structural" logic like Classical Logic and of a "semi-structural" 
one like  Intuitionistic Logic  by  crucially exploiting the
regained expressive power  coming from the exponentials); there 
is  a non-commutative version of Linear Logic (described in a
JSL paper by Yetter) which drops the remaining structural
rule of Exchange, and reintroduces it in a controlled fashion
in terms of yet another exponential.

Therefore,  I would be very interested  if Jamie Andrews  could 
provide examples of other logics which are weaker than Linear Logic 
_because of a restricted use of the structural rules_. 

Of course, I know of several efforts which make use of _fragments_ 
of  Linear Logic:  that is,  logics obtained from a subset of the
vocabulary of Linear Logic, where any formula is a theorem if and
only if is a theorem of Linear Logic.  These efforts  include the
concurrent object oriented/logic programming language LO developed
here at ECRC (papers in the proceedings of ICLP'90, OOPSLA/ECOOP'90, 
and forthcoming in New Generation Computing and in the proceedings
of OOPSLA'91), which is based on one such fragment of Linear Logic.
But there is a clear distinction between logical systems which are
weaker than other systems (i.e. the same formula is a theorem in one
system and is not a theorem in the other), and logical systems which
are fragments of other systems (i.e. the formulae of one systems are
a subset of the formulae of the other system, but for such a subset,
the set of theorems for the two systems coincide).

Cheers -- Remo