An Elementary Theory of the Category of Sets

January 12, 2014

An Elementary Theory of the Category of Sets

Posted by Emily Riehl

$MathML-enabled post (click for more details).$

William Lawvere’s Elementary Theory of the Category of Sets (ETCS) was one of the first attempts at using category theory as a foundation of mathematics and formulating set theory in category theoretic language. In this post I will outline the content of Lawvere’s paper [Lawvere 1965] and put it in a historical context; suggestions for further reading are at the end. Before I begin, I’d like to thank Emily Riehl, Steve Awodey and the other Kan Extension Seminar participants for their helpful feedback, suggestions, and reading responses to the paper; and, of course, William Lawvere for writing it!

$MathML-enabled post (click for more details).$

Some history

ETCS came about at a boomtime for category theory and the foundations of mathematics. It was the early 1960s; category theory had found its feet and had started being used extensively throughout mathematics, notably in algebraic geometry with the work of Alexander Grothendieck. Around the same time, Paul Cohen developed the technique of forcing, which has since become central to modern set theory. Lawvere had recently written his Ph.D. thesis [Lawvere 1963], which was the first step in his programme of using the category of categories as a foundation. It was therefore fitting that he should want to try his hand at doing set theory inside category theory.

Lawvere’s attempt did not go unopposed, even by the likes of Samuel Eilenberg and Saunders Mac Lane:

His attempt to explain this idea to Eilenberg did not succeed; […] Sammy asked me to listen to Lawvere’s idea. I did listen, and at the end I told him “Bill, you can’t do that. Elements are absolutely essential to set theory.” [Mac Lane 1988]

Unfazed, Lawvere pressed on and in 1964 he published the ETCS paper, which was expanded and reprinted in 1965. What follows is a very brief sketch of its contents; more depth and technical details can be found in the paper itself.

Axioms of ETCS

Before listing the axioms, we should fix some set theoretic notation with category theoretic meaning: given an object $A$ in a category with a terminal object $1$ , if $a \colon 1 \to A$ then we write $a \in A$ and say $a$ is an element of $A$ . If $s \colon S \to A$ is monic then we say $s$ is a subset of $A$ , and write $s \subseteq A$ . We then write $a \in s$ if $a$ factors through $s$ .

The axioms of ETCS consist of the usual axioms for a category $\mathcal{C}$ together with the following eight axioms:

$\mathcal{C}$ has an initial object $0$ , a terminal object $1$ , products $A \times B$ and coproducts $A+B$ of all pairs $A,B$ , and equalisers and coequalisers of all pairs $f,g : A \rightrightarrows B$ . (Thus $\mathcal{C}$ has all finite limits and colimits.)
Every pair of objects $A,B$ has an exponential $B^A$ .
$\mathcal{C}$ has a natural numbers object $\mathbb{N}$ , with zero morphism $\mathtt{zero} : 1 \to \mathbb{N}$ and successor morphism $\mathtt{suc} : \mathbb{N} \to \mathbb{N}$ .
$\mathcal{C}$ is well-pointed, i.e. given any pair of maps $f,g : A \rightrightarrows B$ with $f \ne g$ , there is an element $a \in A$ such that $f \circ a \ne g \circ a$ .
Axiom of Choice: If $f : A \to B$ and there is some $a \in A$ , then there exists a quasi-inverse $g : B \to A$ , which satisfies $f \circ g \circ f = f$ .
If $A$ has no elements then $A$ is an initial object.
If $a \in A + B$ then $a$ factors through one of the coproduct inclusions.
$\mathcal{C}$ has an object with more than one element.

With modern technology we can simplify this list considerably: a model of ETCS is a well-pointed topos with a natural numbers object satisfying the axiom of choice.

In Lawvere’s paper, the axioms are introduced as they are needed, rather than all as one list. As such, it becomes clear which properties held by the category of sets are also held by other categories. Moreover, Lawvere comments on how the axioms interact with each other. For example, since the category $\mathbf{Pos}$ of posets and order-preserving maps satisfies each of the axioms except for #5, the axiom of choice is independent of the other axioms of ETCS.

Mathematics with ETCS

Lawvere demonstrated the usefulness of ETCS as a set theory by proving six mathematical theorems.

Theorem 1 (Primitive recursion). Given a pair of morphisms $f_0 : A \to B, \quad u : \mathbb{N} \times A \times B \to B$ there is a morphism $f : \mathbb{N} \times A \to B$ satisfying, for each $n \in \mathbb{N}$ and $a \in A$ , $f \circ \langle \mathtt{zero}, a\rangle = f_0 \circ a, \quad f \circ \langle \mathtt{suc} \circ n, a \rangle = u \circ \langle n, a, f \circ \langle n, a \rangle \rangle$

The primitive recursion theorem requires only axioms 1-3, and uniqueness of $f$ is implied by axiom 4. Thus primitive recursion can be done in categories such as the functor category $[\mathbb{C}, \mathbf{Set}]$ for any small category $\mathbb{C}$ , and in the arrow category $\mathbf{Set}^{{\rightarrow}}$ .

Theorem 2 (Peano’s postulates).

The morphism $\mathtt{succ} : \mathbb{N} \to \mathbb{N}$ is monic
If $n = \mathtt{succ} \circ m$ for some $m \in \mathbb{N}$ then $n \ne \mathtt{zero}$ .
If $s \subseteq \mathbb{N}$ and $n \in s \Rightarrow \mathtt{succ} \circ n \in s$ then $s = \mathrm{id}_{\mathbb{N}}$ .

The third of these allows us to perform mathematical induction in any model of ETCS.

Theorem 3 (Image factorization). Every morphism can be factored as an epi followed by a mono.

Theorem 4 (Unions). Let $2 = 1+1$ and let $\top : 1 \to 2$ be one of the inclusion maps. Given any $\alpha : I \to 2^A$ there is a subset $u : {\bigcup_{\alpha}} \to A$ such that, for all $a \in A$ , $a \in u$ if and only if $\mathtt{ev}_{2^A} \circ \langle \alpha \circ j, a \rangle = \top$ for some $j \in I$ .

Intuitively, $\bigcup_{\alpha}$ is the union of the subsets of $A$ picked out by the indexing morphism $\alpha$ ; that is, ${\bigcup_{\alpha}} = \bigcup_{j \in I} \alpha(j)$

Theorem 5 (Complements). Let $A$ be an object. Given any subset $s : S \to A$ there is a subset $s' : S' \to A$ , such that $A \cong S+S'$ with $s$ and $s'$ as the coproduct injections.

Theorem 6 (Quotients). Let $A$ be an object and $f = \langle f_0, f_1 \rangle : R \to A \times A$ be an equivalence relation. Let $\pi_0, \pi_1: A \times A \to A$ be the product projections. Then $f$ is the equaliser of $q \circ \pi_0$ and $q \circ \pi_1$ , where $q : A \to Q$ is the coequaliser of $f_0$ with $f_1$ .

Intuitively, $Q$ is the quotient of $A$ by $R$ , then the theorem is stating that $R$ is precisely the set of pairs $\langle a,b \rangle \in A \times A$ such that $[a]_R = [b]_R \in Q$ .

Metamathematics

The paper closes with a theorem justifying that the axioms of ETCS really do characterise categories which are sufficiently ‘like’ the category of sets. Lawvere refers to this likeness as the invariant form of the category of sets.

(Meta)theorem. If $\mathcal{C}$ is a locally small, complete model of ETCS, then $\mathcal{C}$ is equivalent to $\mathbf{Set}$ .

The equivalence $\mathcal{C} \overset{T}{\underset{\check T}{\rightleftarrows}} \mathbf{Set}$ is given by $TA = \text{Hom}_{\mathbf{Set}}(1,A) = \{ \text{elements of } A \}$ $\check{T}X = \sum_{x \in X} 1$

What happened next?

The appeal of ETCS was not felt by the mathematical community at the time. Indeed, according to Marquis and Reyes:

The category of sets was not taken as a foundational framework. It was not studied and explored. […] It seems that one of the most common reactions at the time was that ETCS was merely a translation in categorical terms of the standard axioms of set theory [Marquis and Reyes 2011]

Even Lawvere acknowledged the shortcomings of his work:

However, it is the author’s feeling that when one wishes to go substantially beyond what can be done in the theory presented here, a much more satisfactory foundation for practical purposes will be provided by a theory of the category of categories.

However, the impact of ETCS stems not from its (non-)use as a foundation, but from the research that it led to. It was one of the first attempts to give a categorical account of logic, and it led directly to the definition of an elementary topos, which generalised the notion of a Grothendieck topos and bridged the gap between geometry and logic via category theory. For a number of reasons it was toposes, rather than models of ETCS, which became the central object of study in categorical logic.

