Is it possible to formulate category theory without set theory?

Solution 1:

From a formal viewpoint it is possible to study category theory within category theory, using the notion of a topos. Topos theory does many things, but one thing it provides is an alternative, category-theoretic foundation for mathematics.

By augmenting topos theory with sufficient additional axioms, it is theoretically possible to re-construct all of ZFC within topos theory. So, if someone can study category theory in ZFC, they can do the same thing by studying category theory within ZFC within topos theory! Or they can just study category theory using topos theory without using ZFC as an intermediate step. A practical challenge to doing this is that the axioms for a topos are arguably more complicated than the axioms for ZFC, which apart from replacement can all be justified in terms of relatively basic properties of sets.

One other way to look at some issues raised in this thread is to look at the notion of type. There is a nice analogy for the difference between ZFC vs. some categorical foundations: it is like the difference bewteen an untyped programming language (such as Scheme) and a strongly typed language (such as Java or C++).

In Scheme and other untyped languages, there is no separation between code and data: given any two objects, we can treat the first as a function the second as an input, and (attempt to) compute the corresponding output. So, for example, we could define natural numbers using Church numerals, treat "$5$" as a function, and compute its value on the ordered pair $(0,17)$. Of course, nobody really does this seriously in practice. Similarly, in ZFC, we can ask whether the $\pi$ is a member of the ordered pair $(8, \mathbb{R})$, although in practice nobody does this seriously.

In Java and C++, there are strict definitions of each data type. For example, if I have a "natural number" object, and I want a "real number" object, I need to convert ("cast") the original object to make it have the appropriate type. Thus I cannot directly add $1_\mathbb{N}$ and $\pi_\mathbb{R}$. This is similar to the way that some categorical foundations handle things. Instead of speaking of "casting", these foundations focus on the "natural inclusion map" from $\mathbb{N}$ to $\mathbb{R}$, etc.

It is worth knowing that there are many other type theories, apart from the ones inspired by topos theory. There is intuitionistic type theory, which is very poweful, and classical second-order arithmetic, which is much weaker but which is still able to formalize almost all undergraduate mathematics.

I believe, as do many working in foundations of math, the the naive informal mathematics found in practice is done in some sort of complicated (and informal) type theory. This makes type-theoretic foundations much more natural for many mathematicians -- many of the objections laid out to ZFC rest on the lack of typing in set theory. Simple type-theoretic foundations would arguably be a more natural formal system than ZFC for many practical purposes, just as Java is a more practical language than Scheme for many purposes.

On the other hand, the lack of typing in ZFC, like the lack of typing in Scheme, is useful for many theoretical purposes, and so it is good for mathematicians to be aware of untyped systems as well. For example, to make a model of ZFC we only need to define one undefined relation, $\in$. To make a model of type theory we have to lay out the system of types, then lay our a domain for each type, and also lay out all the maps between types and operations on each individual type. This is much more complicated. Analogously, it is a common exercise in computer science classes to ask students to write a scheme interpreter in Scheme, or even to write a Scheme compiler in assembly language, but it is not common to ask students to write a full Java interpreter in Java, much less in assembly language.

Solution 2:

ZF set theory, for the sake of specificity, allows you to ask questions that I (and probably many other category theorists) regard as meaningless: because the elements of sets are other sets, for any pair of sets $X$ and $Y$, it's meaningful in ZF to ask whether $X$ is an element of or a subset of $Y$. For example, you can ask whether $\mathbb{R}$ is an element or a subset of $\pi$. My main motivation for avoiding set theory is avoiding these types of meaningless questions, which I believe genuinely make mathematics harder to learn.

(The statements about sets I regard as meaningful are the ones you can make in the elementary theory of the category of sets; for example, you can ask whether two sets are isomorphic, what the limit or colimit of a diagram of sets is, etc.)

