[Prev][Next][Index][Thread]
Non-commutative linear logic
Date: Tue, 4 Feb 92 08:36:36 -0500
To: linear@cs.stanford.edu
This is a response to a posting of Thomas Streicher (Jan 23) asking
in effect whether it was well known that relation algebras are a
model of non-commutative linear logic (without exponentials).
I was fascinated to learn from Vaughan Pratt's posting (Jan 24)that Peirce
used complement-of-negation as converse. I did not know this, and as you
will see below this idea has occurred in the relevance logic literature
in both a somewhat abstract form (look for -* below) and also in a very
explicit form (look for my representation of de Morgan lattices below).
In my thesis (Univ. of Pittsburgh, 1966), I introduced de Morgan
monoids, which are the algebraic models of the relevance logic R.
De Morgan monoids can be understood as structures (D, <, o, e, ->, ~),
where (D, <, o, e) is a #distributive# lattice ordered monoid which
is also 1) commutative, and 2) square-increasing, and -> is a right
residual:
a o x < b iff x < a -> b
[I use < for <= to aid the eyes]
and ~ is a unary operation of period two satisfying the principle of
the "antillogism":
a o x < b iff x o ~b < ~a.
[Note that setting x = e gives that ~ is a dual automorphism.]
Dropping distribution and square increasingness gives what has been
called a "Girard monoid," and is an algebraic model of linear
logic without exponentials. This observation is due to Avron, though
our particular formulation differs in inessential details.
Dropping distribution also gives algebraic models of the relevance logic
"ortho-R"or "lattice-R", gentzenized in Meyer's 1966 U. of Pittsburgh
thesis and used as the basis of the Canberra automated reasoning
project. Cf. P.B. Thistlewaite, R.K. Meyer, and M.A. McRobbie,
Automated Theorem Proving in Non-classical Logics, Research Notes
in Theoretical Computer Science, John Wiley & Sons, 1989? Dropping
2) gives the system R-W (cf. A.R. Anderson and N.D. Belnap, Entailment,
vol. 1, Princeton Univ. Press, 1975). Relevant portions of my thesis
relating to de Morgan monoids are republished in that book. I also
entertained not having commutativity (and then one could have two
residuals, and two negations as well).
OR = (linear logic - exponentials) + contraction
R-W = (linear logic - exponentials) + distribution
R = (linear logic - exponentials) + contraction + distribution
Back when writing my thesis (and several times since then) I thought long
and hard about relation algebras as being *almost* de Morgan monoids, and
hence *almost* models for the paradigm relevance logic R. I knew that
complement of converse looked like a good modelling of de Morgan negation
(but did not yet have the formal representation I cite below). But to get
full R, I had 3 problems:
1) How to get commutativity (RoS = SoR)?
2) How to get square-increasingness (R included in RoR)?
-1
3) How not to get S -> R = -(S o -R) .
Cf. Birkhoff's Lattice Theory 1967, p. 344 for this last and note that
Birkhoff uses / for the *right residual* where I use -> .Many writers,
e.g., Lambek use \. A dual is also listed, but with commutativity
these are the same.
I thought about various natural conditions that might give 1) or 2). Thus
e.g., denseness gives 2) (and transitivity gives its converse, and so the
two together give idempotence, as required by the relevance logic R-Mingle).
Of course for linear logic (or for the relevance logic R-W, where
contraction is not a desirable logical property, it could well be
considered a plus not to get 2).
I don't recall ever getting a natural condition for 1). (Requiring the
relations to be symmetric quickly occurs to one, but a little thought shows
that this is not even close.)
And of course 3) holds in all relation algebras, so the only way to get rid
of it would be by some suitable abstraction, losing the very concrete models
(relation algebras) that seemed so attractive. What is wrong with 3)
someone might ask. It is tantalizing close to something that should
be true for either linear logic or R(-W) (using ~ for de Morgan negation):
3') S -> R = ~(So~R),
but of course it replaces ~ is replaced by Boolean complement - and a
"random" converse is thrown in on S). I am pretty sure that 3) would lead
to some undesirable properties in relevance logic (and I would think
linear logic), but cannot quickly say what. It certainly is not verified
by the Routley-Meyer (1973) semantics for relevance logic, even after it
has been fiddled with so as to accomodate as explicit connectives both
boolean negation (-) and "the star-operator" (*), which (warning)
corresponds to converse and #not# ancestral (iteration) as in the
action/dynamic logic literature.
There is the added problem for linear logic (not a problem
for the orthodox relevance logics like R) that distribution of additive
"and" (intersection) over additive "or" (union) holds in relation algebras.
In the relevance logic literature, de Morgan negation (~) has
been defined by the Routleys and Meyer using a map * of period two.
Actually this was anticipated by Bialynicki-Birula and Rasiowa who showed
that every de Morgan lattice (they said "quasi-Boolean algebra" can be
represented as a lattice of subsets of some set U, on which is defined such
a function, with ~X = -(X*) and X* = {x*: x in X}. This was related in my
dissertation to a number of other representations. Incidentally, a de Morgan
lattice is a #distributive# lattice with involution, i.e., an order inverting
map of period two. This looks very much like Peirce's "complement of
converse, with * put in the role of converse.
In my "Relational representation of quasi-boolean algebras," Notre
Dame Journal of Formal Logic, 23, 353-357, I fulfilled "half of a
dream of a lifetime" by showing that every de Morgan lattice ( =
quasi-Boolean algebra) can be represented as a collection of relations,
where meet and join are intersection and union, and de Morgan complement
is defined so
-1
~R = -(R ).
The other half would have been to represent relative product as well,
and of course to do so in such a way as to represent de Morgan monoids.
References can be found in my "Relevance logic and entailment," in
Handbook of Philosophical Logic, vol. 3, eds. D. Gabbay and F. Guenthner,
D. Reidel, 1985. A very interesting additional reference is R. K.
Meyer's "Boolean valued semantics for R," Research paper no. 4 (1979),
Australian Nat.Univ. Logic Group, Philosophy Dept., Research School of Social
Sciences, Canberra, Australia. Also by Meyer: "New Axiomatics for
relevant logics I," Journal of Philosophical Logic, 3, 53-86, and
""Classical relevant logics I," Studia Logica, 32 (1973), 51-66, and
"II", Studia Logica , 33 (1974) , 53-86.
This work of Meyer is related ultimately to showing that boolean negation
can be added conservatively to R, and how de Morgan negation can then be
defined from Boolean negation and *, and how conversely * can be defined
as -~. I suppose analogous facts hold for linear logic, but I have not
thought closely about this. Meyer uses his and Routley's Kripke-style
semantics to produce these results, and it seems quite possible that
Gerry Allwein's and my Kripke-style semantics for linear logic (announced
recently to this group) could be employed in similar ways.
Incidentally, the condition that must be added to the Routley-Meyer
semantics to represent relation algebras is Rxyz only if Ry*x*z. You
must also fiddle with the other conditions (drop Rxyz only if Ryxz,
which gives commutativity, and restate Rxyz only if Rxz*y* so as to
not assume commutativity). There is another subtlety or two involving
their 0, and I believe one can then represent relation algebras
analogous to the way that Routley-Meyer (1973) represent de Morgan
monoids (not as relations unfortunately), defining the two residuals
the way they define relevant implication, but having two definitions that
vary only in their choice of which of the two first positions of Rxyz are
used as the point at which the truth of the implication is being
evaluated. All of this is in the spirit of my "Gaggle Theory" paper
in JELIA '90.
Mike Dunn
dunn@iuvax.cs.indiana.edu
Depts. of Philosophy/Computer Science
Indiana University
Bloomington, IN 47405