References and suggested reading

Lawvere, F.W. Functorial Semantics of Algebraic Theories, Ph.D. thesis, Columbia University (1963).
Lawvere, F.W. An elementary theory of the category of sets, Proceedings of the National Academy of Science of the USA 52, 1506-1511 (1965), reprinted as Lawvere, F.W., McLarty, C. An elementary theory of the category of sets (long version) with commentary, Reprints in Theory and Applications of Categories, No. 11 (2005), pp. 1-35.
Mac Lane, S. Concepts and categories in perspective. In A Century of Mathematics in America, I, vol. I, pages 323-365. American Mathematical Society, Providence (1988).
Marquis, J.-P. and Reyes, G. The History of Categorical Logic: 1963-1977. In Handbook of the history of logic, vol. 6, pp. 689-800. Elsevier (2011).

Posted at January 12, 2014 6:31 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2682

87 Comments & 1 Trackback

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Clive, thank you for this fantastic summary!

I’m hoping that we can use the comments, not just for the broader philosophical/historical/conjectural conversation that the $n$ -Category Café excels at, but also to provide a space to ask and answer smaller questions raised by the paper itself, for those who want to read along with the seminar. I’ll start:

In Remark 5 on the top of page 28, Lawvere mentions three power-set functors, which surprised me, because I was only aware of two.

The contravariant power-set functor is the easiest: it’s immediate from the parametrized adjunction defining the exponentials.

In set-builder notation, the (usual) covariant power-set functor, applied to a map $f \colon A \to B$ , takes $S \subset A$ to

$f_!(S) := \{ b \in B \mid \exists s \in S, f(s)=b\}.$

This is what Lawvere describes categorically on the previous page.

I believe that the third power-set functor (also covariant), when applied to $f \colon A \to B$ , should take $S \subset A$ to

$f_*(S) := \{ b \in B \mid f^{-1}(b) \subset S\}.$

With some work I’m sure this map $2^A \to 2^B$ can be constructed in ETCS, but let me decline to do this right now.

The reason I think this is right is that I remember from somewhere in Peter Johnstone’s topos theory lecture notes that $f_!$ , $f^*$ (meaning precomposition), and $f_*$ should be adjoints.'' Interpretingadjoint” with respect to the posets of subobjects of $A$ and $B$ , I think this is right: we have $f^*(T) \subset S$ if and only if $T \subset f_*(S)$ , which says that $f^* \dashv f_*$ .

What I don’t see (quoting Remark 5), is how $f_*$ is

a dual covariant functor related to universal quantification in the same way that the direct image functor is related to existential quantification.

Can someone clarify?

Posted by: Emily Riehl on January 12, 2014 7:06 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Thanks for your comment!

Another equivalent definition of $f_!$ is given by $f_!(S) = \{ b \in B : \exists s \in f^{-1}(b), s \in S \}$ Then you can, quite literally, replace the $\exists$ with $\forall$ in the definition of $f_!$ , i.e. $f_*(S) = \{ b \in B : \forall s \in f^{-1}(b), s \in S \}$

Posted by: Clive Newstead on January 12, 2014 7:11 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Ah, very good. I didn’t think to use the inverse image in the first definition.

Posted by: Emily Riehl on January 12, 2014 7:40 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Trying to explain this to philosophers, I like to give a concrete example. For some reason I settled on $A$ as the set of dogs, $B$ the set of people, $f$ the function picking out a dog’s unique owner.

Then the two covariant maps take dog predicates to human predicates. E.g., if we take ‘poodle’, it will be mapped respectively to ‘owner of some poodle’ and ‘owner only of poodles’ (to include not owning a dog at all).

Posted by: David Corfield on January 12, 2014 7:18 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Nice!

Posted by: Emily Riehl on January 12, 2014 7:41 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Here is how I remember that there should be three of these functors. If $f:A\to B$ , then of course $f^{-1}:2^B\to 2^A$ preserves unions and intersections, ie

$f^{-1}\left(\bigcup_{C\in S}C\right)=\bigcup_{C\in S}f^{-1}(C)$

and

$f^{-1}\left(\bigcap_{C\in S}C\right)=\bigcap_{C\in S}f^{-1}(C)$

whenever $S$ is a subset of $2^B$ . Viewing posets as categories in the usual way, $f^{-1}$ is a functor from $2^B$ to $2^A$ , and this condition says exactly that $f^{-1}$ commutes with all limits and colimits. Since $2^B$ is complete and cocomplete, it follows by the adjoint functor theorem for preorders that there should be a left adjoint and a right adjoint, which will be maps $2^A\to2^B$ . These are the two covariant powerset functors.

This is nice because it means I don’t have to remember the definitions of all three maps, or which ones preserve unions and which preserve intersections. Instead I just remember that the inverse image preserves both, and then the definitions and properties of the other two follow for free by adjointness.

Posted by: Erik Crevier on January 13, 2014 2:12 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

You meant $S \subset B$ , I think.

Thanks for sharing this mnemonic! It’s very nice.

Posted by: Emily Riehl on January 13, 2014 5:57 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

I think he really did mean $S \subseteq 2^B$ : it’s a collection of subsets of $B$ . Anyway, I agree: it’s a nice way of looking at it. At least, I hope it is, because that’s what I do too.

Posted by: Tom Leinster on January 13, 2014 6:24 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Oh, of course, it’s the index for the (co)limit. My mistake.

Posted by: Emily Riehl on January 13, 2014 6:28 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

In the world of naive set theory, you may think of $f_{!}(S)$ as a left Kan extension $Lan_f S$ of $S\colon A \to 2$ along $f\colon A \to B$ and $f_{*}(S)$ as a Right Kan extension $Ran_f S$ where one think of $S$ as a functor from a discrete category $A$ to a poset $2$ .

If you take $B$ to be a/the terminal object $1$ , then you may think of $f_{!}= \exists\colon 2^A \to 2^1 \cong 2$ and $f_{*}=\forall \colon 2^A \to 2$ .

Posted by: ST on January 20, 2014 2:04 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

With regard to the quotation of Mac Lane, it’s probably a good idea also to record Lawvere’s correction (see here, page 10):

… I never proposed “Sets without elements” but the slogan caused many misunderstandings during the next 40 years because, for some reason, Saunders liked to repeat it. Of course, what my program discarded was instead the idea of elementhood as a primitive, the mathematically relevant ideas of both membership and inclusion being special cases of unique divisibility with respect to categorical composition. I argue that set theory should not be based on membership, as in Zermelo-Frankel set theory, but rather on isomorphism-invariant structure.

Posted by: Todd Trimble on January 12, 2014 9:44 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

I find it hard to see how anyone would think that Lawvere wanted to do away with elements having read the paper, given that they’re the very first thing he defines and he uses them constantly. As Lawvere says in your quotation, the real difference between traditional set theories (ZFC, say) and ETCS is that ZFC is concerned with the internal structures of individual sets via membership whereas ETCS is about how different sets interact via functions. I think a nice example of this contrast can be seen by comparing ZFC’s extensionality, which says “sets are defined by their elements”, with Lawvere’s axiom 4, which says “functions are defined by their values”. This also highlights the importance of elements in both theories!

Posted by: Tom Avery on January 13, 2014 10:59 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Yeah, I think Mac Lane did understand that (ETCS is covered in his book with Moerdijk, and it’s something that Mac Lane thought about a lot). Back in the very early 60’s, maybe what Lawvere had been driving at in his discussions with Mac Lane (pre-PhD) wasn’t as clear.

Lawvere in that interview takes a very balanced view IMO on such comments by Mac Lane. One remark is that the “sets without elements” bit made its way into the posthumously printed autobiography of Mac Lane; Lawvere says that book was rushed into print before necessary corrections could be obtained. It’s generally true that Mac Lane enjoyed telling stories about the old days, for instance the time before Lawvere became legendary, and perhaps not always with perfect scholarly care.

Meanwhile, there is persistent confusion in the mathematical community about category theory wanting to “do away with elements” generally.

Posted by: Todd Trimble on January 13, 2014 2:53 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Meanwhile, there is persistent confusion in the mathematical community about category theory wanting to “do away with elements” generally.

There is also persistent confusion in the mathematical community about category theorists wanting to do away with sets and replace them with categories. As Colin McLarty wrote (Exploring categorical structuralism, p.39):

ETCS is a set theory. It is not a membership-based set theory like ZF. It is a function-based set theory.

