Is it possible to formulate category theory without set theory?

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

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.

Attribution
Source : Link , Question Author : Matt Calhoun , Answer Author : Carl Mummert

Leave a Comment