Linear Logic without Units

Abstract

We study categorical models for the unitless fragment of multiplicative linear logic. We find that the appropriate notion of model is a special kind of promonoidal category. Since the theory of promonoidal categories has not been developed very thoroughly, at least in the published literature, we need to develop it here. The most natural way to do this - and the simplest, once the (substantial) groundwork has been laid - is to consider promonoidal categories as an instance of the general theory of pseudomonoids in a monoidal bicategory. Accordingly, we describe and explain the notions of monoidal bicategory and pseudomonoid therein. The higher-dimensional nature of monoidal bicategories presents serious notational difficulties, since to use the natural analogue of the commutative diagrams used in ordinary category theory would require the use of three-dimensional diagrams. We therefore introduce a novel technical device, which we dub the calculus of components, that simplifies the business of reasoning about a certain class of algebraic structure internal to a monoidal bicategory. When viewed through this simplifying lens, the theory of pseudomonoids turns out to be essentially formally identical to the ordinary theory of monoidal categories. We indicate how the calculus of components may be extended to cover structures that make use of the braiding in a braided monoidal bicategory, and use this to study braided pseudomonoids. A higher-dimensional analogue of Cayley's theorem is proved, and used to deduce a novel characterisation of the unit of a promonoidal category. This, and the other preceding work, is then used to give two characterisations of the categories that model the unitless fragment of intuitionistic multiplicative linear logic. Finally we consider the non-intuitionistic case, where the second characterisation in particular takes a surprisingly simple form.