The Journal of Symbolic Logic

Research Article

Quantales and (noncommutative) linear logic

David N. Yetter 

Department of Mathematics and Statistics, McGill University, Montréal, P. Q. H3A 2K6, Canada

It is the purpose of this paper to make explicit the connection between J.-Y. Girard's “linear logic” [4], and certain models for the logic of quantum mechanics, namely Mulvey's “quantales” [9]. This will be done not only in the case of commutative linear logic, but also in the case of a version of noncommutative linear logic suggested, but not fully formalized, by Girard in lectures given at McGill University in the fall of 1987 [5], and which for reasons which will become clear later we call “cyclic linear logic”.

For many of our results on quantales, we rely on the work of Niefield and Rosenthal [10].

The reader should note that by “the logic of quantum mechanics” we do not mean the lattice theoretic “quantum logics” of Birkhoff and von Neumann [1], but rather a logic involving an associative (in general noncommutative) operation “and then”. Logical validity is intended to embody empirical verification (whether a physical experiment, or running a program), and the validity of A & B (in Mulvey's notation) is to be regarded as “we have verified A, and then we have verified B”. (See M. D. Srinivas [11] for another exposition of this idea.)

This of course is precisely the view of the “multiplicative conjunction”, ⊗, in the phase semantics for Girard's linear logic [4], [5]. Indeed the quantale semantics for linear logic may be regarded as an element-free version of the phase semantics.

(Received July 06 1988)

(Revised November 17 1988)

Correspondence

Department of Mathematics, Ohio State University at Mansfield, 1680 University Drive, Mansfield, Ohio 44906