I don't pretend to understand what category theory has to say about the foundations of mathematics, but I would rather like to understand. To that end these notes are compiled recording my impressions, such as they are, about the why Category theorists have misgivings about classical set theory as a foundation for mathematics and what (if anything) they would like to offer in its stead.
Many categories are categories of all examples of a particular kind of mathematical structure (or of all models of a particular theory). Such collections are problematic in set theory in the same way as the set of all sets. In consistent set theoretic foundations based on the iterative conception of set they can be proven not to exist. Though there are techniques which can be employed to mitigate these difficulties, the solutions are not entirely satisfactory, and the view that set theory is not a natural context in which to do category theory may persist. For more on this kind of problem, see:[Hatcher82], Chapter 8, Introduction and Section 3. Furthermore, certain kinds of construction which are important in category theory cannot reliably be done in set theory, for similar reasons, see [Hatcher82] Ch.8 Section 4.
Category theorists have contributed to views on how mathematics should be done, with a particular emphasis on abstraction, relative to which more traditional accounts of set theory now appear unsatisfactory. Among the problems are:
For example, the ordered pair constructor is typically defined in set theory by an explicit recipe for the construction of an ordered pair from its constituents. From the more abstract perspective of category theory, pairing would be treated without chosing any specific way of constructing pairs. Pure mathematicians are generally interested in objects as examples of mathematical structures, and think of these only "up to isomorphism", i.e. without regard for any particular representative of a kind of structure. The practice of chosing a specific method of constructing a type of mathematical object in this context appears to be insufficiently abstract.
Related to the trend toward abstraction is a preference for understanding the structure of mathematical objects by showing how the structures of different objects are related. This is contrasted with talking about these structures by referring to the constituents from which they are built. Thus category theory prefers to avoid talk about elements, and a category theoretic approach to set theory would emphasise talking about the structure of the category of sets through talk about the morphisms within the structure rather than talk about sets and their elements. As in combinatory logic, variable binding constructs are out, and, one step further, composition takes over from application as the primitive constructor of choice (avoiding mention of the elements to which functions are applied).
First a brief restatement of "the problem", which is to find some alternative to classical set theories which would fix the problems mentioned above and also touched upon in [MacLane71], Chapter I, Foundations and discussed in [Hatcher82], Chapter 8, Introduction and Sections 3 and 4.
This is still pretty much of a muddle to me and I invite comments on this material, especially from anyone who can clarify any of the approaches (preferably by means other than referral to a weighty tome which I may not have the time to read), or identify other approaches, or give links to relevant online materials.
Here I attempt a classification of the approaches of which I am aware to fixing problems in classifications perceived from the standpoint of category theory. Let me emphasise, for those of you to whom this is not obvious, that I don't understand most of this work.
I will discuss this under the following headings:
It is often recognised that some of the problems which category theory has with set theory are due to the restricted forms of set comprehension available. i.e. they are to do with the non-existence of things that you might wish existed (e.g. the category of all groups, the category of categories) which don't exist for exactly the same reasons that the set of all sets doesn't exist.
It is sometimes recognised that not all set theories (among the exceptions are those of Quine) share these constraints, but I've never seen anyone suggest that a non-well founded set theory should be used, or any analysis of how well this works. (another possibility is to use some other kind of non-well-founded foundation system, such as an illative combinatory logic). Presumably when you get the universal set and such goodies you loose something else which is important (e.g. cartesian closure, though I don't know whether that is important).
Even if you don't like this idea, you should bear in mind that insofar as the problem is these ontological weaknesses, tinkering with classical set theory but leaving it well-founded is not going to make much difference.
That's too strong. There are two other ways of ameliorating the ontological problems. A traditional way of weakening the constraints imposed by well-foundedness is to introduce some kind of polymorphism (this is usually thought of as overcoming rigidity in type systems, but you get exactly the same problems in untyped well-founded systems, which is one of the reasons category theorists don't like classical set theory). Set theories admitting classes or universes can also help, and sometimes you get hybrids of these various approaches (e.g. dependent type theories with universes).
There seem to have been many variants on classical set theory proposed by category theorists or others inspired by category theory. I have to confess I havn't a clue what most of them are supposed to do.
Let me first mention the things that do make sense to me. It is common to use a set theory with classes in preference to one without, e.g. NBG rather than ZFC (Mac Lane does this in "Categories for the Working Mathematician" [MacLane71] ). This leads to the distinction between small and large categories, and you find that you can have a category of all groups (say) but only of all small groups (which are sets) and it is a large category (i.e. its "hom-sets" are classes). Similarly, you get a category of all categories, but only a large category of all small categories (which isn't a member of itself). One step further is to use a set theory with a "Universe" (Mac Lane [MacLane71] also discusses use of a universe, and in Cohn's Universal Algebra a set theory is adopted in which every set is a member of a universe, giving a hierarchy of universes). These are palliative, and with them category theorists may grudgingly get by.
One I've tried myself is the use of a polymorphic higher-order logic (I've tried this with the cambridge HOL system, and you do get to reason about the category of categories, but it isn't exactly the category you might have hoped it to be). I doubt that would appeal to a category theorist.
There seem to have been lots of other proposals which I don't understand. Some of them are weaker than ZF, on the grounds that the strength isn't needed. Some of them are stronger (don't know why). Some of them are intuitionistic (which in itself makes no difference to strength). In the latter case the initial motivation may come from the connection between Topos theory and higher order intuitionistic logic (whose models are the toposes). As far as I am aware these proposals stick with well-founded set theories.
There seems to me to be a big difference between using set theory as a foundation for mathematics (and what kind of set theory you need to do that), and studying set theory as a subject in its own right. In terms of logical foundations, set theory is primarily about ontology, which is in turn primarily about providing a framework in which mathematics can proceed by definition, or, more liberally, by conservative extension.
Topos theory is the platform from which category theory approaches set theory. This solves some of the problems which category theorists may have with the way in which set theory is done. However, its not clear to me whether or how this solves the problems arising from the well foundedness of classical set theory. (this isn't saying much!)
This isn't a serious proposal but a little game I played, which has some minor merit perhaps in making people think about what they mean by founding mathematics in category theory rather than set theory.
When you found mathematics in set theory, what you do is take a universe in which there are lots of sets, and use these as the raw material in which to do mathematics. (or else you are just using them as raw material to establish the consistency of conservative extensions).
If you ask "so what would it be like to found mathematics on categories rather than sets?" the naive answer would be "You construct a universe in which everything is a category and use that as the raw material for doing mathematics."
Now would that be possible?
Well I did spend some time, for reasons not connected with category theory, playing with foundational systems which are similar to set theory except that the things in the universe aren't sets. The simplest example I worked with was a theory of pure functions, which was closely analogous to set theory except that everything in the universe was a function. At one point when I was engaged in this kind of foundational innovation it occurred to me that one could just as well do it with categories. It seemed at the time that a two sorted theory involving both categories and functors would be nicest. I spent a small amount of time on this but the construction I first attempted failed (because I tried to inject some "up to isomorphism" constraint on the ontology and the universe collapsed). However I don't have the slightest doubt that it can be done, though my most recent inclinations have been to do the construction in the first instance just with functors.
What you would get would be a foundation system equal in strength to ZFC in which the ontology was entirely category theoretic. It is instructive (if at all) only in ruling out this intepretation of category theoretic foundation, since I doubt that it would solve any of the problems which have been raised. Though it certainly would yield a foundation for mathematics as a theory of categories (or functors). I'm still curious to find how it works out.