We wish to announce the following preprint: The logic of weakly distributive categories I: Two sided proof nets with units R. Blute R.A.G. Seely Abstract We define a two sided notion of proof nets, suitable for logics, like the logic of weakly distributive categories, which have the two-tensor structure (with/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 sequentialisation theorem for these nets and the corresponding sequent calculus, and deduce the coherence theorem for weakly distributive categories as an application. We extend these techniques to cover the case of non symmetric tensors ("planar logic"). One significant feature of this version of proof nets is that we are able to include the units for the tensors in our presentation. With this, we are able to extend these nets to the full case of multiplicative linear logic (with units), and prove sequentialisation there. This represents an improvement over the treatment via one sided nets, which cannot handle the units successfully. ==================================================== The preprint may be obtained by anonymous ftp from triples.Math.McGill.CA (132.206.150.30) in the usual manner, or by contacting one of the authors. Via ftp: Login as anonymous, use your email ID as password. The various files are located in the directory pub/rags/nets You will find a PostScript file, a DVI file, and the TeX source code. If you want to take the TeX source code, read the nets.README file first, to find out what macro files are also necessary. (And for other instructions.) At the moment only the extended abstract will be found in this ftp directory; shortly the full paper (including other results, such as conservativity of the extension from weakly distributive categories to *-autonomous categories, in the unit-free case,) will be placed there as well. If you wish to be notified of such "upgrades", drop one of us a line. (Or just browse, from time to time.) Authors' address: Department of Mathematics McGill University 805 Sherbrooke St. W. Montreal Quebec H3A 2K6 Canada FAX: (514) 398-3899 Phone: (514) 398-3804 Authors' email addresses: Blute: blute@triples.math.mcgill.ca Seely: rags@triples.math.mcgill.ca
participants (1)
-
rags@triples.Math.McGill.CA