Xref: utzoo sci.math:17593 sci.logic:1288 comp.theory:2022
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!spool.mu.edu!agate!ucbvax!van-bc!ubc-cs!andrews
From: andrews@cs.ubc.ca (Jamie Andrews)
Newsgroups: sci.math,sci.logic,comp.theory
Subject: Re: Linear Logic
Keywords: Linear Logic
Message-ID: <1991May21.222324.12820@cs.ubc.ca>
Date: 21 May 91 22:23:24 GMT
Article-I.D.: cs.1991May21.222324.12820
References: <3023@puck.sw.mcc.com> <1991May16.232218.8032@newshost.anu.edu.au>
Sender: usenet@cs.ubc.ca (Usenet News)
Organization: University of British Columbia, Vancouver, B.C., Canada
Lines: 27


     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.

     The important thing is not necessarily to understand the
details and mystique of the system called linear logic, but
rather to get some feel for the effect of using restricted
structural rules in combination with the various kinds of
connectives.

     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.

     The main reason to claim you're doing "linear logic" is to
get a buzzword into your paper.  Not a bad reason, but it does
encourage a rather narrow view.

--Jamie.
  andrews@cs.ubc.ca