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.