Here McLarty is rebutting (what he sees as) a misconception of Hellman. But he also notes:

Mac Lane generally uses the phrase ‘set theory’ to mean ZF, a habit of more than thirty years before ETCS was conceived. But we cannot let his terminology misdirect us.

Posted by: Tom Leinster on January 13, 2014 5:34 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

How does one prove the existence of the “natural number object”? How one does this using the second-order axiom

|X| = |Y| iff X ~ Y

is well-known to logicians and philosophers, since Frege and Russell. It’s sometimes called Frege’s theorem.

But how does Lawvere prove it? Can the proof be written down?

Cheers,

Jeff

Posted by: Jeffrey Ketland on January 12, 2014 11:38 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

The existence of an NNO is an axiom. The theorem you cite cannot be expressed in the language of ETCS without some changes: for finite sets, it is essentially a triviality; for infinite sets, one runs into the problem of not having distinguished ordinals.

Posted by: Zhen Lin on January 13, 2014 1:38 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Yes, so, on Lawvere’s approach, one assumes

(L) There exists a NNO

as an axiom. And Frege does the opposite; one assumes

(F) $|X| = |Y| \Leftrightarrow X \sim Y$

as an axiom. Frege proves (L) as a theorem, based on (F). While, on Lawvere’s approach, (F) will become a theorem based on (L) and a few other things, using some suitable definition for $|X|$ .

However, having thought about how ETCS is meant to work as a foundation, I think assuming (L) as an axiom is kind of cheating. Admittedly, ETCS is to be compared with standard $Z$ set theory, which assumes something like (L) too - i.e., “there is a set containing $\varnothing$ and closed under $x \mapsto x \cup \{x\}$ ”. And the usual set existence axioms are motivated by natural closure conditions, much as Lawvere’s axioms are motivated by analogous closure conditions.

Jeff

Posted by: Jeffrey Ketland on January 13, 2014 4:48 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

How’s it cheating?

Of course, the category of finite sets satisfies all the ETCS axioms except existence of an NNO. So I don’t know where this line of inquiry (“how does Lawvere prove it?”) is going.

Posted by: Todd Trimble on January 13, 2014 7:14 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Todd, the question (a bit tongue in cheek, I admit …) concerned how Lawvere proved the existence of a NNO. The answer is: he assumes it as an axiom. In a sense, that’s ok, as one has to start somewhere, and one can’t start with nothing. (In Z, we assume infinity, which is analogous.) Frege, though and interestingly, proves it, using (F) above, along with comprehension; and we have good reasons to think (F) is true. The result is a theory that interprets second-order arithmetic. So, just assuming there is a NNO can be accused of cheating, at least when compared with a theory that proves the existence of a NNO from what seem like more intuitive axioms/assumptions.

Jeff

Posted by: Jeffrey Ketland on January 13, 2014 9:28 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Surely, using the comprehension scheme is also cheating, since it is (pace Quine) inconsistent?

The fundamental issue is that ETCS does not have a global membership relation. It is not even possible to ask whether ETCS satisfies a comprehension scheme. Thus, Frege-style cardinals are entities that only exist at the meta level. As you know, ZF gets around this problem by identifying each cardinal with a distinguished representative, but this trick is contrary to the principle of isomorphism-invariance.

Posted by: Zhen Lin on January 13, 2014 10:04 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Yes, that’s right for naive unrestricted comp; but, on Frege’s approach, we use second-order comprehension,

$\exists X \forall y(X(y) \leftrightarrow \phi(y))$

$\exists R \forall x, y(R(x,y) \leftrightarrow \phi(x,y))$

That’s all ok. Then we add on

$|X| = |Y| \leftrightarrow X \sim Y$

The resulting second-order theory $FA$ interprets second-order arithmetic, $PA_2$ , and that gives us our NNO. And it proves Dedekind’s Isomorphism Theorem: there’s a recent paper by Simpson & Yokoyama on the reverse math status of this result here.

The fundamental issue is that ETCS does not have a global membership relation. It is not even possible to ask whether ETCS satisfies a comprehension scheme. Thus, Frege-style cardinals are entities that only exist at the meta level. As you know, ZF gets around this problem by identifying each cardinal with a distinguished representative, but this trick is contrary to the principle of isomorphism-invariance.

Yes … not having global notions

$x \in y$

$x = y$

is connected to this “evil” thing/”isomorphism invariance”. Is there a nice definition of “isomorphism-invariance”? It seems to mean something like “the only properties (of mathematical objects) one should talk about are those which are invariant under isomorphism”.

Jeff

Posted by: Jeffrey Ketland on January 13, 2014 10:53 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

As an outsider to this field, the existence of the NNO always has seemed odd to me, for what it’s worth. What do the natural numbers have to do with set theory? Why should they be elevated to a foundational element?

Posted by: Aaron on January 13, 2014 1:15 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Another advantage for univalent foundations, that no specific (higher) inductive type is singled out?

By the way, for anyone who didn’t see it, take a look at Mike Shulman’s account of univalent foundations as taking the best of structural and material set theory.

(It seems nLab’s inductive type still needs some finishing off.)

Posted by: David Corfield on January 13, 2014 1:58 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

And even if you take all ordinary inductive types, such as the natural numbers, it can be seen as an unmotivated limitation, as Mike says here:

