[Prev][Next][Index][Thread]

Linear consequences

Date: Thu, 9 Jan 92 10:56:17+020
To: LINEAR@cs.stanford.edu

In his last message Jean Gallier wrote that from T |- A -o B and
T |- B -o C it does not follow in LL that T |- A -o C, only that
T,T |- A -o C. This indeed is the case for the LINEAR consequence relation
which is usually associated with linear logic (and corresponds to the
sequents of its Gentzen type formulation).  This, however, is not an
ordinary consequence relation in the Tarskian sense.  It is not suitable,
therefore, for semantical investigations of the usual type.  It is much
more fruitful to use instead the ``extensional" consequence relation which
was introduced in my TCS paper. This consequence relation can be given any
of the following characterizations (the equivalence between these
characterizations is shown in that paper or easily follows from results
proved there):

1) T |- A iff there exists a subset {B_1...B_n} of T and a proof (in the
   ordinary sense) of => A from {(=> B_1), ... ,(=> B_n)}.

2) T |- A iff there exists a proof (in the ordinary sense) of A from T in
   the Hilbert-type system HLL of LL (say that presented in my TCS paper).

3) T |- A in the multiplicative fragment iff A belongs to any superset of
   T (in its language) which includes all theorems of multiplicative LL and
   is closed under MP for -o.  in the multiplicative-additive fragment T |- A
   if A belongs to any superset of T which includes all theorems of this
   fragment and is closed under MP for -o and adjunction for & (from A and B
   infer A&B).  Finally, in full propositional LL one should add also the
   condition (on the supersets of T) of closure under the necessitation rule:
   from A infer !A.

The following  deduction theorems for this consequence relation
can easily be proved (each of them easily provides a forth syntactic
characterization of this consequence relation in the corresponding fragment):

i) T,A |- B in the multiplicative fragment iff for some n>=0,
   T |- A-o(A-o...-o(A-oB)...). Here n is the number of "A"s.

ii) T,A |-B in the multiplicative-additive fragment iff for some n>=0,
    T |- 1&A-o(1&A-o...-o(1&A-oB)...). Here n is the number of "1&A"s.

iii) T,A |- B in full propositional LL iff T |- !A-oB (it should be noted
     that the standard translation of intuitionistic implication in LL is
     faithful only relative to the extensional consequence relation, and NOT
     relative to the linear (intensional) one.

Now with respect to the extensional consequence relation one can easily
prove STRONG completeness theorems relative to the various algebraic
structures disussed in my paper and in Gallier's message (and the
formation of the Lindenbaum algebra of any theory is then possible and
useful). For example:

   T |- A iff $A$ is true in every model (in the sense of the "phase
   semantics" of [Gi87]) of $T$.

Finally, I like to note that the fact that the same Gentzen-type formalism
(or any other formalism) naturally induces more than one consequence
relation is not peculiar to linear logic. Even in classical predicate
logic there are two. According to one, e.g., A|-(x)A (since from =>A one
can easily infer =>(x)A), while according to the other this is false
(since A=>(x)A is in general not a valid sequent). As explained in my
paper "Gentzen-type systems, resolution and tableaux" (to appear in JAR),
resolution is based on the first, while the tableaux method on the second.
The truth, however, is that in LL there are MORE THAN TWO. In my
"Axiomatic systems, deduction and implication" (forthcoming in the journal
of Logic and Computation), I discuss 3 natural consequence relations which
are associated with the multiplicative case. In the multiplicative-
additive case (which is not yet treated in that paper) there are at least 5
(similar observations were independently made by Kosta Dosen).

Arnon Avron