Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

January 12, 2014

An Elementary Theory of the Category of Sets

Posted by Emily Riehl

Guest post by Clive Newstead

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!

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 AA in a category with a terminal object 11, if a:1Aa \colon 1 \to A then we write aAa \in A and say aa is an element of AA. If s:SAs \colon S \to A is monic then we say ss is a subset of AA, and write sAs \subseteq A. We then write asa \in s if aa factors through ss.

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

  1. 𝒞\mathcal{C} has an initial object 00, a terminal object 11, products A×BA \times B and coproducts A+BA+B of all pairs A,BA,B, and equalisers and coequalisers of all pairs f,g:ABf,g : A \rightrightarrows B. (Thus 𝒞\mathcal{C} has all finite limits and colimits.)
  2. Every pair of objects A,BA,B has an exponential B AB^A.
  3. 𝒞\mathcal{C} has a natural numbers object \mathbb{N}, with zero morphism zero:1\mathtt{zero} : 1 \to \mathbb{N} and successor morphism suc:\mathtt{suc} : \mathbb{N} \to \mathbb{N}.
  4. 𝒞\mathcal{C} is well-pointed, i.e. given any pair of maps f,g:ABf,g : A \rightrightarrows B with fgf \ne g, there is an element aAa \in A such that fagaf \circ a \ne g \circ a.
  5. Axiom of Choice: If f:ABf : A \to B and there is some aAa \in A, then there exists a quasi-inverse g:BAg : B \to A, which satisfies fgf=ff \circ g \circ f = f.
  6. If AA has no elements then AA is an initial object.
  7. If aA+Ba \in A + B then aa factors through one of the coproduct inclusions.
  8. 𝒞\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 Pos\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:AB,u:×A×BBf_0 : A \to B, \quad u : \mathbb{N} \times A \times B \to B there is a morphism f:×ABf : \mathbb{N} \times A \to B satisfying, for each nn \in \mathbb{N} and aAa \in A, fzero,a=f 0a,fsucn,a=un,a,fn,af \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 ff is implied by axiom 4. Thus primitive recursion can be done in categories such as the functor category [,Set][\mathbb{C}, \mathbf{Set}] for any small category \mathbb{C}, and in the arrow category Set \mathbf{Set}^{{\rightarrow}}.

Theorem 2 (Peano’s postulates).

  • The morphism succ:\mathtt{succ} : \mathbb{N} \to \mathbb{N} is monic
  • If n=succmn = \mathtt{succ} \circ m for some mm \in \mathbb{N} then nzeron \ne \mathtt{zero}.
  • If ss \subseteq \mathbb{N} and nssuccnsn \in s \Rightarrow \mathtt{succ} \circ n \in s then s=id 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+12 = 1+1 and let :12\top : 1 \to 2 be one of the inclusion maps. Given any α:I2 A\alpha : I \to 2^A there is a subset u: αAu : {\bigcup_{\alpha}} \to A such that, for all aAa \in A, aua \in u if and only if ev 2 Aαj,a=\mathtt{ev}_{2^A} \circ \langle \alpha \circ j, a \rangle = \top for some jIj \in I.

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

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

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

