#
Finite sum - product logic

##
J. R. B. Cockett and R. A. G. Seely

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. Furthermore, it suggests a type-theoretic approach to 2-player
input-output games.

Keywords: categories, categorical proof theory, finite coproducts, finite products, deductive systems.

2000 MSC: 03B70, 03F05, 03F07, 03G30

*Theory and Applications of Categories*, Vol. 8, 2001, No. 5, pp 63-99.

http://www.tac.mta.ca/tac/volumes/8/n5/n5.dvi

http://www.tac.mta.ca/tac/volumes/8/n5/n5.ps

http://www.tac.mta.ca/tac/volumes/8/n5/n5.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/8/n5/n5.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/8/n5/n5.ps

TAC Home