Logical challenges for category theory
Jonathon Cohen – 7 September 2005
It is commonly assumed that monoidal categories entered the logical arena shortly after Girard's paper on linear logic. What is less well known is that most of what now falls under the banner of linear logic had already existed for many years in the philosophical community, under various different names. Indeed, a fruitful exchange between Saunders Mac Lane and the proof theorist Grigori Mints led to a straightforward proof of the coherence theorem using an old logical technique applied to one of these "philosophical" logics.
There is still much active work on the sorts of logics that Mac Lane and Mints discussed. These are collectively called "substructural" and incorporate, amongst others, linear logic. While the "flat" algebraic semantics of these logics is quite mature, relatively little has been done on the categorical front.
I shall give a categorically phrased introduction to modern nonclassical logic, including a variety of substructural logics. Along the way, we shall see how to construct the centre of a monoidal category in a purely logical way. Several possibilities for future research will be pointed out, including a "grand challenge" for higher dimensional category theory.