FOM: Categorical foundations, pro and con

[Vaughan R. Pratt]

My apologies to Sol for that misattribution.  (I realized halfway
through that Torkel hadn't attributed the quote to Kreisel and went
back and deleted the reference to Kreisel in the body of my message,
but forgot it was also in the subject line.  Sigh.)


From: cxm7 at po.cwru.edu (Colin McLarty)
>>... Thus the foundations of category theory must be given
>>in terms of some sort of theory of operations (or functions) and
>>collections (or classes),
>    
>    	This seems to me quite wrong. [...]
> [..,] categorical foundations do not begin with a class of 
>objects and one of arrows. They begin by positing arrows and a composition
>relation, and stating assumptions about them.

Colin is exactly right here, but it is easy to miss an absolutely
crucial point that he makes towards the end of his message, without
which it is not at all apparent what the problem is with Sol's
argument.

One could easily suppose Sol and Colin were talking at crosspurposes.
For Sol, set theory is the theory of the sets forming the ZF
universe---the individuals in the theory are sets.  For Colin, category
theory is the theory of the objects forming a single category---the
individuals in the theory are objects.

This looks on the face of it like a mismatch between levels.  Surely
category theory in the sense of a universe whose individuals are
categories requires those individuals to somehow form a set of arrows,
which is Sol's point.

The crucial point Colin makes is:

>One well known first order extension of this theory specializes
>it to categorical set theory, another to a categorical theory of
>categories and functors.

Here's my understanding of the official category theory line on the
latter, Colin can correct my misimpressions.

The latter allows the machinery that has been previously developed for
categories in general, *as the universe*, to be brought to bear on the
description of a universe whose individuals we now wish to be
categories.  At no point is there any need to interpolate a notion of
set so as to say that a category is a set of arrows.  What is true of
the categories and functors constituting respectively the objects and
arrows of the category of categories can be said in first order logic
without bringing in any notion of set.

Unless a suitable category of sets is postulated, "the" underlying set
of a category as an individual in the category of categories is
nonexistent and a meaningless concept in category theory.

That's my understanding of the categorical view of this matter, I hope
I'm not too way off base here.

I do have a couple of concerns with this view, the first of which might
well just be due to some misinterpretation of the view on my part.

First, I'd like to know how a category theorist would interpret the
first-order predicate "x is incident on y" (i.e. "object y is either
the source or target of arrow x").  To a set theorist, this predicate
associates to each object y a class of arrows.  In the absence of a
notion of class, what interpretation does a category theorist place on
it?  Certainly not a subcategory of the universe, since for any given y
this class need not be closed under composition.  And there is no
evident alternative structure for this class, which looks awfully like
an unstructured class.

It seems to me that a category theorist is going to have a harder time
than a set theorist explaining the interpretation of sentences of
category theory.

I see this as one of various ways set theory can leak into category
theory.  Leaks such as this need to be plugged one way or another in
order for category theory to retain its purity, otherwise Sol will be
vindicated in the end.  Though to make Sol's argument watertight it
would seem necessary to show the unpluggability of some leak, which
sounds hard.

Second, there is the question of whether Cat is in fact a category as I
think Colin is implying, or should more properly be understood as a
2-category.  But this is easily fixed in the style of Colin's
axiomatization -- start out with not just objects and arrows but
2-cells as well, which is why I was proposing a geometric basis for
Colin's axiomatization.  But this second concern probably takes us too
far afield from the problem at hand.

Vaughan Pratt