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

ABSTRACT





      NEW LINEAR LOGIC PROOF THEORY AND SEMANTIC, II .
      by
      Aldo Ursini

      Dipartimento di Matematica
      via del Capitano 15
      53100 SIENA
      Italy
      tel.(577)286244
      fax.(577)270581
      e-mail: ursini@sivax.cineca,it

                        -extended abstract-
        Abstract of the abstract.

        We give a different presentation of phase semantic for linear
        logics.First of all this allowed us to understand the PAR
        connective.Secondly it runs very smoothly in all existing
        directions: commutative, non commutative, classic, intuitionistic.
        So, as the II-nd paper of the series, this is devoted to
        "truth semantic" of linear logics.Since we are in no way
        pupils able to overcome their master, in the classical commutative case
        the advantage is admittedly rather thin, and is only visible
        when exponetials come to the limelight.In all other cases there
        seems to be some real surplus over existing semantics.In a
        different paper the method will be tested for LC and LU.

                      ***********************

        A right subtitle to this paper slould be:"An easy way to
        phase semantic for linear logics",mimicking my old friend
        Hans Peter Gumm's "An easy way to the commutator"....
        The trigger to this investigation was the desire to understand
        that most mysterious of all linear connectives, namely
        the PAR (Ipse Dixit [3]).The defining formulas for the PAR
        of two facts A,B are, at your choice :

               A PAR B = { x / for any u,v , if uv R x then
                               for some y  B , u R y  or else
                               for some z  A , v R z }

               A PAR B = { x / for any u,v , if x R uv then
                               for some y  B , y R u or else
                               for some z  A , z R v }

         -place yourself into your favourite phase space and let
         R a binary relation, of the kind specified below -.So, we
         have such a parallel nicety as a parallel reading of parallel
         disjunction.This alone would have prompted us to annoy people
         in the linear logic community with our abstracts... .
         N.B.The results in this paper were submitted for the 1993
         Summer Meeting of the ASL, but I was unable to deliver the
         talk there.

         1.COEXISTENCE RELATIONS.
         If R is a binary relation, R~ will be its converse.If
         R is  a binary relation on the set M , x belongs to
         M and  X is a subset of M ,we let

                   Rx = R(x) = { y / x R y }
                   RX = R(X) = { y / for some x in X, x R y }
                   X #R  = (X)#R  ={ y / Ry intersection X is empty }

         We get two operators from Pow(M) into Pow(M) :

                   k(X) = (X)#R#R~
                   h(X) = (X)#R~#R

         These are closure operators.We are interested in those sets
         which are both k-closed and h-closed, and name them facts
         of (M,R).If we want to have the largest class of facts, we
         better require that h=k.This is gratis when R is symmetric.
         In general the following are equivalent :

             i.  k(X) is included in h(X),for all X;
             ii.If R~(X) is included in R~X then R(X) is included in R(Y),
                for all X,Y ;
             iii. For any a,b in M :  a R b  iff for some  u in R~(a)
                R(u) is included in R~(b).

         (By: "dualize" we mean : "interchange R and R~").Of course
         iii. and its dual give a characterization of : h = k .
         R is called a coexistence relation in case h = k .
         We urge the reader to drow a diagram to visualize the
         meaning of this property in terms of R... .

         2. Phasoids.
         Consider a grupoid (M,.) - just a binary operation on M-.
         It is called R-associative if for any a,b,c ;

               a R bc  iff  ab R c

         A phasoid is a structure  (M,R,.,1)  in which . is R-associative,
         R is a coexistence relation, and 1 is neutral for . .
         From here on, we work in a phasoid. Define

                  X PAR1 Y      ,   X PAR2 Y

         as in the premiss.If X,Y are facts ,then  X PAR1 Y = X PAR2 Y.
         This will be the PAR of  two facts.As for linear implications,
         one  shows that, if X,Y are facts, then :

                  X ---o Y = X#R~ PAR Y ;
                  Y o--- X = Y PAR X#R ;
                  X o--- Y#R~ = X#R ---o Y .

         And hence X#R and X#R~ are the linear negations of X , etc.
         The connection with phase spaces is clear , namely:

         (*)       x R y   iff  xy belongs to BOTTOM .

         We do not need full associativity of  . , only R-associativity.
         The Cyclic case corresponds to : R symmetric.
         The Commutative case corresponds to : . commutative.
         The Exponentials fill in smoothly.For instance :

         p is in  !X      iff   R(p) is covered by the R(G)'s,
                              G open facts containig X ,

         Etc. etc.

         The Intuitionistic cases fill in through a family of
         coexistence relations, instead of just one.But this
         Author believes that Sambin's Pretopologies are more akin to
         the BASIC PRINCIPLE OF SEMANTIC :"A semantic has to be
         simpler then the formal logic it modelizes".
         Of course, a proof of completeness may be got via (*),
         but a direct proof , via the  Provabilty Phasoid is
         rather illuminating ... .

         3.Reduced phasoids.
         The study of phasoids is pretty interesting.If you define

             a~b  iff R(a) = R(b)

         you get a congruence of the phasoid.The quotient phasoid
         is said to be a reduced phasoid , for it obeys:

              if R(a) = R(b)  then  a = b .

         In a reduced phasoid, you define a partial order by :

              a < b  iff  R(a) is smaller then R(b).

         This is compatible with the phasoid structure.You can
         characterize  the l-phasoids, namely the reduced phasoids
         in which the ordering is a lattice, and investigate the
         completeness of your favourite linear logic with regard to
         l-phasoids semantic. Etc,etc.

                        REFERENCES
         V.M.Abrusci,Phase semantic and sequent calculus for pure
                     non commutative classical linear propositional
                     logic
                     Journal of Symbolic Logic 56,1991.

         J-Y.Girard ,Linear Logic
                     Theoretical Computer Science 50,1987.

         J-Y.Girard ,La Logique Lineare,
                     Pour la Science,100,1990.