Abstract

The category of coherent phase spaces introduced by the author is a refinement of the symplectic “category” of A. Weinstein. This category is *-autonomous and thus provides a denotational model for Multiplicative Linear Logic. Coherent phase spaces are symplectic manifolds equipped with a certain extra structure of “coherence”. They may be thought of as “infinitesimal” analogues of familiar coherent spaces of Linear Logic. The role of cliques is played by Lagrangian submanifolds of ambient spaces. Physically, a symplectic manifold is the phase space of a classical dynamical system, and a Lagrangian submanifold is a phase of a short-wave oscillation. Typically, Lagrangian submanifolds represent such objects as short-wave approximations of wave functions in asymptotic quantization and wave fronts in geometrical optics. The coherent phase space semantics was motivated to a large extent by methods of geometric and asymptotic quantization and suggests some interesting intuitions on Linear Logic. In particular Lagrangian submanifold-cliques of types A and A can be interpreted as semiclassical limits of eigenstates of respectively position and momentum observables. These observables being canonically conjugate cannot be measured simultaneously, which corresponds to the idea that a formula A and its negation A cannot both simultaneously have proofs . We show that the coherent phase space semantics of Linear Logic enjoys several completeness properties in general much stronger than the usual full completeness with respect to the class of dinatural transformations. These properties of completeness in conjunction with a quite natural -physical meaning make the coherent phase space semantics an interesting object of investigation