Intuitively, QQ is the quotient of AA by RR, then the theorem is stating that RR is precisely the set of pairs a,bA×A\langle a,b \rangle \in A \times A such that [a] R=[b] RQ[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 Set\mathbf{Set}.

The equivalence 𝒞TˇTSet\mathcal{C} \overset{T}{\underset{\check T}{\rightleftarrows}} \mathbf{Set} is given by TA=Hom Set(1,A)={elements of A}TA = \text{Hom}_{\mathbf{Set}}(1,A) = \{ \text{elements of } A \} TˇX= xX1\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:   http://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

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 nn-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:ABf \colon A \to B, takes SAS \subset A to

f !(S):={bBsS,f(s)=b}. 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:ABf \colon A \to B, should take SAS \subset A to

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

With some work I’m sure this map 2 A2 B2^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_!, f f^* (meaning precomposition), and f f_* should be adjoints.'' Interpretingadjoint” with respect to the posets of subobjects of AA and BB, I think this is right: we have f (T)Sf^*(T) \subset S if and only if Tf (S)T \subset f_*(S), which says that f f f^* \dashv f_*.

What I don’t see (quoting Remark 5), is how f *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

Thanks for your comment!

Another equivalent definition of f !f_! is given by f !(S)={bB:sf 1(b),sS}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 !f_!, i.e. f *(S)={bB:sf 1(b),sS}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

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

Trying to explain this to philosophers, I like to give a concrete example. For some reason I settled on AA as the set of dogs, BB the set of people, ff 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

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

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

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

and

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

whenever SS is a subset of 2 B2^B. Viewing posets as categories in the usual way, f 1f^{-1} is a functor from 2 B2^B to 2 A2^A, and this condition says exactly that f 1f^{-1} commutes with all limits and colimits. Since 2 B2^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 A2 B2^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

You meant SBS \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

I think he really did mean S2 BS \subseteq 2^B: it’s a collection of subsets of BB. 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

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

In the world of naive set theory, you may think of f !(S)f_{!}(S) as a left Kan extension Lan fSLan_f S of S:A2S\colon A \to 2 along f:ABf\colon A \to B and f *(S)f_{*}(S) as a Right Kan extension Ran fSRan_f S where one think of SS as a functor from a discrete category AA to a poset 22.

If you take BB to be a/the terminal object 11, then you may think of f !=:2 A2 12f_{!}= \exists\colon 2^A \to 2^1 \cong 2 and f *=:2 A2f_{*}=\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

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

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

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

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

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

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

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|XY|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||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 ZZ set theory, which assumes something like (L) too - i.e., “there is a set containing \varnothing and closed under xx{x}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

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

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

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

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

Xy(X(y)ϕ(y))\exists X \forall y(X(y) \leftrightarrow \phi(y))

Rx,y(R(x,y)ϕ(x,y))\exists R \forall x, y(R(x,y) \leftrightarrow \phi(x,y))

That’s all ok. Then we add on

|X|=|Y|XY|X| = |Y| \leftrightarrow X \sim Y

The resulting second-order theory FAFA interprets second-order arithmetic, PA 2PA_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

xyx \in y

x=yx = 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

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

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

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

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

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

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 00 and the rest of \mathbb{N} is generated recursively by application of successor ss. Within the category of sets in which it is embedded, it is the universal example of that data (0,s)(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 VV equipped with a successor operation s:VVs: V \to V (conceived as taking a set xx to the singleton {x}\{x\}). In this set-up, the elementhood relation xyx \in y is recovered as the relation s(x)ys(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

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

\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

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

I agree this is quite suggestive.

Apparently, an element ff of a ring is called von Neumann regular if there exists a “quasi-inverse” gg such that f=fgff = 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 Set\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

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

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

The unit η:1LR\eta:1\rightarrow LR and counit ϵ:LR1\epsilon:LR\rightarrow 1 satisfy

Lη:LLRLL\eta:L\rightarrow LRL and ϵ:LRLL\epsilon:LRL\rightarrow L

ηR:RRLR\eta R:R\rightarrow RLR and Rϵ:RLRRR\epsilon:RLR\rightarrow R

with Lη.epsilonL=1L\eta . \epsilonL=1 and ηR.Rϵ=1\eta R.R\epsilon=1

Apparently a semigroup which satisfies the conditions fgf=ffgf=f and gfg=ggfg=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

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

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

Certainly, although of course we need to keep the (with nonempty domain) caveat for monos, for if 010 \to 1 splits then 010 \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

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 Set\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

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 XX as a map X2X \to 2, but there is no canonical injection SXS \to X to which a map X2X \to 2 corresponds — it’s only canonical up to isomorphism. We could choose a representative injection SXS \to X for each X2X \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

[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}A = \{cat, dog, mouse\} and B={cat,mouse,pig}B = \{cat, mouse, pig\} then what is ABA \cup B and ABA \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 catcat etc. are sets then what are the values of catdogcat \cup dog or mousepigmouse \cap pig?

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

there is no canonical injection SXS \to X to which a map X2X \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 LabelsLabels and this is just the slice category MonoSubCat(Set)/LabelsMonoSubCat(Set)/Labels, the power set of LabelsLabels (MonoSubCat(Set)MonoSubCat(Set) is the wide subcategory of Set with morphisms being all injections). This is how subobjects in the topos SetSet are defined without mentioning the word “topos”.

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

(PS. I haven’t been able to find any discussion of MonoSubCatMonoSubCat as a particular type of forgetful functor though people tend to use it and EpiSubCatEpiSubCat 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

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 aba \subseteq b on subsets of a fixed object AA, 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 elemente l e m e n t xx of a set AA is a map 1xA1 \overset{x}{\to} A.

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

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

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 Set\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 Set\mathbf{Set} your model CC is equivalent to. Suppose that CC is equivalent to a Set(U)\mathbf{Set}(U) for some universe UU. If we pass to a larger universe, then CC is no longer complete. If we pass to a smaller universe, then CC is no longer locally small.

I found this confusing at first because in the paper, Lawvere doesn’t explicitly state that CC 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

Indeed, it is true that an elementary topos \mathcal{E} with limits of shape 𝒥\mathcal{J} also has colimits of shape 𝒥 op\mathcal{J}^\mathrm{op} and vice versa. This is because of Paré’s theorem: the power object functor op\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

If the power object functor is monadic, then it creates limits. So a limit in 𝒞\mathcal{C} can be created from a limit in 𝒞 op\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

We have a monadic functor op\mathcal{E}^\mathrm{op} \to \mathcal{E}, thus, limits in op\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

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

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 iA_i is an II-indexed collection of objects, we can construct the evident arrow

iIA i iI1\sum_{i \in I} A_i \to \sum_{i \in I} 1

in EE 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

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

Sorry, I misspoke. The powerset functor 𝒞 op𝒞\mathcal{C}^{\mathrm{op}} \to \mathcal{C} creates limits, so a limit in 𝒞 op\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

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

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

Re: An elementary theory of the category of sets

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

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 XX is a coproduct X=⨿ s:1X1X = \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 𝒞(1,X)𝒞(1,Y)\mathcal{C}(1,X) \to \mathcal{C}(1,Y) is representable as postcomposition by an arrow XYX \to Y. But if 𝒞\mathcal{C} is a countable model, then we know that not every function 𝒞(1,N)𝒞(1,N)\mathcal{C}(1, N) \to \mathcal{C}(1, N), where NN is the natural number object, can be so represented. The reason is that there are uncountably many such functions, but only countably many arrows NNN \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

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 SetSet 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 11 – 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

On the subject of internal (co)limits: Lawvere does construct (Thm 4 & Rmk 4, pp. 22-3), from an arrow Iα2 XI \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 XX. 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

The accepted definition is a little subtle. The main point is this: a family of objects over II is just a morphism with codomain II, and their internal coproduct is the domain of such a morphism. We have an adjunction Σ II *: /I\Sigma_I \dashv I^* : \mathcal{E} \to \mathcal{E}_{/ I} and I *I^* has a further right adjoint Π I\Pi_I, which computes the internal product. In the case =Set\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

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 II-indexed family of sets to be a function with domain II whose values are sets, i.e. a set FF of ordered pairs which contains exactly one of the form (i,x)(i,x) for each iIi\in I and for which each xx is a set. In this case, note that the sets xx (which we are taking the coproduct of) are elements of the transitive closure of FF: if we define ordered pairs in the Kuratowski way as (a,b)={{a},{a,b}}(a,b) = \{\{a\},\{a,b\}\}, then we have x{i,x}(i,x)Fx \in \{i,x\} \in (i,x) \in F. Therefore, they are also really all already collected together inside the object FF: 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 II-indexed family of sets to be a class function with domain II whose values are sets, i.e. a logical formula ϕ\phi such that for each iIi\in I there exists a unique set xx such that ϕ(i,x)\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 II and a formula ϕ\phi such that for each ETCS-element i:1Ii:1\to I there exists a set XX, unique up to (non-unique) isomorphism, such that ϕ(i,X)\phi(i,X), then there exists a map YXY\to X such that for each ii we have ϕ(i,i *(Y))\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

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

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

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

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 CC 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 CC. Then apparently we get just one example that’s locally small and complete: SetSet.

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 Set\mathbf{Set} your model CC is equivalent to. Suppose that CC is equivalent to a Set(U)\mathbf{Set}(U) for some universe UU. If we pass to a larger universe, then CC is no longer complete. If we pass to a smaller universe, then CC is no longer locally small.

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

What if CC 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 CC 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

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

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

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

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

(1)v.x.xvxaϕ(x) \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 Δ 0\Delta_0-formula) is one in which all quantifiers are bounded (xa\exists x\in a\ldots or xa\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

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 EE, construct a set theory Tree(E)Tree(E) out of well-founded trees, and then consider the category Set(Tree(E))Set(Tree(E)) of such sets, you get the subcategory of EE 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 VV of a set theory, construct its category Set(V)Set(V) of sets, and then consider the structure Tree(Set(V))Tree(Set(V)) of well-founded trees therein, what you get is not in general either a substructure or a superstructure of VV. However, if VV 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 VV embeds in a well-founded tree (its transitive closure), so VV is a submodel of Tree(Set(V))Tree(Set(V)). And if VV also satisfies Mostowski’s collapsing lemma, then VTree(Set(V))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

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

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 λ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 ω+ω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 ω+ω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

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 ω+ω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

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 λ=P λ()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

David (and Tim),

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

Well, add 1 and take the least such! A set xx has rank α\alpha just if α\alpha is the least ordinal such that xV α+1x \in V_{\alpha + 1} (equivalently, xV α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 αV_{\alpha}s are defined by transfinite recursion over the ordinals, with V 0=V_0 = \varnothing, V α+1=𝒫(V α)V_{\alpha +1} = \mathcal{P}(V_{\alpha}), and V λ= α<λV αV_{\lambda} = \bigcup_{\alpha &lt; \lambda}V_{\alpha}, if λ\lambda is a limit ordinal. Then V= αOnV αV = \bigcup_{\alpha \in On}V_{\alpha}.

V ω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 ωV_{\omega} is more or less interdefinable with (N,0,s,+,×)(N,0,s,+,\times), the natural numbers. And V ω+ωV_{\omega+\omega} is the least V αZV_{\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

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

That’s right: BZC is a (proper) subsystem of Z, so V ω+ω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 λ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

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

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

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

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))Tree(Set(V)) always satisfies it), and all the “natural” models V α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

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

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

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

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

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

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 UU) 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 asSS is small” and AB𝒞(A,B)U\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+ACHZFC+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

…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

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 xx 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 1T_1 I can build a model of T 2T_2” translates to “Given that T 1T_1 is consistent I can show that T 2T_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

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

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

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

Informally, one can algorithmically convert a proof (ϕ 0,,)(\phi_0, \dots, \bot) of inconsistency in ETCS+RETCS+R to a proof (f(ϕ 0),,)(f(\phi_0), \dots, \bot) of inconsistency in ZFCZFC, 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 ff and gg). And second, having defined f,gf,g in L PAL_{PA}, that the required proofs of (i) and (ii) should go through using Σ 1\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Σ 1I \Sigma_1:

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

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

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

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

as follows: IΣ 1 ETCS+R() ZFC(f()))I \Sigma_1 \vdash \square_{ETCS+R}(\bot) \to \square_{ZFC}(f(\bot))). So, IΣ 1 ETCS+R() ZFC())I \Sigma_1 \vdash \square_{ETCS+R}(\bot) \to \square_{ZFC}(\bot)). So, IΣ 1¬ ZFC()¬ ETCS+R())I \Sigma_1 \vdash \neg \square_{ZFC}(\bot) \to \neg \square_{ETCS + R}(\bot)). So, IΣ 1Con(ZFC)Con(ETCS+R)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

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

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

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 xx 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 1T_1 I can build a model of T 2T_2” translates to “Given that T 1T_1 is consistent I can show that T 2T_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

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

Post a New Comment