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