Re: Linear notation

• To: types
• Subject: Re: Linear notation
• From: pratt@cs.Stanford.EDU
• Date: Tue, 31 Dec 91 09:28:40 EST
• Sender: meyer@theory.lcs.mit.edu

```Date: 29 Dec 91 23:32:36 PST (Sun)
To: linear@cs.stanford.edu

From: aa%taurus.bitnet@TAUNIVM.TAU.AC.IL
Date: Sun, 29 Dec 91 12:43:51+020

J.Y. has admitted himself that relevance logicans were the first  to
distinguish between the "multiplicative" and "additive" conjunction and
disjunction

This distinction surely belongs to C.S. Peirce, who in 1870 [Pei] gave
De Morgan's calculus of binary relations pretty much exactly the form
used today by relation algebraists.

Here are the two-typed lattice notations I'm aware of.

Binary   Residuated     Closed  Relevance    Linear
Relations   Lattices    Categories  Logic      Logic

Peirce,     Ward-    Eilenberg- Anderson-   Girard
Schroeder   Dilworth     Kelly     Belnap
[Pei] 1870   [WD] 1939  [EK] 1965  [AB] 1960's  [Gir] 1980's

AB        [A,B]        AxB       A^B         A&B  "with"
1          i           1         T           T

A+B       (A,B)        A+B       AvB         Ao+B "plus"
0          z           0         F           0

A;B     A.B or AB      AoxB      AoB         AoxB "times"
1'          i           I         t           1

A+,B                             A+B         A~8B "par"
0'                                f          _|_

The notation favored by Barr, Cockett, Seely, and myself is basically
the Eilenberg-Kelly notation with the concession that I is changed to T
(whose dual is then naturally _|_ ) and with the dual of ox being taken

I don't know why Ward and Dilworth insisted on identifying the units i
of the two conjunctions---it rules out many residuated lattices
occurring "in nature" as Max Kelly likes to put it.  Nor do I know why
lattice-theoretic notation deteriorated so badly in the first third of
this century---in 1933 Birkhoff wrote meet as (A,B) [sic] and join as
A\cap B [sic!]---after both sides of the Atlantic, Peirce in the US and
Schroeder in Germany, seemed to have converged on a very nice notation
in the last third of the 19th century.  Maybe competing obscure and
mysteriously powerful notations, particularly Peano's as adopted by
Russell and Whitehead but also those of Lukasiewicz, Schoenfinkel,
confusion.

I omitted from the table the notation in Robert and Ferland's [RF] 1968
semiring abstraction of the 1962 Floyd-Warshall algorithm, and no doubt
other semiring notations too, but enough is enough.

I believe relevance logic's tensor product AoB, cotenability, first
appeared in Mike Dunn's thesis [Dun66], which is why I put relevance
logic chronologically after Eilenberg and Kelly (La Jolla'65).  However
given the vagaries of publication (the proceedings appeared in 1966)
this should probably count as a tie for third place, at least for the
conjunction.

However the only place I've seen "relevant disjunction" is in [Avr84].
I don't recall seeing it in what I've read of Dunn, Routley, Meyer,
McRobbie, Urquhart, or Maksimova.  In particular a pass through Mike
Dunn's 105-page chapter on relevance logic in HPL3 [Dun86], the most
recent comprehensive survey of relevance logic that I have to hand,
turned up no occurrences.  While it may appear elsewhere it clearly
does so at best sparsely, and seems to be going places at the same
speed as Peirce's relative sum, probably for similar reasons.  Not only
is it the last operation on the above list, but as I argued a few days
ago on both technical and historical grounds, it is also likely to be
the last operation anyone wants to spend much time debating the proper
notation for.

Vaughan Pratt

PS. A reminder, a propos of linear logic, that a draft of "Event Spaces
and Related Structures", pub/esrs.tex, can be retrieved by anonymous
ftp from boole.stanford.edu.  See pub/README for abstracts of other
papers in the same directory..

========================

@Book(
AB,     Author="A. R. Anderson and N. D. Belnap",
Title="Entailment", volume=1, Publisher="Princeton University Press",

@Article(
Avr84,	Author="Avron, A.",
Title="Relevant Entailment--Semantics and Formal Systems",
Journal="J. Symbolic Logic", Month=Jun, Year=1984)

@PhDThesis(
Dun66,	Author="Dunn, J.M.",
Title="The Algebra of Intensional Logics",
School="Univ. of Pittsburgh", Year=1966)

@InCollection(
Dun86,  Author="J. M. Dunn",
Title="Relevant Logic and Entailment",
Booktitle="Handbook of Philosophical Logic",
Volume="III", Editor="D. Gabbay and F. Guenthner", Pages="117-224",

@InProceedings(
EK66a,  Author="Samuel Eilenberg and G. Max Kelly",
Title="Closed Categories",
Pages="421-562",
Editor="S. Eilenberg and D. K. Harrison and S. MacLane and
H. R{\"o}hrl",
Booktitle="Proceedings of the Conference on Categorical Algebra,
La Jolla, 1965", Publisher="Springer-Verlag", year=1966)

@Article(
Gir,    Author="Girard, J.-Y.",
Title="Linear Logic", Journal="Theoretical Computer Science",
Pages="1-102", Volume=50, year=1987)

@InCollection(
Pei,	Author="Peirce, C.S.",
Title="Description of a notation for the logic of relatives,
resulting from an amplification of the conceptions of {B}oole's
calculus of logic.  1870",
Booktitle="Collected Papers of Charles Sanders Peirce. {III}.
{E}xact Logic", Publisher="Harvard University Press", Year=1933)

@Article(
RF,	Author="Robert, P. and Ferland, J.",
Title="G\'en\'eralisation de l'algorithme de {W}arshall",
Journal="Revue francaise d'Informatique et de
Recherche Operationnelle", Volume=2, Number=7, pages="13-25", Year=1968)

@Article(
WD,	Author="Ward, M. and R.P. Dilworth",
Title="Residuated Lattices",
Journal="Trans. AMS", Volume=45, Pages="335-354", Year=1939)

```