I feel like to a category theorist, at least (I can’t say about type theorists), this point of view implies that restricting yourself to ordinary inductive types — initial algebras for free monads — is a weird and artificial restriction. Including higher inductive types is much more natural. (-:

Posted by: David Corfield on January 13, 2014 2:22 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

What do the natural numbers have to do with set theory?

We want there to be a set of natural numbers!

It’s really that simple. I think the fierce image of ZFC sometimes fools people into thinking that set theory has to be some mega-sophisticated thing. It’s really about the most simple objects in the world.

Posted by: Tom Leinster on January 13, 2014 2:00 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

I think I might know what you mean, Aaron. For me, “the natural numbers” is an object with a very algebraic feel. I tend to think of $\mathbb{N}$ primarily as a ring – or rather, a rig. And I think it would be unnatural to stipulate that $\mathbb{N}$ has addition and multiplication operations in the axioms of a set theory.

So maybe what should be emphasized is that the aspect of $\mathbb{N}$ that is axiomatized in a NNO is not this algebraic aspect, but rather the more logic-flavored fact that you can induct over the natural numbers. Maybe this is a drawback of the term “natural number object.” It could just as easily have been called “ $\omega$ -object”.

Posted by: Tim Campion on January 13, 2014 2:19 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

The existence of the NNO always has seemed odd to me, for what it’s worth. What do the natural numbers have to do with set theory? Why should they be elevated to a foundational element?

I think of the concept of natural numbers object as the quintessential expression of recursion. And what after all is set theory, if not a case study in general recursion?

You could look at it this way: the natural numbers starts with $0$ and the rest of $\mathbb{N}$ is generated recursively by application of successor $s$ . Within the category of sets in which it is embedded, it is the universal example of that data $(0, s)$ . Likewise, the cumulative hierarchy starts with an initial element (the empty set) and the universe of sets is generated recursively by applying set-theoretic operations. The analogy is made even stronger and more precise through Algebraic Set Theory, where the universe of sets is conceived as a universal model of a small-complete poset $V$ equipped with a successor operation $s: V \to V$ (conceived as taking a set $x$ to the singleton $\{x\}$ ). In this set-up, the elementhood relation $x \in y$ is recovered as the relation $s(x) \leq y$ .

Posted by: Todd Trimble on January 13, 2014 2:34 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

It’s an interesting discovery of set theorists and type theorists over the past several decades that very often, the additional axioms that we add to our foundational theories to make them stronger take the form of “stronger and stronger axioms of infinity” (in Godel’s foresighted words), or more precisely the existence of longer and more complicated well-founded relations. Set theorists speak of large cardinals, while type theorists speak of inductive definitions. In both cases (ZFC’s axiom of infinity or ETCS’ existence of the NNO), the “smallest nontrivial” such axiom is the existence of $\mathbb{N}$ — it’s the least inaccessible cardinal (at least, if you don’t arbitrarily declare “inaccessible” to include “greater than $\mathbb{N}$ ”) and the most basic inductive definition of an infinite type.

Posted by: Mike Shulman on January 13, 2014 6:47 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

$\mathbb{N}$ the least inaccessible cardinal? Only if you still arbitrarily declare “inaccessible” to include “greater than 0”…

Posted by: Peter LeFanu Lumsdaine on January 14, 2014 10:15 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

The Axiom of Choice in ETCS whispers to me “functions from nonempty sets are Von Neumann regular arrows”; can anybody explain this similarity?

Posted by: Fosco Loregian on January 13, 2014 12:02 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

I agree this is quite suggestive.

Apparently, an element $f$ of a ring is called von Neumann regular if there exists a “quasi-inverse” $g$ such that $f = f g f$ , and the ring is called von Neumann regular if all its elements are.

If we think of a ring as a one-object category with composition given by mulitiplication, then the von Neumann condition is a strengthening of Lawvere’s axiom of choice: von Neumann says that every arrow has a quasi-inverse, whereas Lawvere says that every arrow with nonempty domain has a quasi-inverse.

Google turns up this paper by Borceux and Rosicky, where the von Neumann condition is considered in an arbitrary variety. According the introduction, one class of examples is the category of finitely-presentable (left or right) modules over a von Neumann regular ring.

The upshot is that many natural categories have more choice than $\mathbf{Set}$ does! I suppose the same could be said of the category of nonempty sets, but still I find this surprising.

Posted by: Tim Campion on January 13, 2014 1:38 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Thanks for the reference, they seem to catch exactly my point! What I had in mind was to look at the condition of Von Neumann in a category with only one object. There are a large number of equivalent conditions that characterize a Von Neumann regular ring, and yesterday I wondered if they can be rephrased in some sense. I’ll have a look.

Posted by: Fosco Loregian on January 13, 2014 2:34 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Slightly orthogonally, the triangle equalities for an adjunction have a similarly ‘von neumann regular’ feel to them.

The unit $\eta:1\rightarrow LR$ and counit $\epsilon:LR\rightarrow 1$ satisfy

$L\eta:L\rightarrow LRL$ and $\epsilon:LRL\rightarrow L$

$\eta R:R\rightarrow RLR$ and $R\epsilon:RLR\rightarrow R$

with $L\eta . \epsilonL=1$ and $\eta R.R\epsilon=1$

Apparently a semigroup which satisfies the conditions $fgf=f$ and $gfg=g$ is called an inverse semi-group ‘where they’re used to study partial symmetries’.

This is suggestive of something - but quite what, I’m not sure of.

Posted by: Mozibur Ullah on January 15, 2014 2:36 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Another perspective on this form of the Axiom of Choice is that it is equivalent to the statement “every mono (with nonempty domain) splits, every epi (with nonempty domain) splits, and every morphism (with nonempty domain) has an epi-mono factorisation”. Since no respectable non-trivial epi in a category of sets would have nonempty domain, this implies the perhaps more familiar version of the axiom. Note that the construction of the epi-mono factorisation uses equalisers.

Posted by: Alexander Campbell on January 13, 2014 2:19 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Thank you! This reinforces the idea that there is a strong connection between WFSs on Set and the Axiom of Choice. As far as I can see by now, sections 3,4 of Rosicki/Borceux paper point it out even more neatly (see for Example thm 4.2!).

Posted by: Fosco Loregian on January 13, 2014 3:15 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Certainly, although of course we need to keep the (with nonempty domain) caveat for monos, for if $0 \to 1$ splits then $0 \cong 1$ .

Posted by: Alexander Campbell on January 13, 2014 3:43 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Another highlight: Borceux and Rosicky’s Theorem 3.4 shows under the hypothesis of Cauchy completeness (idempotents split), that any arrow satisfying the von Neumann criterion / axiom of choice factors as a split epi followed by a split mono. So they only need absolute equalizers to get this.

On another note, it appears to me that Borceux and Rosicky’s examples of von Neumann categories are all small. They are concerned with varieties (which are, of course, large and complete), but they only impose the von Neumann criterion on certain small subcategories of varieties – especially the subcategory of finitely presentable objects. Certainly having this amount of choice makes itself felt in the larger structure of the variety, but maybe it was a little overblown of me to say that we’ve found categories with more choice than $\mathbf{Set}$ .

Posted by: Tim Campion on January 13, 2014 4:07 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

I’m excited to see the first of these Kan posts go up, and feel bad that I’m about to write a post that will push this one off the top — but that’s what happens on a blog!

As I currently see it, the greatest conceptual shift when moving from ZF-style set theory to Lawvere-style set theory is in the handling of subsets. In the Lawvere style, we can define a subset of a set $X$ as a map $X \to 2$ , but there is no canonical injection $S \to X$ to which a map $X \to 2$ corresponds — it’s only canonical up to isomorphism. We could choose a representative injection $S \to X$ for each $X \to 2$ , but this seems like an act of vandalism. If we don’t, though, it requires us to think quite differently about what a set is.

Does Lawvere address this point in his paper?

Posted by: Tom Leinster on January 13, 2014 12:34 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

[this is for other people, not you Tom]

In grade school style set theories, sets are made up of atoms that have names (that must be distinct) and questions are asked such as if $A = \{cat, dog, mouse\}$ and $B = \{cat, mouse, pig\}$ then what is $A \cup B$ and $A \cap B$ ?

In material set theory (ZF) there is only one atom, the empty set $\emptyset$ , and all other elements must be constructed from it, though from the multi-atom perspective this can seem silly - if $cat$ etc. are sets then what are the values of $cat \cup dog$ or $mouse \cap pig$ ?

In structural set theory (ETCS) sets are made up of indistinguishable distinct points and if you want to distinctly label a set $S$ then you have to it with an injection $label: S \to Labels$ where $Labels$ has some outside-the-math human interpretation such as $\{dog, cat, mouse, pig\}$ .

there is no canonical injection $S \to X$ to which a map $X \to 2$ corresponds — it’s only canonical up to isomorphism.

The na¯ve notion of subset comes from regarding sets as containing named atoms which does give a canonical injection, however structurally we are no longer talking about subset being an injection between sets but subset being an injection between injections to some set $Labels$ and this is just the slice category $MonoSubCat(Set)/Labels$ , the power set of $Labels$ ( $MonoSubCat(Set)$ is the wide subcategory of Set with morphisms being all injections). This is how subobjects in the topos $Set$ are defined without mentioning the word “topos”.

Regarding subsets as injections to $Lables$ fixes the problem of what does $cat \cap dog$ mean because that question is ill-typed. As injections to $Lables$ we get $\{cat\} \vee \{dog\} = \{cat, dog\}$ and $\{cat\} \wedge \{dog\} = \{\}$ .

(PS. I haven’t been able to find any discussion of $MonoSubCat$ as a particular type of forgetful functor though people tend to use it and $EpiSubCat$ all over the place. Is there any literature on these?)

Posted by: RodMcGuire on January 13, 2014 5:07 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

There was some discussion of Lawvere’s treatment of subsets in the seminar. His official definition (Def 2, p. 17 of TAC edition) says that a subset is a monomorphism, simpliciter. He does define a relation $a \subseteq b$ on subsets of a fixed object $A$ , but he doesn’t give an English name to this relation! Presumably this is because “subset” is already taken. And he doesn’t discuss the possibility of two subsets being equivalent.

One point to notice is that most of Lawvere’s theorem statements are couched in terms of (global) elements. He is careful to introduce the terminology:

An $e l e m e n t$ $x$ of a set $A$ is a map $1 \overset{x}{\to} A$ .

If $a$ is a subset of $A$ ( $\bullet \overset{a}{\rightarrowtail} A$ ) and $x$ is an element of $A$ ( $1 \xrightarrow{x} A$ ), then $x$ is a $m e m b e r$ of $a$ if it factors through $a$ .

I’d speculate that if he wanted to show that two subsets were equivalent, he might just show that they have the same members and leave it at that if possible. But it does seem that there’s no dodging the issue forever.

Posted by: Tim Campion on January 14, 2014 11:16 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

I found that thinking about this paper became slippery whenever the difference between first-order and second-order conditions became important. Here’s an example.

As Clive explained in his blog post, Lawvere’s Metatheorem says:

If $\mathcal{C}$ is a locally small, complete model of ETCS, then $\mathcal{C}$ is equivalent to $\mathbf{Set}$ .

There are two clauses in the statement that depend on the ambient set theory: “locally small” and “complete,” and you need both of them to nail down which category $\mathbf{Set}$ your model $C$ is equivalent to. Suppose that $C$ is equivalent to a $\mathbf{Set}(U)$ for some universe $U$ . If we pass to a larger universe, then $C$ is no longer complete. If we pass to a smaller universe, then $C$ is no longer locally small.

I found this confusing at first because in the paper, Lawvere doesn’t explicitly state that $C$ must be locally small! Luckily Sean Moss was able to point out the implicit hypothesis.

(Side note: Lawvere says “complete” where today we’d say “complete and cocomplete”. I think it’s true that a (locally small!) topos is complete iff it is cocomplete (right?) but Lawvere doesn’t prove anything along these lines.)

Posted by: Tim Campion on January 13, 2014 4:58 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Indeed, it is true that an elementary topos $\mathcal{E}$ with limits of shape $\mathcal{J}$ also has colimits of shape $\mathcal{J}^\mathrm{op}$ and vice versa. This is because of Paré’s theorem: the power object functor $\mathcal{E}^\mathrm{op} \to \mathcal{E}$ is monadic.

Posted by: Zhen Lin on January 13, 2014 8:24 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

If the power object functor is monadic, then it creates limits. So a limit in $\mathcal{C}$ can be created from a limit in $\mathcal{C}^{\mathrm{op}}$ , so cocompleteness implies completeness. But I’m not sure about the converse: how does completeness imply cocompleteness?

Posted by: Tim Campion on January 13, 2014 2:33 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

We have a monadic functor $\mathcal{E}^\mathrm{op} \to \mathcal{E}$ , thus, limits in $\mathcal{E}^\mathrm{op}$ are created in $\mathcal{E}$ , i.e. colimits in $\mathcal{E}$ can be constructed using limits in $\mathcal{E}$ .

My claim about the other direction is not quite correct; but it is true that a cocomplete locally small elementary topos is automatically complete as well.

Posted by: Zhen Lin on January 13, 2014 3:03 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Tim, I think you got it backwards: the monadic functor $P: E^{op} \to E$ creates (or reflects if you prefer) limits, so limits in $E^{op}$ are created from limits in $E$ . Thus completeness of $E$ with respect to some class of diagrams implies cocompleteness for the same class in $E$ .

For the other direction (external cocompleteness implies external completeness), it’s enough to construct external products from external coproducts, since we already have equalizers in a topos. If $A_i$ is an $I$ -indexed collection of objects, we can construct the evident arrow

$\sum_{i \in I} A_i \to \sum_{i \in I} 1$

in $E$ using coproducts, and then the product can be constructed as the object of sections.

Posted by: Todd Trimble on January 13, 2014 3:07 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Ah! It’s gratifying that you both caught my mistake so fast. Thanks.

And this “object of sections” constructions sounds eminently plausible. Thanks again!

Posted by: Tim Campion on January 13, 2014 3:18 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Sorry, I misspoke. The powerset functor $\mathcal{C}^{\mathrm{op}} \to \mathcal{C}$ creates limits, so a limit in $\mathcal{C}^{\mathrm{op}}$ can be created as a limit in $\mathcal{C}$ . So completeness implies cocompleteness.

It’s the “cocompleteness implies completeness” direction that puzzles me. If we had a suitable generating set, then we could conclude that the $\mathcal{C}$ is locally presentable (i.e. a Grothendieck topos) or perhaps total, and hence complete. I don’t suppose this works, even though I don’t know an example of a (co)complete topos which is not Grothendieck.

Posted by: Tim Campion on January 13, 2014 3:13 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

One of the canonical examples of elementary toposes that are complete/cocomplete but not Grothendieck toposes is $[G, Set]$ for $G$ a non-small group. Note that this one is even locally small and admits a geometric morphism to $Set$ !

Posted by: Zhen Lin on January 13, 2014 4:57 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Thanks for the example. It’s so straightforward, I wish I had thought of it!

Posted by: Tim Campion on January 13, 2014 10:30 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Another first-order / second-order issue that came up has to do with just how “discrete” the ETCS sets really are. During seminar, someone (I forget who) suggested that what the axioms were driving at was the statement:

(*) Every object $X$ is a coproduct $X = \amalg_{s:1 \to X} 1$

It seems like (*) would subsume such theorems as “every subset has a complement” or “1 is a generator”, and it would be nice if the ETCS axioms implied (*). Alas, (*) seems essentially a second-order property, dependent on the ambient set theory. For (*) implies that every function $\mathcal{C}(1,X) \to \mathcal{C}(1,Y)$ is representable as postcomposition by an arrow $X \to Y$ . But if $\mathcal{C}$ is a countable model, then we know that not every function $\mathcal{C}(1, N) \to \mathcal{C}(1, N)$ , where $N$ is the natural number object, can be so represented. The reason is that there are uncountably many such functions, but only countably many arrows $N \to N$ .

I wonder how much completeness is required to show that (*) holds. Is it enough to require that subobject lattices are complete?

Posted by: Tim Campion on January 13, 2014 6:56 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

Your statement (*) is somewhat unreasonable because it confuses internal and external sets. It can only be true if your model is equivalent to a full subcategory of $Set$ that is closed under finite limits and powersets, e.g. the category of sets of cardinality $\lt \beth_\lambda$ , where $\lambda$ is any limit ordinal, or alternatively the category of sets of rank $\lt \lambda$ , where $\lambda$ is any limit ordinal $\gt \omega$ .

As it turns out, every elementary topos $\mathcal{E}$ is cocomplete with respect to itself, i.e. every internal diagram in $\mathcal{E}$ has a colimit. And from the internal point of view, every object in $\mathcal{E}$ is indeed a coproduct of copies of $1$ – but this is a bit of a tautology.

Posted by: Zhen Lin on January 13, 2014 9:37 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

On the subject of internal (co)limits: Lawvere does construct (Thm 4 & Rmk 4, pp. 22-3), from an arrow $I \overset{\alpha}{\to} 2^X$ , something he calls $\sum_\alpha$ , which I assume is the internal coproduct. But he doesn’t prove any universal property. Also, it seems “uncategorical” to me that the sets we’re taking the coproduct of must first be amalgamated into a single set $X$ . Is this really the standard way of doing things internally?

Lawvere also indicates an internal product construction $\prod_{\alpha}$ derived from $\sum_{\alpha}$ in exactly the way Todd indicated above for external products and coproducts. It’s interesting to see this construction appearing in both internal and external contexts.

Posted by: Tim Campion on January 13, 2014 10:27 PM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

The accepted definition is a little subtle. The main point is this: a family of objects over

I

is just a morphism with codomain

I

, and their internal coproduct is the domain of such a morphism. We have an adjunction

\Sigma_I \dashv I^* : \mathcal{E} \to \mathcal{E}_{/ I}

and

I^*

has a further right adjoint

\Pi_I

, which computes the internal product. In the case

\mathcal{E} = Set

, this agrees with the classical definitions.

Posted by: Zhen Lin on January 14, 2014 8:06 AM | Permalink | Reply to this

Re: An elementary theory of the category of sets

$MathML-enabled post (click for more details).$

It’s admittedly a little unsatisfying that the topos-theoretic definition of “family of sets” essentially already includes the coproduct of that family as data, so that “taking the coproduct” appears to be just a “forgetful” operation rather than one which actually does something. There are at least two ways to respond to this, depending on what you take the definition of “family of sets” (the thing of which you take the coproduct) to be in ordinary membership-based (“material”) set theory (like ZFC).

On the one hand, you might define an $I$ -indexed family of sets to be a function with domain $I$ whose values are sets, i.e. a set $F$ of ordered pairs which contains exactly one of the form $(i,x)$ for each $i\in I$ and for which each $x$ is a set. In this case, note that the sets $x$ (which we are taking the coproduct of) are elements of the transitive closure of $F$ : if we define ordered pairs in the Kuratowski way as $(a,b) = \{\{a\},\{a,b\}\}$ , then we have $x \in \{i,x\} \in (i,x) \in F$ . Therefore, they are also really all already collected together inside the object $F$ : taking their coproduct is just “rearranging” them, so the topos-theoretic situation is not really any different. (A ZFC-style set is really a tremendously complicated mathematical object, since to determine its structure requires not just a collection of elements, but their elements and their elements and so on, together with the intricate $\in$ relationships between all of these elements. This becomes evident when you try to construct a model of ZFC out of a model of ETCS.)

On the other hand, you might define an $I$ -indexed family of sets to be a class function with domain $I$ whose values are sets, i.e. a logical formula $\phi$ such that for each $i\in I$ there exists a unique set $x$ such that $\phi(i,x)$ holds. In this case, to construct the coproduct one must first apply the replacement axiom of ZFC (or something like it) to get into the situation of the previous paragraph. So one might argue that what is missing from ETCS to make coproducts contentful is a “replacement axiom”. (In highfalutin’ language, we need to compare the “self-indexing” of the topos of sets with its “naive indexing”.) There have been a lot of such axioms proposed by different people, but the one which is most obviously related to coproducts (and indexings) is McLarty’s: given a set $I$ and a formula $\phi$ such that for each ETCS-element $i:1\to I$ there exists a set $X$ , unique up to (non-unique) isomorphism, such that $\phi(i,X)$ , then there exists a map $Y\to X$ such that for each $i$ we have $\phi(i,i^\ast(Y))$ . (If you’re bothered by “unique up to (non-unique) isomorphism”, that’s good — it turns out to be okay here because ETCS has the axiom of choice, but absent AC one needs a fancier sort of axiom, such as the ones studied here.)

Posted by: Mike Shulman on January 14, 2014 5:21 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Emily, will you be putting up a list of the Kan seminar participants? It would somehow be nice to have it.

Posted by: Tom Leinster on January 14, 2014 1:45 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

I’ve added their names to the seminar webpage.

Posted by: Emily Riehl on January 17, 2014 5:13 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Great! I recognize a good percentage of those names from the nForum and MathOverflow, and looking forward to hearing from them!

Posted by: Todd Trimble on January 17, 2014 6:27 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Great article, Clive! It gets right to the point. If this is representative, I bet these Kan Extension posts will really liven up the n-Café.

Here’s my question: can we in some sense ‘classify’ categories $C$ that obey the ETCS axioms? In other words: can we classify well-pointed topoi with natural numbers object satisfying the axiom of choice?

I’m willing to use ‘standard’ set theory, say ZFC, to describe such categories $C$ . Then apparently we get just one example that’s locally small and complete: $Set$ .

Tim Campion wrote:

There are two clauses in the statement that depend on the ambient set theory: “locally small” and “complete,” and you need both of them to nail down which category $\mathbf{Set}$ your model $C$ is equivalent to. Suppose that $C$ is equivalent to a $\mathbf{Set}(U)$ for some universe $U$ . If we pass to a larger universe, then $C$ is no longer complete. If we pass to a smaller universe, then $C$ is no longer locally small.

So I guess one question is: do these statements have converses of some sort, which allow us to ‘classify’ $C$ that are either locally small but not complete, or complete but not locally small?

What if $C$ is neither complete nor locally small? Can that happen?

(I am happy to use the word ‘classify’ in a very generous sense here; for example we might get examples of $C$ depending on a choice of inaccessible cardinal, or some such mysterious entity.)

Posted by: John Baez on January 15, 2014 12:38 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Surely, given any model of BZC (Bounded Zermelo set theory with Choice) in an ambient ZFC we get a model of ETCS?

Posted by: David Roberts on January 15, 2014 1:38 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

I don’t know what ‘bounded Zermelo set theory’ is, so I certainly can’t answer that (rhetorical?) question.

I suppose an acceptable answer to my question would be naming some kind of ‘traditional’ set theory axioms, like the ‘blah-di-blah Zermelo blah-di-blah axioms’, and saying the category of models of ETCS is equivalent to the category of models of those. But then I’d need to learn about those!

Posted by: John Baez on January 15, 2014 5:34 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Bounded Zermelo with choice (BZC), or to give it a slightly more descriptive name, ‘Zermelo with bounded comprehension and choice’, is a fragment of ZFC that’s equal in strength to ETCS. I forget exactly what bounded comprehension is, but I’m sure someone like David can explain. (This is also in Mac Lane and Moerdijk’s topos theory book, should you be feeling fabulously energetic.)

From any model of BZC, one can very easily build a model of ETCS: simply take the category of sets in your model. From any model of ETCS, one can with some effort build a model of BZC. (The ‘sets’ in this model are trees of a certain kind.) The two processes aren’t quite mutually inverse, though. Maybe they’re inverse one way round but not the other; I’m fuzzy on the details.

Here’s a paragraph from page 7 of my paper Rethinking set theory summarizing the situation:

The relationship between our axioms [ETCS] and ZFC is well understood. The ten axioms [ETCS again] are weaker than ZFC; but when the eleventh [replacement] is added, the two theories have equal strength and are ‘bi-interpretable’ (the same theorems hold). Moreover, it is known to which fragment of ZFC the ten axioms correspond: ‘Zermelo with bounded comprehension and choice’. The details of this relationship were mostly worked out in the early 1970s [2, 14, 15]. Good modern accounts are in Section VI.10 of [7] and Chapter 22 of [9].

Although that paper wasn’t the place for going into details, one fact in the background is that the relationship between

(ETCS + comprehension) and ZFC

is tighter than the relationship between

ETCS and BZC.

In both cases, each member of the pair has the same proof-theoretic strength as the other, i.e. if a model for one exists then so does a model for the other. But in the former case only, we have bi-interpretability, i.e. there’s a perfect dictionary between the theorems in one and the theorems in the other.

Posted by: Tom Leinster on January 15, 2014 1:36 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Bounded comprehension (also known as restricted comprehension) is comprehension for bounded formulas:

(1)

\exists v. \forall x. x \in v \leftrightarrow x \in a \wedge \phi(x)

for bounded formulas $\phi$ . A bounded formula (or restricted formula, or $\Delta_0$ -formula) is one in which all quantifiers are bounded ( $\exists x\in a\ldots$ or $\forall x\in a\ldots$ ).

If we think of sets as something we create (rather than the universe of sets existing preformed independently of us), then one of the prime ways we create sets is via comprehension. In bounded comprehension we only refer to previously defined sets, so you should think of it as a predicativity condition.

It’s the kind of comprehension used in Myhill’s and Aczel’s constructive set theories (CST, CZF) for the same reason. It also occurs in Kripke-Platek set theory (KP).

Posted by: Ulrik Buchholtz on January 15, 2014 5:26 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Maybe they’re inverse one way round but not the other; I’m fuzzy on the details.

That’s right: the composite ETCS $\to$ BZC $\to$ ETCS is the identity, but not BZC $\to$ ETCS $\to$ BZC. However, this is an idiosyncracy of the particular axioms chosen to comprise ETCS and BZC. The procedure of comparing well-pointed categories to set theories applies much more generally, and in general neither composite is necessarily the identity.

If you start from a well-pointed category $E$ , construct a set theory $Tree(E)$ out of well-founded trees, and then consider the category $Set(Tree(E))$ of such sets, you get the subcategory of $E$ consisting of those objects that can be embedded into a well-founded tree. Thus, if every object can be so embedded, then the composite this way around is the identity. In particular, this applies to ETCS, since it includes the axiom of choice, which implies the well-ordering principle, and a well-ordering is in particular a well-founded tree.

If you start from a model $V$ of a set theory, construct its category $Set(V)$ of sets, and then consider the structure $Tree(Set(V))$ of well-founded trees therein, what you get is not in general either a substructure or a superstructure of $V$ . However, if $V$ satisfies the axiom of foundation (which BZC includes) and transitive closures exist (which are not, as far as I know, constructible in BZC), then every object of $V$ embeds in a well-founded tree (its transitive closure), so $V$ is a submodel of $Tree(Set(V))$ . And if $V$ also satisfies Mostowski’s collapsing lemma, then $V\cong Tree(Set(V))$ . Since transitive closures and Mostowski’s lemma are both provable from replacement, if we add replacement to BZC (obtaining ZFC) and ETCS (I think this is the eleventh axiom you meant, not comprehension), we get the equivalence you mentioned.

Posted by: Mike Shulman on January 16, 2014 12:21 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Mike wrote:

replacement […] I think this is the eleventh axiom you meant, not comprehension

Right. Thanks for catching that. I’ll go back and fix my comment, so as not to cause confusion.

Posted by: Tom Leinster on January 16, 2014 1:06 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

The other commenters have supplied some technical details, but I didn’t give any motivation, so here goes. As mentioned above, BZC is essentially ZFC but where instead of saying ‘given such a formula, I can make a set (out of thin air) whose elements satisfy that formula’, I can only say ‘Given a set and a formula dealing with elements of that set, I can form a subset whose elements satisfy that formula’.

I had a vague thought that just as a (strongly) inaccessible cardinal $\lambda$ (or rather $V_\lambda$ ) gives a model of ZFC, one can use a cardinal of lesser consistency strength to get a model of BZC (I was thinking weakly inaccessible, but that doesn’t seem right). However, we do have that the set $V_{\omega+\omega}$ is a model of Zermelo set theory, which is probably the “same as” BZC, but I’m not 100% sure. Since $V_{\omega+\omega}$ exists in vanilla ZFC with no further axioms (such as “ $\exists$ an inaccessible cardinal”), if my supposition is correct there should be lots of models of ETCS inside an ambient ZFC universe, small with respect to that universe, but only cocomplete wrt themselves.

However, if you mean for the models of ETCS to be cocomplete wrt the ambient ZFC, I have no idea :-)

