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.

TAC Home