Is it possible to formulate category theory without set theory?

Question

I have never understood why set theory has so many detractors, or what is gained by avoiding its use.

It is well known that the naive concept of a set as a collection of objects leads to logical paradoxes (when dealing with infinite sets) that can only be resolved by defining the concept of a set according to a system of axioms.

With this context, can someone please help me to understand the following passage from Categories for the Working Mathematician, Chapter 1, first two paragraphs (emphasis added):

First we describe categories directly, by means of axioms, without using any set theory, and call them "metacategories". Actually we being with a simpler notion, a (meta)graph.

A metagraph consists of objects a,b,c..., arrows f,g,h..., and two operations as follows:

Is it really possible to avoid the use of set theory in the foundations of category theory simply by using the phrase "objects a,b,c ..." instead?

Thanks!

Answer 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.

Answer 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.

Answer 3

It's a somewhat subtle question. As you say, MacLane's definition looks a lot like simply removing the word "set" from the set-based one, which seems fishy. As was also mentioned, a more formal way to make MacLane's claim would be to say something like

A category is a model of the theory $T_{cat}$ whose language has two types $O,M$ and function symbols $s,t:M\to O,i:O\to M$, satisfying the axioms...

Now, this won't really work, because it can't describe composition, for which you need some fancier logic (some notion of "pullback" of types.) But it hopefully clarifies what MacLane is claiming nonetheless.

Leaving the need for composition swept under the rug, two questions arise. Can we study $T_{cat}$ directly without postulating any theory of sets? This would be, essentially, the proof theory of categories, formally viewed as trying to prove theorems involving finite strings of $s,t,i,\circ$ joined via the standard logical quantifiers. Noting the occurrence of the word "finite" in the previous sentence, I think you have to have some ideas about sets to justify proof theory, in particular, some notion of finitude. But in doing proof theory, in this case, syntactic category theory, the question of whether a string is finite never comes up, so that from this angle a category theorist would in practice never need to think about sets explicitly. And even with regard to justification, where we want to really explain what we're doing in a precise way, it doesn't seem you need nearly the full strength of "standard" set theory.

The second question that arises, whose motivation should be clear, is whether there are any categories. I may well be missing some subtlety in the literature on this, but it seems to me that for this you have to either simply accept as intuitive that $\cdot \to \cdot$ and other such inscriptions give examples of models of $T_{cat}$ or else resort to some sort of set theory to define exactly what you mean by that diagram. For me and many others, claiming that the category $\cdot\to\cdot$ exists is no more controversial than claiming that $\{\}$ exists: we don't feel the need to reduce the intuition that there are things and ways to relate things into a more basic intuition that there are things. Some people have claimed that categories are just obviously too complicated to postulate all at once, however, and for them there is set theory. Anyway, all of this is rather solidly at the level of justification, of explaining to a non-category theorist or even to a non-mathematician what exactly are the objects you work with. At the level of practice, none of it is needed at all, although most people find set theory useful for working with categories constructed out of infinite sets.

As an aside, questions about disjointness of homsets should be easily dispatched by the observation that $T_{cat}$ makes no provision for intersections, so that such questions are inherently about the contingent aspects of the model, rather than the theory-so aren't any more meaningful than asking whether every real number has an element which eventually has denominator not divisible by 7.

Answer 4

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

Answer 5

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}

Answer 6

You have asked three questions and so far answers have concentrated on the first one since it is the most polemical.

1. Why does set theory have so many detractors, and what is gained by avoiding its use?
2. What does Mac Lane mean when he says he can describe categories without using set theory?
3. Is it really possible to avoid the use of set theory in the foundations of category theory simply by using the phrase "objects a,b,c ..." instead?

I'll answer the first question last.

---

For the second question, Mac Lane attempts to weasel his way out of discussing logic. He says a metacategory "consists of" objects, arrows, and operations between them. But what he really means is that a metacategory is a collection of objects, a collection of arrows, and graph-of-function like collections of ordered pairs between them. Formally, a collection, also called a class when working with set theory, is a formula (in first-order logic) with free variables. This is why later on Mac Lane can talk about "the metacategory of all sets".

In my opinion, what Mac Lane calls metacategories should simply be called categories. My reasons are

• Mac Lane's metacategories are elements of the theory, first-order logic, nevermind that they are not objects (e.g. are not sets) that the formal theory is describing. A true metacategory by contrast would consist of all classes (formulas) and "class functions" between them, since such a thing would be part of the metatheoretical analysis of first-order logic.

• Mac Lane is not using standard set theory (ZFC). Instead he is assuming that there is a set closed under all the operations of set theory, i.e. a universe (ZFC+U). He refers to elements of the universe as small sets and to all other sets as large sets. He then has a large category of small sets and a metacategory of all sets. But large sets (i.e. ZFC+U) are (for the basic category theory he's doing) merely a way to get at the classes and metacategories of ZFC without having to think about first-order logic.

---

The answer to the third question is no. This is because Mac Lane's metacategories depend on what you have axiomatized using first-order logic. Most of category theory really is the study of the metacategories that arise when you axiomatize set theory. In turn, this is because set theory is used as the foundation of modern mathematics and we would like category theory to be applicable to modern mathematics. The use of universes and large vs small sets is primarily a way to make the application of category theory to modern mathematics easier and more convenient.

A very thorough discussion of how category theory interacts with set theory is Mike Shulman's Set Theory for Category Theory, though it does presuppose some familiarity with category theory.

However, there are other mathematical theories of independent interest, such as Peano arithmetic, which certainly do not require you to axiomatize set theory to do mathematics with. In particular, the metacategories of Peano arithmetic are related to computability theory; sadly I don't know any good references for this -- most everyone does tend to stick to modern mathematics and hence does everything with some set theory in mind.

---

The answer to the first question is that set theory doesn't actually have many detractors. Rather its detractors are quite vocal but many of the usually given objections are frankly irrelevant.

Currently, my primary objection to set theory is that it's purpose from a purely logical perspective is to mimic higher-order logic inside first-order logic. But why not just directly use higher-order logic (even better: dependent type theory) instead of trying to mimic it in first-order logic? Furthermore, logical systems naturally have the structure of fibred categories, so from a more modern viewpoint set theory ought to be presented as a fibred category satisfying appropriate conditions (this is what a topos is; a mind-blowing reference for some of this stuff is Jacobs' Categorical Logic and Type Theory).

My secondary objection is that set theory and first-order logic are actively harmful when it comes to learning type theory or more advanced algebraic geometry. One has to actively unlearn some (tacitly) internalized set-theoretic expectations in order to grok those subjects (types are not sets, the "points" of schemes seem weird).