Posted by: David Roberts on January 15, 2014 11:41 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Lawvere does say (Rmk 10, p. 34 of TAC edition) that a model of ETCS is given by “the set of all mappings between sets of rank less than $\omega + \omega$ ”. I don’t actually know what “rank” means here, but I guess it probably means the same as $V_{\omega+\omega}$ ?

Posted by: Tim Campion on January 15, 2014 11:59 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Tim - exactly right! So even in an ambient ZFC, there are many small categories that are models of ETCS as a first-order theory, even if not equivalent to the category of sets from the ZFC universe (as the small category is clearly not cocomplete wrt arbitrary diagrams taken from said universe).

(For reference: for an ordinal $\lambda$ , ‘rank $\lambda$ ’ means that the set is an element of $V_\lambda = P^\lambda(\empty)$ , the $\lambda$ -iterated powerset. This needs the full strength of ZFC to construct through limit stages, ETCS can’t build it in general.)

Posted by: David Roberts on January 16, 2014 4:46 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

David (and Tim),

for an ordinal $\lambda$ , ‘rank $\lambda$ ’ means that the set is an element of $V_{\lambda}=\mathcal{P}^{\lambda}(\varnothing)$ , the $\lambda$ -iterated powerset.

Well, add 1 and take the least such! A set $x$ has rank $\alpha$ just if $\alpha$ is the least ordinal such that $x \in V_{\alpha + 1}$ (equivalently, $x \subseteq V_{\alpha}$ ). E.g., the rank of $\varnothing$ is 0. (On the above defn, the rank of $\varnothing$ would be 1.)

