Geodesic
Natural deduction and coherence for non-symmetric linearly distributive categories
Theory and applications of categories, The Lambek Festschrift, Tome 6 (1999), pp. 105-146

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

In this paper certain proof-theoretic techniques of [BCST] are applied to non-symmetric linearly distributive categories, corresponding to non-commutative negation-free multiplicative linear logic (mLL). First, the correctness criterion for the two-sided proof nets developed in [BCST] is adjusted to work in the non-commutative setting. Second, these proof nets are used to represent morphisms in a (non-symmetric) linearly distributive category; a notion of proof-net equivalence is developed which permits a considerable sharpening of the previous coherence results concerning these categories, including a decision procedure for the equality of maps when there is a certain restriction on the units. In particular a decision procedure is obtained for the equivalence of proofs in non-commutative negation-free mLL without non-logical axioms.

Classification : 03B60, 03F05, 03F07, 03G30, 18D10, 18D15.
Keywords: categorical proof theory, linear logic, monoidal categories. 
@article{TAC_1999_6_a8,
     author = {Robert R. Schneck},
     title = {Natural deduction and coherence 
for non-symmetric linearly distributive categories},
     journal = {Theory and applications of categories},
     pages = {105--146},
     publisher = {mathdoc},
     volume = {6},
     year = {1999},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_1999_6_a8/}
}
TY  - JOUR
AU  - Robert R. Schneck
TI  - Natural deduction and coherence 
for non-symmetric linearly distributive categories
JO  - Theory and applications of categories
PY  - 1999
SP  - 105
EP  - 146
VL  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_1999_6_a8/
LA  - en
ID  - TAC_1999_6_a8
ER  - 
%0 Journal Article
%A Robert R. Schneck
%T Natural deduction and coherence 
for non-symmetric linearly distributive categories
%J Theory and applications of categories
%D 1999
%P 105-146
%V 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_1999_6_a8/
%G en
%F TAC_1999_6_a8
Robert R. Schneck. Natural deduction and coherence 
for non-symmetric linearly distributive categories. Theory and applications of categories, The Lambek Festschrift, Tome 6 (1999), pp. 105-146. http://geodesic.mathdoc.fr/item/TAC_1999_6_a8/