FOM: Founations of naive category theory?

[Solomon Feferman]

I appreciate Robert Tragesser's bringing attention to my distinction
between local and global foundations in the discussion of SET vs. TOP.
The stand-off here between these when conceived to be all-encompassing
schemes continues with each side dug in and shoring up its defences.  I
have already stated my position in that respect ("Toposey-turvey", Jan.16,
19:15) and I don't aim to repeat my cabbage twice on that.  Robert has
tried to suggest one way that the discussion could more profitably be
channeled, namely to see where in mathematics each of the two ways of
thinking is really appropriate, where they pay off (and, I suppose, why
in those places).  I would not myself call such redirection an example 
of local foundational work, but it is quite a reasonable line of
questioning that is not freighted with ideology.  

Our valued moderator, Steve Simpson, has been promoting a bottom-up view
of f.o.m., starting with the "List 1" absolutely fundamental
concepts, preoccupation with which has led to the kinds of entrenched
opposing positions that have occupied so many of the postings here.
Certainly these have to be dealt with in one way or another,  but insofar
as the views concerning them may come down to fundamentally different
postions regarding ph.o.m., they do not per se lend themselves to making
progress in f.o.m.  It's not that I'm averse to ph.o.m.; far from
it--indeed I think it is or should be the driving force for why we should
care about f.o.m.  But, as Martin Davis has rightly stressed, progress
there has mainly been made by solving certain problems, and those problems
are met all over the place for all sorts of reasons.  The solutions of
those problems may lead to reconsiderations of the foundations right down
to the bottom, but focusing on the bottom may lead one to be mired there
without any genuine progress. End of sermon.

I drew attention to the different ways in which local foundational work is
actually and profitably pursued in my posting "Working foundations" of
Nov.12, 13:10.  In the articles (referenced there) from which that is
drawn, under "Dealing with problematic concepts and principles", I
mentioned particularly the problem of representing what one might call
naive category theory in a faithful, yet demonstrably consistent way.
Now Simpson might say: this is no more a proper subject of f.o.m. than
proper foundations for infinitesmal analysis, or algebraic geometry or the
Dirac delta function.  Let me try to explain what the problem is, and why
that makes it a (local) problem in f.o.m. according to my lights.  This
explanation is drawn from an lecture that I gave at the 7th Scandinavian
Logic Symposium, held in Uppsala in August 1996, under the title "Three
conceptual problems that bug me".  I had not prepared the lecture for
publication, but I will put it on my ftp site before too long (I also have
some hard copies I can send out in the meantime to interested readers). 

The general problem here is that of self-applicable structural concepts.

The mathematical notion of category isolates an interesting mathematical
structure on the class of structure-preserving maps ("morphisms") between
all structures of a given kind.  Pursued informally, one is naturally and
directly led to the following two requirements:

(R1)  For each usual kind of mathematical structure for which we have some
usual notion of structure-preserving morphism, there is the category of all
structures of that kind, e.g. the category Grp of all groups (group
homomorphisms), the category Top of all topological spaces (continuous
maps), the category Cat of all categories (functors).

(R2) For any two categories A and B we have the category (A->B) of all
functors from A to B (with natural transformations as morphisms).  

(R1) and (R2) may be considered to be partial requirements (or criteria)
on a framework that it must meet in order to permit direct expression of
self-applicable structural concepts.  Thus far, one has only provided
frameworks for versions of (R1) and (R2) which are essentially restricted
in one way or another.  Thinking of structures as objects (A,...) with one
or more domains A, which are collections of objects, on which are defined
some relations, operations, etc., it is natural to think of what has to be
accomplished as being part of some broader framework in which we have the
following familiar closure conditions of an [informal] set-theoretical
nature on objects, collections and operations:

(R3) (i) The set N of natural numbers is among our collections.
     (ii) For any objects a and b, we have the ordered pair (a,b)
     (iii) For any collections A and B we can form their union,
intersection, difference, cartesian product, cartesian power, collection
of all subcollections, etc.
     (iv) For any sequence of collections <B_x> indexed by x in A, we have
the collections given by union, intersection, product and disjoint sum of
the B_x's for x in A. 

The obvious first place to look for a (relative) foundation of these
requirements in full or in part is in some system or other of set theory.  
Indeed, (R3) is met if we take all objects, collections and operations to
be sets in ZF or ZFC. But then we can't meet (R1), since there is no set
of all groups, etc.  Various proposals have been proposed for a framework
which meets (R1)-(R3) but only in restricted forms for one or another of
these.  I have described several such proposals in my Uppsala lecture and
won't repeat them here, but what one would like is something that comes
closer to meeting the full requirements than those presently on offer.
The two most familiar ones are Grothendieck's method of universes, and
MacLane's use of GB theory of sets and classes to make a distinction
between small and large categories  (e.g. the large category of small
groups, the large category of small categories, the large category of all
functors from a small category into a large one, etc.) and to distinguish
various large from small collections (e.g. a locally small category is one
which has small hom-sets).  This serves all practical purposes in the
applications of category theory, but is not faithful to the naive
understanding of the concepts involved.  In MacLane's approach, the
distinction is essential for various theorems, e.g. the Freyd general
Adjoint Functor Theorem (of which Freyd said in his Abelian Categories
book that the set-class distinction is "not baroque"), the Yoneda
Embedding Theorem, etc.  It even comes up in homological algebra when
defining the functors Ext^n.  

Now, unlike the naive comprehension principle for classes or collections,
one has the feeling that the informal unrestricted theory of categories
meeting most of the requirements above without universe or large/small
distinctions, can be carried out in a coherent way that is consistent
relative to a presently reasonably accepted formal system.  Over the years
I have made several attempts to come up with such a system, but never to
my complete satisfaction.  That's why it's a conceptual problem that still
bugs me.  These concerns seem to relate to those raised in postings by
Martin Schlottmann and Carsten Butz.  They and others may be interested in
having a look at my attempts so far:

1. "Set-theoretical foundations of category theory", in Reports of the
Midwest Category Seminar III, Lecture Notes in Maths. 106 (1969), 201-247
(with an Appendix by G. Kreisel).

2. "Some formal systems for the unlimited theory of structures and
categories" (Unpublished MS, Abstract in J.Symbolic Logic 39 (1974)
374-375).

3. "Categorical foundations and foundations of category theory", in
*Logic, Foundations of Mathematics, and Computability Theory*,Vol.I,
(1977) 149-169.

(For NF buffs, the attempted solution #2 used an extension of Jensen's NFU
by a stratified pairing operation, needed to explain various structural
notions in a stratified way, and proved consistent a la Jensen.)

The Uppsala lecture also suggested some more recent ideas of mine to base
a solution in one of my theories of functions and classes in the Explicit
Mathematics program, but so far these have not been realized.  

Insofar as a solution to the problem of self-applicable structural notions
cuts across subfields of mathematics, touches on fundamental concepts and
makes use of methods of mathematical logic, I consider this to be an
excellent local problem in f.o.m.  I hope someone will solve it.

Sol Feferman