#
Natural deduction and coherence
for non-symmetric linearly distributive categories

##
Robert R. Schneck

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.

Keywords: categorical proof theory, linear logic, monoidal categories.

1991 MSC: 03B60, 03F05, 03F07, 03G30, 18D10, 18D15.

*Theory and Applications of Categories*, Vol. 6, 1999, No. 9, pp 105-146.

http://www.tac.mta.ca/tac/volumes/6/n9/n9.dvi

http://www.tac.mta.ca/tac/volumes/6/n9/n9.ps

http://www.tac.mta.ca/tac/volumes/6/n9/n9.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.ps

TAC Home