#
Proof theory for full intuitionistic linear logic,
bilinear logic, and MIX categories

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

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.

Keywords: monoidal closed categories, tensorial strength, coherence, categorical proof theory.

1991 MSC: 03B70, 03F07, 03G30, 18D10, 18D15, 19D23.

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

http://www.tac.mta.ca/tac/volumes/1997/n5/n5.dvi

http://www.tac.mta.ca/tac/volumes/1997/n5/n5.ps

http://www.tac.mta.ca/tac/volumes/1997/n5/n5.pdf

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

TAC Home