Geodesic
Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories
Theory and applications of categories, Tome 3 (1997), pp. 85-131

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.

Classification : 03B70, 03F07, 03G30, 18D10, 18D15, 19D23.
Keywords: monoidal closed categories, tensorial strength, coherence, categorical proof theory. 
@article{TAC_1997_3_a4,
     author = {J.R.B. Cockett and R.A.G. Seely},
     title = {Proof theory for full intuitionistic linear logic, 
bilinear logic, and {MIX} categories},
     journal = {Theory and applications of categories},
     pages = {85--131},
     publisher = {mathdoc},
     volume = {3},
     year = {1997},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_1997_3_a4/}
}
TY  - JOUR
AU  - J.R.B. Cockett
AU  - R.A.G. Seely
TI  - Proof theory for full intuitionistic linear logic, 
bilinear logic, and MIX categories
JO  - Theory and applications of categories
PY  - 1997
SP  - 85
EP  - 131
VL  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_1997_3_a4/
LA  - en
ID  - TAC_1997_3_a4
ER  - 
%0 Journal Article
%A J.R.B. Cockett
%A R.A.G. Seely
%T Proof theory for full intuitionistic linear logic, 
bilinear logic, and MIX categories
%J Theory and applications of categories
%D 1997
%P 85-131
%V 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_1997_3_a4/
%G en
%F TAC_1997_3_a4
J.R.B. Cockett; R.A.G. Seely. Proof theory for full intuitionistic linear logic, 
bilinear logic, and MIX categories. Theory and applications of categories, Tome 3 (1997), pp. 85-131. http://geodesic.mathdoc.fr/item/TAC_1997_3_a4/