The $V_{\alpha}$ s are defined by transfinite recursion over the ordinals, with $V_0 = \varnothing$ , $V_{\alpha +1} = \mathcal{P}(V_{\alpha})$ , and $V_{\lambda} = \bigcup_{\alpha < \lambda}V_{\alpha}$ , if $\lambda$ is a limit ordinal. Then $V = \bigcup_{\alpha \in On}V_{\alpha}$ .

$V_{\omega}$ is the first infinite stage - it contains all the hereditarily finite sets, (i.e., all finite mathematical objects) - and is a model of Z with the axiom of infinity removed. $V_{\omega}$ is more or less interdefinable with $(N,0,s,+,\times)$ , the natural numbers. And $V_{\omega+\omega}$ is the least $V_{\alpha} \models Z$ , the smallest “sensible” model of Z.

Jeff

Posted by: jeffrey Ketland on January 16, 2014 5:57 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Well, add 1 and take the least such!

Thanks for the correction, jeffrey! I should have said ‘least such’ at the very least, even if I was out by 1.

Posted by: David Roberts on January 16, 2014 11:05 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

That’s right: BZC is a (proper) subsystem of Z, so $V_{\omega + \omega}$ is a model of BZC, hence, gives rise to a model of ETCS. More generally, for any limit ordinal $\lambda \gt \omega$ , $V_\lambda$ is a model of Z; thus every set (in ZFC) is a member of a “weak universe”.

