### Girard on the Limitations of Categories

#### Posted by David Corfield

What do people make of Jean-Yves Girard’s entry for CATEGORY in his paper Locus Solum?

Category-theory played an important role in the disclosure of the deep structure of logic : for instance coherent spaces form a categorical model for linear logic, and by the way came from this model, not the other way around. The pregnancy of categories in our area made me style the period 1970-2000 as the

time of categories, a period which opened with the Curry-Howard isomorphism. Ludics originates in the category-theoretic approach, but eventually took some distance.The limitations of categories–insofar as we can judge them from the sole logical viewpoint–lies in their spiritualism, their extreme spiritualism :

everything is up to isomorphism. In particular categories cannot explain locative logical constructions such as intersection types–or if you prefer, the categorical viewpoint compelled us to consider these artifacts as non-logical. In the same way, category-theory cannot explain the prenex form of ludics, which are based onequalitiesand which are definitely impossible to explain by means of isomorphisms.To sum up, category theory only presents a limited aspect of logic; provided we realise this, it remains a very important tool. (Locus Solum, pp. 96-97)

He has later entries on LOCATIVE LOGIC and on PRENEX FORM.

We were wondering back here whether higher categories met other demands of his.

Posted at July 23, 2008 9:47 AM UTC
## Re: Girard on the Limitations of Categories

I agree that the

up to isomorphismaspect of category theory is overstated by category-theoreticians. Allow me to be provocative by in turns stating that many essential categorical structures found in nature are strict anyway: if one is dealing with three systems there is no reason why we should first associate two of these before associating the third one. The natural isos only come in when one wants to model these structures in set-theoretic terms. But this is not necessary if one is happy with a purely diagrammatic formalism, which is inherently strict. So the problem is not category theory but the flavour of it one prefers.I seem to remember a story of Lawvere punching out Girard. Does anyone have details on this?