62
$\begingroup$

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!

$\endgroup$
  • 11
    $\begingroup$ What Mac Lane is trying to say, in more technical language, is that (meta)categories are models of a certain first-order theory. However, he then goes on to say that he will primarily work with categories that actually exist inside the universe of set theory. $\endgroup$ – Zhen Lin Nov 8 '15 at 18:57
  • 4
    $\begingroup$ ZFC is a theory of well-founded, rooted, rigid trees; there's a lot of internal structure in ZFC sets that we don't necessarily want. $\endgroup$ – Hurkyl Nov 9 '15 at 4:37
  • 2
    $\begingroup$ Russell's paradox happens in CT, too. And independently, you can take CT as a base formalization and embed set theory in it (similar to the usual reverse situation to bootstrap people into understanding of category theory by starting off stating CT in terms of sets of objects, morphism, etc.) $\endgroup$ – Mitch Nov 9 '15 at 19:43
  • $\begingroup$ Dear @DVD: the remark about embeddings in $R^3$ seems to miss the point of the question. This OP is about a serious concern for formalization from the ground up. Then your suggestion to take subsets of $R^3$ as the 'primitives' is not an option, since constructing '$R$', which supposedly is to mean 'the' real numbers, is itself problematic. And if your suggestion is to rely of some "subjectively [...] real space", then this is not 'mathematics' as usually construed nowadays, if only for the empirical fact that opinions are divided whether Euclidean space is 'the' 'real' space. $\endgroup$ – Peter Heinig Oct 8 '17 at 15:20
29
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ If you would have used Common Lisp as an example, rather than its far stricter cousin Scheme, I would have linked here to Paul Graham's essay about how Common Lisp was used to give them the edge in the early days of web shopping, paulgraham.com/avg.html $\endgroup$ – Asaf Karagila Nov 9 '15 at 14:25
  • $\begingroup$ Thanks for the link. I am not sure that Common Lisp is as untyped as Scheme, and I wanted an example of a language that is untyped to the maximum extent possible. $\endgroup$ – Carl Mummert Nov 9 '15 at 14:27
  • 1
    $\begingroup$ That's true - in assembly where you can jump to any address and where you can read and write data to any address (e.g. theoretical pure assembly), there is also no real separation between data and code or between different types of data. $\endgroup$ – Carl Mummert Nov 9 '15 at 14:38
  • 1
    $\begingroup$ Carl: Yes, and it's always fun to write code in real time to memory and execute it from unprotected memory pages. @littleO: I'm not sure that I understand your question. $\endgroup$ – Asaf Karagila Nov 9 '15 at 14:40
  • 1
    $\begingroup$ The purpose of a type system is to prevent you from saying nonsense “by construction”, but Java's and C++'s happen not to be terribly good at that. Both languages ultimately resort to performing dynamic checks in several places (e.g. downcasts), and C++ even allows unchecked unsafe operations (e.g., reinterpret_cast, projection from unions, etc.), with potentially disastrous consequences for the integrity of running processes. $\endgroup$ – pyon Jan 19 '17 at 0:45
26
$\begingroup$

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.

$\endgroup$
  • 16
    $\begingroup$ I am truly intrigued by the remark that the ability to formally write the somewhat meaningful statement "$\Bbb R\in\pi$" makes mathematics harder to learn. How? $\endgroup$ – Asaf Karagila Nov 8 '15 at 21:58
  • 15
    $\begingroup$ @Kevin: That makes no sense. I can ask you infinitely many irrelevant questions in English. Does it make English any easier or harder to learn? One of the things to learn and understand about mathematics, in general, is what questions are relevant at all. If anything, working in ZF does a service that way. $\endgroup$ – Asaf Karagila Nov 9 '15 at 4:32
  • 24
    $\begingroup$ -1 for the "Kool aid" comment, which is needlessly pejorative, and which wrongly suggests that (ZF) set theorists are dullards about foundational matters. Whereas the fact of the matter is that set theory has been an enormous success in foundations. We are proud to have clarified many fundamental and confounding matters, such as those surrounding the axiom of choice, the continuum hypothesis, the ubiquity of logical independence, large cardinals and their connections with descriptive set theory, such as the measurability of projective sets of reals, and many other matters. $\endgroup$ – JDH Nov 9 '15 at 21:09
  • 9
    $\begingroup$ Well, in that case you appear to be suggesting that set theorists are dispensing drugs and misguiding the youth on foundational matters. (Whereas my view is that set theorists have much wisdom on the subject.) Frankly, I don't see that such confrontational name-calling has a place in a philosophical discussion. Why not stick to reasoned analysis and argument? I would encourage you to edit your post. $\endgroup$ – JDH Nov 9 '15 at 21:53
  • 8
    $\begingroup$ @Qiaochu: I don't know any set theorists who would mislead people like that. More likely that these students were misled by people who don't have any reasonable grasp on set theoretic foundations. $\endgroup$ – Asaf Karagila Nov 9 '15 at 21:59
13
$\begingroup$

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

$\endgroup$
11
$\begingroup$

One usually doesn't axiomatically define the notion of set1 — 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

$\endgroup$
  • 1
    $\begingroup$ Your final paragraph reminds me of Greenspun's tenth rule. Especially since Common Lisp was already brought up in this discussion. :-) $\endgroup$ – Asaf Karagila Nov 9 '15 at 20:16
9
$\begingroup$

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

$\endgroup$
7
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ But $T_{Cat}$ doesn't actually capture the vast majority of the reasoning category theorists use - for instance, it does not appear to allow one to reason about functors (within the theory). If one has to move to the metalevel to even talk about functors, how are more complicated category-theoretic notions going to fare? $\endgroup$ – user3589318 Nov 8 '15 at 21:54
  • 1
    $\begingroup$ @user3832080 Guilty. "Functors are just morphisms between models," but then you need a context for your models, so, yes, that would be trouble. You could say functor is a model of the theory of two categories with a function symbol between the two morphism and object types, though. But, right, in the end people who try to really do this end up somewhere like ETCC, I think. $\endgroup$ – Kevin Carlson Nov 8 '15 at 21:58
  • 2
    $\begingroup$ Yes - my point is that you're not formulating category theory within $T_{Cat}$, you're studying models of $T_{Cat}$. Saying that category theory can be formulated within $T_{Cat}$ is like saying logic can be formulated within first order logic (when of course when doing logic, one works within some more substantial metatheory - ZFC, PA, the choice is often irrelevant) $\endgroup$ – user3589318 Nov 8 '15 at 22:02
  • 1
    $\begingroup$ @user3832080 Did I claim that category theory could be formulated within $T_{Cat}$? $\endgroup$ – Kevin Carlson Nov 8 '15 at 22:04
  • 4
    $\begingroup$ First-order logic is (much) more than enough to axiomatise $T_\mathrm{cat}$. One defines composition using a ternary relation symbol. $\endgroup$ – Zhen Lin Nov 8 '15 at 23:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.