by

J.R.B. Cockett and R.A.G. Seely

ABSTRACT

This note applies techniques we have developed to study coherence in
monoidal categories with two tensors, corresponding to the tensor-par
fragment of linear logic, to several new situations, including Hyland and
de Paiva's Full Intuitionistic Linear Logic (FILL), and Lambek's Bilinear
Logic (BILL). Note that the latter is a noncommutative logic; we also
consider the noncommutative version of FILL. The essential difference
between FILL and BILL lies in requiring that a certain tensorial strength
be an isomorphism. In any FILL category, it is possible to isolate a full
subcategory of objects (the ``nucleus'') for which this transformation is
an isomorphism. In addition, we define and study the appropriate
categorical structure underlying the MIX rule. For all these structures,
we do not restrict consideration to the ``pure'' logic as we allow
non-logical axioms. We define the appropriate notion of proof nets for
these logics, and use them to describe coherence results for the
corresponding categorical structures.

Theory and Applications of Categories, Vol. 3, 1997, No. 5, 85-131

http://www.tac.mta.ca/tac/

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1997/n5/n5.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1997/n5/n5.ps

We would draw your attention to the following "highlights":

- we develop proof nets for FILL (as well as bilinear logic - but this latter is shown equivalent to the system of non-commutative *-autonomous categories we studied in an earlier paper [BCST], so that is not new).
- our proof nets seem very like the "naive" sequent calculus that Schellinx has shown does not admit cut elimination; we analyze the apparent "paradox" in claiming a normalization result for this system of proof nets, and relate our work to previous work of Hyland and dePaiva.
- we show several equivalent formulations of bilinear logic = non-commutative *-autonomous categories. One interesting one is that if one requires of a FILL category that a natural transformation equivalent to the tensorial strength given by the weak distributivity is isomorphic, then you get the full bilinear logic.
- we introduce a generalisation of the notion of "nuclear map" suitable for weakly distributive categories, and show the nucleus of a FILL category is *-autonomous.
- we give a rigorous definition of what it means for a category to satisfy the MIX rule (previous attempts dealt only with the existence of the required maps, and not the necessary coherence also needed), and prove a coherence theorem for this doctrine.
- these last two points are linked by the observation that a weakly distributive category satisfies MIX iff its nucleus does. As a consequence we note that "cartesian" weakly distributive categories (where the tensor is cartesian product) must satisfy MIX.

The paper is available by ftp as a
PS
file or as a
DVI
file
as well as on Robert Seely's
WWW home page
and the TAC home page.

For assistance with ftp, please contact rags@math.mcgill.ca.