Modelling linear logic without units
Robin Houston
Girard's category of proof nets certainly seems to model the
unit-free fragment of multiplicative linear logic. However
the absence of units means that the category is not star-
autonomous. This raises the question: what categorical
structure is required to model proofs in the unitless
fragment of MLL.
It is not sufficient naively to remove the units from
the definition of star-autonomous category, since there
are proofs that make essential use of sequents that are
empty on one side.
This talk proposes a solution, based on the promonoidal
categories of Day. The basic definition is conceptually
simple, but complicated to work with. Therefore I shall
also outline a couple of elementary axiomatisations of
the structure.