Ph.D. (2005) Cornell University
Abstract: We consider semantics of Linear Logic, mainly of its multiplicative fragment. We construct a model, based on ideas of geometric quantization and semiclassical approximation, where formulas are interpreted as symplectic manifolds (phase spaces of physical systems), and proofs are interpreted as Lagrangian submanifolds (approximate localization of quantized systems in classical phase spaces). Physically this corresponds to the setting of semiclassical approximation of quantum mechanics. In our model we consider the extra structure of coherence (technically — a conic subset of the tangent bundle) on a symplectic manifold, which specifies a class of "coherent" Lagrangian submanifolds. Connectives of Linear Logic obtain very natural interpretation as operations on coherences. We show that the above category (category of coherent phase spaces) is a sound and complete in some strong sense model of the multiplicative fragment of Linear Logic. We also try to understand if our coherences and operations on them have any physical meaning.
In parallel we consider another model of the multiplicative fragment, where formulas are interpreted as compact oriented manifolds and proofs are interpreted as manifolds with boundary (bordisms or space-times). Similarly to the previous model we introduce coherences for bordisms, which allows us again to interpret logical connectives as very natural operations on coherences. Furthermore, this formalism, being essentially a generalization of the well-known formalism of proof-nets, allows us to formulate an alternative syntax of multi-dimensional proof-nets, uncovering a geometric meaning of multiplicative connectives of Linear Logic. Finally, following ides of topological field theory, we discover interesting connections between the two models.
In the last part of the dissertation we attempt to extend the symplectic interpretation to larger fragments of Linear Logic, namely to the exponential and the unital fragments. A correct generalization is the category of coherent prequantum spaces, based on prequantum, rather than symplectic, manifolds. Although the resulting model remains, in some aspects, heuristic, as far as the unital fragment is concerned, we obtain a completely rigorous new interpretation.