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 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
draw 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.