[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.