We wish to announce that the following paper may be obtained by anonymous ftp (details below) or directly from the authors. Natural deduction and coherence for weakly distributive categories by R.F. Blute, J.R.B. Cockett, R.A.G. Seely, T.H. Trimble (The abstract follows, but first let us highlight some points for two specific audiences:) Some points that might interest categorists: * Proof of coherence for weakly distributive categories. (These are a natural generalization of monoidal categories to include a second "interwoven" tensor, the interweaving given by tensorial strength - the "weak distributivities".) * New uses of logical techniques to prove coherence: proof nets and empires (from linear logic). * Conservativity of the extension to *-autonomous categories. (Here we mean that the unit of the adjunction is fully faithful.) Some points that might interest linear logicians: * By studying the weak fragment of linear logic that weakly distributive categories represent, one can better get to the structure of PAR vis a vis TIMES (without duality confusing the issue). * Units are handled in a constructive version of the usual treatment: we introduce "thinning links" to attach units to the net structure so as to preserve the "acyclic and connected" net criterion, and then determine how these links can be moved about without disturbing the essential structure (coherence). * Coherence represents (part of) the structure of the proof theory of logic, namely when do proof structures represent "the same proof". ========================================================================== ABSTRACT We define a two sided notion of proof nets, suitable for categories, like weakly distributive categories, which have the two-tensor structure (TIMES/PAR) of linear logic, but lack a NEGATION operator. These proof nets have a structure more closely parallel to that of traditional natural deduction than Girard's one-sided nets do. In particular, there is no cut, and cut elimination is replaced by normalization. We prove a sequentialization theorem for these nets and the corresponding sequent calculus, and deduce the coherence theorem for weakly distributive categories. We also extend these techniques to cover the case of non-symmetric ("planar") tensors. We further extend the treatment of coherence to include the units for the tensors, giving a characterization of the Lambek equivalence relation on deductions (i.e. equality of morphisms) in terms of the notion of empire. Finally, we derive a conservative extension result for the passage from weakly distributive categories to *-autonomous categories. ========================================================================== To obtain a copy by anonymous ftp, ftp triples.math.mcgill.ca and login as anonymous - use your email address as password; cd to the directory pub/rags/nets and take the appropriate file: either nets.dvi.Z or nets.ps.Z (you will have to uncompress them at your own site). Contact rags@math.mcgill.ca if you have any trouble with the ftp process or with printing the files at your site. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++