Posted by: Zhen Lin on January 16, 2014 8:31 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

BZC is a (proper) subsystem of Z,…

Maybe “… subsystem of ZC”, right?

Jeff

Posted by: Jeffrey Ketland on January 16, 2014 1:01 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

I suppose that depends on whether Z is supposed to have choice or not. The Wikipedia article cited by David says yes.

Posted by: Zhen Lin on January 16, 2014 3:55 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Right, but Z is usually understood to be without choice, and ZF without choice too. Then ZC and ZFC have choice. I guess the reason for the shift is historical. Zermelo’s original 1904 uses Choice to prove that $\mathbb{R}$ has a well order, but people didn’t like it, as it’s non-constructive. So, his 1908 paper giving axioms for set theory was in a sense all about choice – Zermelo’s original version definitely had choice, yes. But then in the 20s people got interested in models of Z where choice fails; Fraenkel used a permutation model for a version of set theory with urelements (“atoms”).

Jeff

Posted by: Jeffrey Ketland on January 16, 2014 4:52 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

According to Wikipedia and Maclane-Moerdijk, Zermelo set theory does not include the axiom of foundation whereas BZC does. If that’s true, then BZC isn’t technically a subsystem of ZC, although it’s equiconsistent with one since foundation doesn’t add any consistency strength (essentially since $Tree(Set(V))$ always satisfies it), and all the “natural” models $V_\alpha$ of ZC do satisfy foundation.

Posted by: Mike Shulman on January 16, 2014 7:19 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Mike, the wikipedia article on ZFC does include foundation. Normally, foundation is included in standard monographs but sometimes not. Jech’s standard monograph, for example includes foundation (aka, regularity) in ZF. Similarly with his SEP article on set theory. (My copy of Kunen is at work.) It’s standard, though, that Z and ZF don’t have choice.

Yes, foundation doesn’t change consistency strength. Aczel’s AFA is equiconsistent with ZFC.

Jeff

Posted by: Jeffrey Ketland on January 16, 2014 7:45 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

What I said was that Zermelo set theory does not include the axiom of foundation. Of course ZFC does include it.

Posted by: Mike Shulman on January 17, 2014 12:10 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Right, but the theory usually called Z has foundation (e.g., e.g., e.g., e.g.,…) No doubt it varies a bit though - one can always check with the author’s convention on what they mean by Z - it’s easily stated. The wikipedia article is about Zermelo’s own 1908 formulation.

Jeff

Posted by: Jeffrey Ketland on January 17, 2014 1:14 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Thanks for all the helpful answers and discussion!

Posted by: John Baez on January 28, 2014 10:18 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

If the NNO axiom is removed from ETCS, is the theory equivalent to Z with infinity removed?

(Z with infinity removed is very closely related to PA.)

Jeff

Posted by: Jeffrey Ketland on January 15, 2014 9:41 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Thanks for this very interesting discussion and the idea to conduct this seminar in public.

If I may, I would like to make some possibly vague remarks about strengthenings of ETCS and how they (could) relate to strengthenings of ZFC. (I apologize if this is an abuse of the format of this seminar, which, from what I understand, is more focused on a close reading of the papers rather than speculation on them.)

Adding an inaccessible cardinal (or, equivalently, a Grothendieck universe $U$ ) to ZFC is the same (i.e. from a model of one you can build a model of the other where these models, I suppose, are constructed in the cumulative hierarchy [see my SIDE REMARK below]) as ETCS+R+U, where we can think of a model of ETCS+R+U as a topos $\mathcal{S}$ (our ambient'' set theory) satisfying all the axioms of ETCS+R with the added stipulation that it contains an internal category <math xmlns='http://www.w3.org/1998/Math/MathML' display='inline'><semantics><mrow><mi>&Cscr;</mi></mrow>\mathcal{C}</semantics></math> that satisfies the axioms of ETCS+R, i.e. a ''topos with a universe''. This is basically the setting in which Lawvere proves his metatheorem (as some of the threads above have clarified.) Indeed, unless I'm missing something, in reasoning about <math xmlns='http://www.w3.org/1998/Math/MathML' display='inline'><semantics><mrow><mi>&Cscr;</mi></mrow>\mathcal{C}</semantics></math> in <math xmlns='http://www.w3.org/1998/Math/MathML' display='inline'><semantics><mrow><mi>&Sscr;</mi></mrow>\mathcal{S}</semantics></math> (i.e. using the usual internal language of <math xmlns='http://www.w3.org/1998/Math/MathML' display='inline'><semantics><mrow><mi>&Sscr;</mi></mrow>\mathcal{S}</semantics></math>) then <math xmlns='http://www.w3.org/1998/Math/MathML' display='inline'><semantics><mrow><mi>S</mi><mo>&Element;</mo><mi>U</mi></mrow>S \in U</semantics></math> will express what we usually refer to as $S$ is small” and $\forall A \forall B \mathcal{C}(A,B) \in U$ ” that $\mathcal{C}$ is locally small, and so on.

Interestingly, of course, an internal category such as $\mathcal{C}$ can be thought of in many equivalent ways, e.g. as a fibration over $\mathcal{S}$ , or an $\mathcal{S}$ -indexed category. Some of these viewpoints will come with questions that are not native to set-theory (as does, of course, ETCS itself) and that is probably interesting in itself to some degree.

