From proof-nets to bordisms: the geometric meaning of multiplicative connectives

Abstract

We develop a multidimensional syntax for cut-free proofs of Multiplicative Linear Logic. This syntax is essentially equivalent to the traditional formalism of proof-nets; the interest of the multi-dimensional formalism consists in its explicit relationship with the formalism of bordisms. Bordisms are compact manifolds with boundary, which are treated as morphisms between the ‘incoming’ and ‘outgoing’ boundary components (composition is given by glueing bordisms along matching boundaries). The category of bordisms has recently become important in contemporary mathematics, in particular, because of developments in topological quantum theory and quantum gravity. A semantics of MLL underlying the multi-dimensional syntax is based on a certain category of bordisms, which we call ‘coherent space-times’. The resulting model has an extremely intuitive geometric description. The dual multiplicative connectives $\otimes$ and $\smash{\raise5.99pt\hbox{\rotatebox{-180}{\&}}}$ correspond simply to disjoint unions and connected sums of bordisms. Following ideas from topological quantum field theory, we also discover deep relationships between this new model and the author's coherent phase spaces model (Slavnov 2003), which is based on the context of symplectic geometry.