Quantales and (noncommutative) linear logic

Abstract

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.