Now I suppose that it makes sense in this new setting to ask whether one can prove similar metatheorems as Lawvere proves in the case of ETCS. Would these be what one would expect? E.g. Any $\mathcal{S}$ -complete, $\mathcal{S}$ -locally small fibration that is a model of ETCS+R+U will be $\mathcal{S}$ -equivalent to the fibration $\mathcal{C} \rightarrow \mathcal{S}$ . What about stronger axioms of infinity? Do these also have natural formulations from a fibrational/internal/indexed point of view? Would one also be able to prove Lawvere-type metatheorems for such even stronger set theories? I’m guessing it all would follow quite naturally in the case of, say, adding more and more Grothendieck universes, if one takes into account that adding more and more Grothendieck universes is like adding more and more internal categories (with respect to Mike Shulman’s comment I’m not sure what this approach is close in spirit to, set theory or type theory, but it seems to combine elements of both.) But what about the stranger large cardinals that axiomatic set theory has studied, e.g. measurable cardinals?

Finally, a bit of science fiction: I wonder if this is another direction in which strengthenings of ETCS can be used to shed light on one of the founding problems of axiomatic set theory, namely Godel’s famous hope that some strong enough axiom of infinity A would be able to settle the Continuum Hypothesis, in the sense that $ZFC+A \vdash CH$ . The approach of adding stronger and stronger such axioms has not, so far, borne fruit, although nothing has been settled yet. Perhaps a categorical viewpoint on set theory may suggest other ways of strengthening set theory other than by adding ever larger cardinals (=longer and more complicated well-founded relations). Perhaps some of the things one can do with (Grothendieck) fibrations and properties that one naturally attaches to them will correspond to different ways of strengthening ZFC some of which may turn out to be relevant to Godel’s problem?

[SIDE REMARK: It would be nice to be able to use a categorical meta-theoretic analogue to the cumulative hierarchy to state this e.g. some theory of 2- or higher-categories. I suppose this really ought to be done if we are to think of structural and extensional set theory as two sides of the same coin, because right now what we mean when we say ”ETCS+R is the same as ZFC” is more like ”ETCS+R is the same as ZFC modulo a (extensional) set-theoretic metatheory”. That said, consistency strength of theories does not require such vertigo-inducing machinery as the cumulative hierarchy and in fact equiconsistency of theories can be proven in very basic fragments of arithmetic. I’m not sure whether the equiconsistency of ETCS+R with ZFC (i.e. the statement Con(ETCS+R) $\leftrightarrow$ Con(ZFC)) is such a statement, but I strongly suspect it is. Does anyone know? Is this well-known? In that sense, it would then probably be pointless to ask whether the basic fragment of arithmetic needed to prove this equiconsistency is ”categorical” or ”set-theoretic” in spirit, and so we would get a neutral perspective from which to assert the theoretical equivalence between, say, structural set theory in the sense of ETCS+R and extensional set theory in the sense of ZFC.]

Posted by: DT on January 16, 2014 6:14 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

…equiconsistency of theories can be proven in very basic fragments of arithmetic. I’m not sure whether the equiconsistency of ETCS+R with ZFC … is such a statement, but I strongly suspect it is.

Yes, I believe it is. I’m not an expert in very basic fragments of arithmetic, but I believe all that is needed is an ambient first-order logic. The equiconsistency is proven by “constructing a model” of each out of a model of the other, but an alternative viewpoint on that is that it translates a statement in the first-order language of each into a statement in the first-order language of the other, preserving theoremhood.

Posted by: Mike Shulman on January 17, 2014 12:10 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

I’m not an expert in very basic fragments of arithmetic […]

Haha, not sure whether or not this is tongue-in-cheek! Anyway, I misspoke, I should have said something more along the lines of “basic first-order theories, some of which can be seen to be extensions or fragments of (possibly higher-order) arithmetic.” But in any case something much more basic and “finitary” than ZFC.

The point I was driving at here, however, is that the standard way in which the above equiconsistency results are proven (e.g. in Moerdijk-Maclane) is that models are constructed in some ambient set-theory in the traditional way, rather than, say, as functors into Set. These two viewpoints of models-as-sets and models-as-functors are of course themselves equivalent, but modulo what? The problem reappears. Perhaps a more conceptually robust theoretical equivalence (of ETCS+R and ZFC) would consist in proving the same eqiconsistency results using a fixed categorical meta-theory, i.e. using a conception of a “model” that is not set-theoretic in character.

But is there such a thing? Probably not. At the end of the day it seems that we cannot really get away from the fact that a variable $x$ in FOL is more naturally treated as an element of some set rather than as a generalized element in a category. Nevertheless, from a purely deductive/formalistic perspective these two approaches to set theory (ETCS+R and ZFC) are indeed indistinguishable. Because, as you point out, the equiconsistency results can merely be read as suitable translations of sentences in one language to the other language, irrespective of the semantics being used.

That said, I don’t really understand what you mean by

[…] I believe all that is needed is an ambient first-order logic

What will be needed will be at least some first-order arithmetic in which we can manipulate the Godel numbers of the consistency sentences of each of ETCS+R and ZFC and therefore express the sentence Con(ETCS+R) $\leftrightarrow$ Con(ZFC). The type of result referred to above, namely “Given a model of $T_1$ I can build a model of $T_2$ ” translates to “Given that $T_1$ is consistent I can show that $T_2$ is consistent” and that last formulation would minimally depend on some arithmetic to prove.

Posted by: DT on January 17, 2014 11:28 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Mike and DT, the crucial thing (like Mike says) is that there are interpretation functions $f,g$ such that:

(i) If $ETCS+R \vdash \phi$ then $ZFC \vdash f(\phi)$

(ii) If $ZFC \vdash \phi$ then $ETCS + R \vdash g(\phi)$

Informally, one can algorithmically convert a proof $(\phi_0, \dots, \bot)$ of inconsistency in $ETCS+R$ to a proof $(f(\phi_0), \dots, \bot)$ of inconsistency in $ZFC$ , and vice versa. So, I think what DT suggests is right. Here’s a more detailed guess about showing this, using two things, both of which I think are true. First, that these functions are primitive recursive on godel codes (btw, I don’t know the details of $f$ and $g$ ). And second, having defined $f,g$ in $L_{PA}$ , that the required proofs of (i) and (ii) should go through using $\Sigma_1$ -induction. I’m not sure this is right. But it seems very likely of one looks at the details. I.e., (i) and (ii) are theorems of $I \Sigma_1$ :

$I \Sigma_1 \vdash \forall n(\square_{ETCS+R}(n) \to \square_{ZFC}(f(n)))$

$I \Sigma_1 \vdash \forall n(\square_{ZFC}(n) \to \square_{ETCS + R}(f(n)))$

where $\square_{ETCS+R}(n)$ means “the formula whose godel code is $n$ is provable in $ETCS+R$ ”. Then, assuming these two things, we’d get,

$I \Sigma_1 \vdash Con(ZFC) \leftrightarrow Con(ETCS + R)$

as follows: $I \Sigma_1 \vdash \square_{ETCS+R}(\bot) \to \square_{ZFC}(f(\bot)))$ . So, $I \Sigma_1 \vdash \square_{ETCS+R}(\bot) \to \square_{ZFC}(\bot))$ . So, $I \Sigma_1 \vdash \neg \square_{ZFC}(\bot) \to \neg \square_{ETCS + R}(\bot))$ . So, $I \Sigma_1 \vdash Con(ZFC) \to Con(ETCS + R)$ . And similarly for the other direction.

Jeff

Posted by: Jeffrey Ketland on January 18, 2014 12:34 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

Yes, that’s the sort of thing I meant.

Posted by: Mike Shulman on January 18, 2014 5:30 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

I think this must be covered in Metamathematics of First-Order Arithmetic by Hájek and Pudlák

Posted by: Kevin Watkins on January 22, 2014 2:34 AM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

I’m not an expert in very basic fragments of arithmetic […]

That said, I don’t really understand what you mean by

[…] I believe all that is needed is an ambient first-order logic

Posted by: DT on January 17, 2014 11:28 PM | Permalink | Reply to this

Re: An Elementary Theory of the Category of Sets

$MathML-enabled post (click for more details).$

There’s no apology needed! Close reading is only one of many ways to engage with the papers; in any case, speculations are encouraged. I’m glad to see that there are a lot of people who are enthusiastic about a wide-ranging discussion.

Posted by: Emily Riehl on January 17, 2014 5:15 PM | Permalink | Reply to this

Read the post An Exegesis of Yoneda Structures
Weblog: The n-Category Café
Excerpt: Motivates the notion of Yoneda structure as an expression of basic notions of category theory in a natural 2-categorical language.
Tracked: March 24, 2014 5:37 AM

The n-Category Café

Skip to the Main Content

January 12, 2014