Finite sum – product logic
J.R.B. Cockett, R. A. G. Seely · Theory and applications of categories · 2001
. 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. Introduction In the late 1960's Lambek introduced the notion of a "deductive system", by which he meant the presentation of a sequent calculus for a logic as a category, whose objects were formulas of the logic, and whose arrows were (equivalence classes of) sequent derivations. He noticed that "doctrines" of categories corresponded under this construction to certain logics. The classic example of this was cartesian closed categories, which could then be regarded as the "proof...