(For example, on math.SE I once saw the question "are the homsets in a category supposed to be disjoint or can they have nontrivial intersection?" and the correct answer is that this is a meaningless question, but depending on how deeply someone's drunk the ZF kool-aid, this can be an annoyingly hard explanation to swallow.)

The "objects" in a direct description of categories have the same ontological status as the "sets" in a direct description of models of set theory.

Solution 3:

As Kevin has pointed out in the comments, one possible axiomatisation of "category theory" is the Elementary Theory of the Category of Categories. The best reference I've been able to find is a paper by McLarty (which isn't necessarily Lawvere's original formulation).

In it McClarty lays out a two sorted theory, with one sort of variables ranging over categories, and the other over functors. He shows how from 8 axioms (one a schema), this theory can formulate and prove many standard results of category theory - including properties one might not immediately expect, for instance properties of the category of groups $G$ in a given category $A$ (here $G$ and $A$ are both objects of the theory), and of a monad (triple) on a category.

Thus it is possible that along these lines, axioms could be given which sufficed for the usual reasoning used by category theorists.

However it does not sound to me like this has yet been conclusively done - there are a great many notions that category theorists use (glancing at the titles in the latest issue of one category theory journal, we see strong homotopy, model categories, weak braided monoidal categories, algebraic kan extensions etc), most of which are much more complicated than those McClarty deals with. Moreover, category theorists are always coming up with new notions - for instance, fairly recently (I think..), $\infty$-categories and the like. When formulating these notions, they are not working in ETCC: the constructions used to define a new kind of category and give examples of it are often (at base) in terms of sets - for instance an $\infty$-category has an infinite tower of morphism sets (morphisms, morphisms between morphisms etc). It might be that one day someone will come up with a definition of $\infty$-categories in terms of ETCC: but (to my knowledge) this has not been done, and there is no uniform way of translating the set theoretic characterisations that are actually given of "kinds" of categories (such as $\infty$-categories) into the language of ETCC.

If this is right, it does not appear that axioms have been put forward that suffice for the current practices of category theory (which includes the option of defining new kinds of categories). To this extent, category theory still currently needs set theory to be formulated.

EDIT: Although actually it looks like you can do analogues of lots of set theoretic reasoning in ETCS, so probably also in ETCC, so you might be able to translate the kind of set theoretic constructions I mentioned above into ETCC after all. Possibly the main difference between such categorical theories and set theory is then that which Qiaochu mentions: that the categorical theories do not allow the asking of certain irrelevant questions

Solution 4:

One usually doesn't axiomatically define the notion of set¹ — theories like ZFC axiomatically define a universe of sets, in a similar way that in linear algebra, we don't define vectors, we define vector spaces.

Also note, for example, that the "theory of a vector space" doesn't say that it has a set of vectors, just that there are elements of the theory, which we call vectors. Sets only enter the picture when we ask for set-theoretic models of the theory: that is, we ask for a set and some functions between sets that satisfy the vector space axioms when suitably interpreted in these terms.

The "theory of a category" is the same way; the elements of the theory come in two sorts: objects and arrows. (there are other versions of the theory that use just one sort, for those so inclined) The only time we ask for there to be a set of objects and a set of arrows, or for the objects and arrows to themselves be sets, is when we ask for a set-theoretic model of the theory of a category.

Unlike the case of vector spaces, we aren't always so inclined to limit our attention to just the set-theoretic models; e.g. one might ask to consider the category of all sets and functions between them; naturally, this cannot be a set-theoretic model, because there isn't a set of all sets!

Category theory also develops its own brand of formal logic, and is wont to consider other sorts of models of theories — things like "internal groups" or "internal categories" where we interpret the theory as talking about objects and arrows rather than sets and functions — so there is added incentive to talk about theories in a way that isn't heavily tied to semantics based in set theory.

That said, you can't get away from set theory entirely; first order logic is itself a form of set theory, and higher order logic even more so.

Furthermore, Set (or other categories resembling it) play an important role in category theory, so any approach to foundations that doesn't start with some form of set theory is going to have to develop its own brand set theory to take its place.

^{1: Actually, it's not a bad idea to do so, just that you do so with the trivial theory that has no axioms, no functions, no constants, no relations, no anything, so there isn't much to learn from it}