Quantales and (noncommutative) linear logic

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.