We wish to announce the following paper, which has been placed on the triples web and ftp site (urls given below). Finite sum - product logic J.R.B. Cockett R.A.G. Seely University of Calgary and McGill University robin@cpcs.ucalgary.ca rags@math.mcgill.ca Brief Abstract: In this paper we describe a deductive system for categories with finite products and coproducts, prove decidability of equality of morphisms via cut elimination, and prove a "Whitman theorem" for the free such categories over arbitrary base categories. This result provides a nice illustration of some basic techniques in categorical proof theory, and also seems to have slipped past unproved in previous work in this field. Notes: Since this material might seem rather close to the sort of categorical proof theory done in the past 2-3 decades, we feel we ought to point out some features which distinguish it from what others have done. Some comments concerning its novelty might help the reader attune himself to some points that otherwise might slip past unnoticed. We present a correspondence between the doctrine of categories with finite sums and products (without any assumption of distributivity), and a "Lambek style" deductive system. But note that unlike the work of Joyal's on the bicompletion of categories, our construction of the free category does not use an inductive chain of constructions, alternating between completions and cocompletions. In this finite case, it is natural do both finite completions (but only for sums and products) in one step. Our proof of cut elimination and Church--Rosser does not make sense without finiteness however. A comment: decidability for categories with finite sums and products seems a result that we ought not to have overlooked all this time, but we cannot find any reference to this in the literature. Of course, comments are welcome. Next, unlike the related work on categories with finite products (or sums, but not both), with or without cartesian closedness, we cannot rely only on directed rewrites ("reductions") but must also make essential use of two-way rewrites (which we might call "equations"). Hence we need to use the theory of reduction systems modulo equations; in particular, we need to strengthen an old result of Huet's in this connection. Our use of such systems to provide a decision procedure for the equality of derivations is not particularly common in categorical cut elimination, but it was a key ingredient in our earlier work on linearly distributive categories and *-autonomous categories [BCST]. Its reappearance here in a slightly different guise is one of the highlights of the present paper, we think. Finally, we drawn the reader's attention to the fact that in setting up the equivalence relation for the category induced by the deductive system, we need not assume the categorical axioms of identity (apart from atomic instances) and associativity - these follow from the cut elimination process. This is not unusual in working with free logics, but may be somewhat less familiar to the reader in the present case of logic over an arbitrary category. Small points individually, but together they give this result a slightly different flavour from its long-familiar relations. ............................................. The paper may be found on the McGill ftp site ftp://ftp.math.mcgill.ca/rags/sigmapi/sigmapi.ps.gz or from rags' web page http://www.math.mcgill.ca/rags ================== R.A.G. Seely <rags@math.mcgill.ca> <http://www.math.mcgill.ca/rags>