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.

TAC Home