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.

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