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.

December 18, 2012

Rethinking Set Theory

Posted by Tom Leinster

Over the last few years, I’ve been very slowly working up a short expository paper — requiring no knowledge of categories — on set theory done categorically. It’s now progressed to the stage where I’d like to get some feedback. Here’s the latest draft. (Edit: Now revised in the light of your helpful comments below — thanks! — and posted as arXiv:1212.6543.) Typos, clumsy wording, mathematical matters: I want to hear it all.

I have one request, though. If you do leave a comment, please take more time than you usually would to make sure it’s (1) carefully worded, (2) respectful to other people, and (3) scrupulously polite. Sorry to ask this: normally I wouldn’t feel the need, but there’s an unfortunate history of discussions of categorical set theory turning bad-tempered, and I really want to avoid that happening here.

So, if you’re composing a comment and you feel yourself getting hot under the collar, please save a draft, sleep on it, and come back later when your temperature has returned to normal. There’s no hurry: this blog isn’t going anywhere.

I’d also like to hear about anything I’ve written in my draft that you think is overstated. (I’m particularly keen to hear about this from people who fundamentally share my views.) This paper is intended to be thought-provoking, and I know there are parts with which some people will disagree. However, it’s definitely not supposed to be inflammatory. I want every statement I’ve made to be careful and measured, so I’ll be grateful if you can help me find places where I might have slipped up.

I won’t write much here about the paper, since it is itself expository. Experts will immediately recognize it as a description of Lawvere’s Elementary Theory of the Category of Sets, which states that sets and functions form a well-pointed topos with natural numbers and choice. (Semi-experts might want the help of this supplement: in my draft, I’ve slightly rephrased the standard axioms, but the supplement proves that the rephrasing makes no difference.)

However, it’s very much not written for experts, or even semi-experts. No knowledge of categories whatsoever is needed to read it. Nor do I attempt to teach the reader anything about categories.

What’s this paper supposed to achieve? I’ll quote from the first page:

… many of us will go our whole lives without learning ‘the’ axioms for sets, with no harm to the accuracy of our work. This suggests that we all carry around with us, more or less subconsciously, a reliable body of operating principles that we use when manipulating sets.

What if we were to write down some of these principles and adopt them as our axioms for sets? The message of this article is that this can be done, in a simple, practical way.

There are probably many ways of doing this, but the one I describe is categorical in spirit.

Relatively few mathematicians have heard of categorical set theory, but my experience is that among those who have heard of it, there are some common misconceptions. These misconceptions are largely a result of bad communication, so I’ve done my best to address them directly.

One misconception is that because of the involvement of categories (and even toposes, God forbid), categorical set theory must be awfully sophisticated. I try to dissolve that assumption by stating the axioms in a wholly elementary way, not using the word ‘category’ once. The box on the first page shows that the axioms—informally paraphrased—are just a bunch of completely mundane statements about sets:

  1. Composition of functions is associative and has identities.
  2. There is a set with exactly one element.
  3. There is a set with no elements.
  4. A function is determined by its effect on elements.
  5. Given sets XX and YY, one can form their cartesian product X×YX \times Y.
  6. Given sets XX and YY, one can form the set of functions from XX to YY.
  7. Given f:XYf\colon X \to Y and yYy \in Y, one can form the inverse image f 1(y)f^{-1}(y).
  8. The subsets of a set XX correspond to the functions from XX to {0,1}\{0, 1\}.
  9. The natural numbers form a set.
  10. Every surjection has a right inverse.

As I said, this is an informal summary, and there is some distance between the statements above and the precise versions (which you can find in the paper). However, if I’ve done my job properly, even the precise versions should come across as run-of-the-mill, unremarkable, statements about sets as used in everyday mathematics.

I also address the misconception that, because the definition of category uses something like the notion of set, categorical set theory must be circular. But I won’t go into that here, because you can find it in my draft — which I’m hoping you’re about to go and read, then carefully comment on here.

Posted at December 18, 2012 2:47 AM UTC

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

234 Comments & 3 Trackbacks

Re: Rethinking Set Theory

Good morning, Tom, you are now waking up, slowly,
you are turning on your computer, it is still
dark outside, you have new email; you are reading
in your email, your tenth axiom is inconsistent;
you are completely relaxed, yet you do not feel
like sleeping; you are now a constructivist,
everything is OK, you will make yourself a cup
of green tea; it is still dark outside…

No, I just wanted to say that while maybe not
strictly inconsistent, I think it is a pity to
build a notational idiosyncrasy (right-to-left
composition) into the axioms. Why not say
section instead of right-inverse?

It is still dark outside.

Posted by: Joachim Kock on December 18, 2012 5:33 AM | Permalink | Reply to this

Re: Rethinking Set Theory

That’s funny — I think I’d always subconsciously imagined constructivists to be the sorts to rise before the sun and drink green tea. But I see from the timestamp on your comment that you really were up in the dark. I expect you typed your comment sitting in the lotus position:

Man sitting cross-legged with laptop, doing that lotusy thing with his hands

(Novices may wonder how it is possible to type while in the lotus position. Ask a constructivist.)

In a way it’s a pity that the axiom of choice, applied to a well-pointed topos, implies that the topos is Boolean and two-valued. If it didn’t, we’d have to state those axioms separately, which would mean that removing the axiom of choice wouldn’t disembowel the whole theory in the way that it currently does.

Regarding “section” versus “right inverse”, I definitely see your point. I struggled with this one for a while. In the end, I went for “right inverse” because I think it’s more widely understood than “section”. (Would you agree? I don’t actually have any evidence.) But yes, “section” is definitely superior terminology. Apart from anything else, I usually can’t remember whether it’s a left or a right inverse that a non-injective surjection might plausibly have — it takes me a few moments to work it out. “Splits” is another possibility, though again it’s less widely understood than “right inverse”.

In general, where there’s been a choice about presentation (as in Karol’s question below), I’ve made the choice that I think will be most immediately appealing to the largest number of people.

Posted by: Tom Leinster on December 18, 2012 8:22 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Well, I hope Joachim’s “lotus” looks better than that! That dude in the picture is obviously a poser – constructivist my foot!

Posted by: Todd Trimble on December 18, 2012 9:22 PM | Permalink | Reply to this

Re: Rethinking Set Theory

You’re right: despite searching for “lotus position laptop”, all I got was some guy sitting cross-legged and doing that thing with his hands. There’s only one solution, Todd: you’ll have to upload a photo of yourself doing it properly.

Posted by: Tom Leinster on December 18, 2012 9:34 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Well, here you go Tom. It’s been a while since I’ve done sitting meditation, but this is me in a kind of half-lotus posture, looking over your axiom 7 on my screen. (Full lotus would be a bit of a stretch – literally.) I never understood how you could type with the hands held in this mudra, but then again, constructivism was never my thing. You’ll have to ask Toby, maybe.

Todd in half-lotus with laptop

Posted by: Todd Trimble on December 21, 2012 2:31 AM | Permalink | Reply to this

Re: Rethinking Set Theory

In constructivist nirvana, you don't have to type anything; the proof assistant derives everything automatically.

Posted by: Toby Bartels on December 23, 2012 11:54 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Actually, Tom, well-pointedness only implies AC if your ambient logic is classical. Mike uses a constructive notion of well-pointedness (definition 3.6 in the linked paper), which in the presence of classical logic is equivalent to the usual sense.

Posted by: David Roberts on December 18, 2012 11:12 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Did you mean to say “implies 2-valuedness” or something? Because surely AC is independent of the other axioms.

Posted by: Todd Trimble on December 18, 2012 11:52 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Duh.

I was think of some mashed-up version of Dionescu’s theorem, that AC implies excluded middle.

The actual result is that a constructively well-pointed topos in intuitionistic logic is not necessarily Boolean.

Posted by: David Roberts on December 19, 2012 12:45 AM | Permalink | Reply to this

Re: Rethinking Set Theory

> (Novices may wonder how it is possible to type while
> in the lotus position. Ask a constructivist.)

Or better, a type theorist.

> I went for “right inverse” because I think it’s more
> widely understood than “section”. (Would you agree?
> I don’t actually have any evidence.)

I have no evidence for either. But the word
“section” you can learn and never forget. The word
“right inverse” you have to relearn every time,
especially if you think it means the opposite of
what you thought it meant. (And if you get it
wrong in Axiom 10, your sets collapse to homotopy
(-1)-types.)

Posted by: Joachim Kock on December 18, 2012 11:35 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Or better, a type theorist.

:-)

Posted by: Tom Leinster on December 21, 2012 2:38 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Re “right-inverse”/”section”… I’m in the odd condition of being confused by the former not because I usually write composites in the same order as I draw arrows (I don’t; and I rather like them being reverse of eachother, actually… ) but because I can never remember whether the factor written on the right in id X=lrid_X = l\circ r is a right-inverse or has a right-inverse.

Posted by: Jesse C. McKeown on December 19, 2012 12:09 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I don’t think I’ve ever said “section” to a mathematician and had them say “what?”. But whenever I hear or say “right inverse” I have to stop and figure out whether that means “section” or “retraction”.

Posted by: Mike Shulman on December 19, 2012 6:56 AM | Permalink | Reply to this

Re: Rethinking Set Theory

“Section” and “retraction” are (somewhat) easier for a newcomer to remember than “left/right inverse”, because they have everyday meanings that can be connected to their mathematical meanings. “Left” and “right” are just based on the order in which a certain notation writes things on the page, and carries no intrinsic meaning related to what the things in question really are. Worse still, there are two opposite conventions for the order of the notation, both perfectly sensible!

Better still, in my opinion, would be directly meaningful names like “post-inverse” and “pre-inverse”, where the post-inverse of f gives the identity when you stick it after f, and the pre-inverse gives the identity when you stick it before f. It’s almost certainly too late to change such a deep-rooted naming convention now – but if there’s any way to do it, it’ll be by teaching the new names to newcomers! (Along with the old names, of course, so they can still talk to other people.)

Posted by: Stuart Presnell on December 19, 2012 9:07 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I conducted a poll (sample size: one) and found that “right inverse” got better recognition than “section”. But I completely agree: as a piece of terminology, “right inverse” isn’t great.

Sometimes I find myself saying “one-sided inverse” when I can’t remember which way round things go. If someone says “every surjection has a one-sided inverse”, I would have thought it’s obvious which side is meant. Ditto “right inverse”, I’d hope.

Posted by: Tom Leinster on December 21, 2012 2:37 AM | Permalink | Reply to this

Re: Rethinking Set Theory

At least because it should be obviously too much to ask for a factoring of the identity on the cover side of the surjection, yes; so there’s a unique sense in which “every surjection has a one-sided inverse” is sensible (if not unique s.t. grammatical). I am content.

Posted by: Jesse McKeown on December 21, 2012 4:26 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I just have one question/comment about Axiom 7. Is there any particular reason why you chose inverse images rather than general pullbacks or equalizers? I assume that you wanted to phrase the axiom in simple terms familiar to every mathematician. But then I would suggest that existence of equalizers is even simpler and more familiar. Informally speaking, it asserts that “every equation has the set of solutions”. It’s obviously a matter of taste but personally I find this more compelling as a basic principle than “every function has an inverse image of every element of its target”. The latter can also be phrased as the solution set of an equation where one side is constant, but I don’t see any advantage in restricting to such equations.

Posted by: Karol Szumiło on December 18, 2012 7:05 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Every math grad student at U.C. Riverside learns what an ‘inverse image’ is. Only students working on category theory have heard the word ‘equalizer’.

I suspect Tom is trying to make things immediately attractive to lots of people, rather than just people who already understand category theory. That seems like a wise objective, but I guess it’s important to state ones objective in foundational projects, since different objectives lead to different notions of success.

I hope the math community has reached the point of realizing that we really need not one foundation of mathematics, but many, together with clearly described relations between them. Indeed at this point the word ‘foundation’ is perhaps less helpful than something else… like maybe ‘entrance’.

Posted by: John Baez on December 18, 2012 7:06 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Every math grad student at U.C. Riverside learns what an ‘inverse image’ is. Only students working on category theory have heard the word ‘equalizer’.

But are they familiar with the universal property of an inverse image? If not then being introduced to this universal property is going to be just as big a leap as being introduced to the universal property of an equalizer. And my point was that you don’t have to use the word ‘equalizer’ to do it. You can replace it by ‘the set of solutions of an equation’ and this is surely understood by any student who understands ‘inverse image’.

Posted by: Karol Szumiło on December 18, 2012 8:58 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Karol, you’ve actually put your finger on the axiom with which I’m least happy. It seems to me that this is the most complicated one. Despite some effort, I couldn’t make it look any simpler.

It could be that the universal property of equalizers would be better in that regard. However, we’re still left with the problem mentioned below, that the notion of inverse image is needed for Axiom 8 (characteristic functions).

Posted by: Tom Leinster on December 18, 2012 9:46 PM | Permalink | Reply to this

Re: Rethinking Set Theory

It’s seems to me that one can equally well phrase Axiom 8. with equalizers as with inverse images. Namely, instead of saying “A=χ 1(t)A = \chi^{-1}(t)” we can say “AA is the set of solutions of the equation χ(x)=t\chi(x) = t i.e. an equalizer of χ\chi and the constant function at tt”. I find it just as clear and understandable but perhaps I’m not fully appreciating the position of a person not familiar with category theory.
Posted by: Karol Szumiło on December 18, 2012 9:58 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Is there any particular reason why you chose inverse images rather than general pullbacks or equalizers?

As you say, it’s just a matter of taste. I certainly agree that equalizers are fundamental too.

Probably the main reason for doing inverse images rather than equalizers is that this concept is needed anyway for Axiom 8 (characteristic functions). So it makes the presentation a bit more economical. John’s reason may have crossed my mind too — I can’t remember.

In reply to John’s point about multiple foundations, Colin McLarty’s book Elementary Categories, Elementary Toposes makes the same point more emphatically than anything else I’ve seen.

Actually, the word “foundation” doesn’t appear once in my draft. That was deliberate: I wanted to keep it focused, and in particular, avoid questions like “what is a foundation?”

Posted by: Tom Leinster on December 18, 2012 7:55 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I think the objection that ZFC requires everything to be a set is basically just a technicality; one can simply move from ZFC to ZFC with atoms ( http://ncatlab.org/nlab/show/ZFA ) and obtain an essentially equivalent theory, in which not everything needs to be a set any more. Logicians prefer to work with a pure set theory because it makes proof theory and model theory easier, but certainly from the point of view of working mathematician, an impure set theory with atoms is certainly conceptually preferable.

[An aside: I was not able to figure out how to use HTML in comments. Presumably the mysterious “Text filter” options are relevant, but I have no idea what “Markdown”, “Textile”, etc. are, and some experimentation did not produce any useful results. Adding some text to the comment boxes to explain the options better would be nice.]

Posted by: Terence Tao on December 18, 2012 7:33 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think the objection that ZFC requires everything to be a set is basically just a technicality;

That’s true and I can see how this leads people to conclude that there is no significant difference between so called material and structural set theories. However, I believe that this is only a symptom of a deeper “problem”. Namely, set theories like ZFC or ZFC with atoms force us to carry out many constructions by hand, for example in order to define products we need to introduce a particular notion of an ordered pair. There are many choices of such a definition, none more canonical than the others. Of course we can make this choice, prove the universal property of products and then forget our choice for all eternity. But having to make this choice in the first place is a distraction and distractions of this type happen all the time, for example in the classical construction of the progression of algebraic structures \mathbb{N}, \mathbb{Z}, \mathbb{Q}, \mathbb{R}. Structural set theory like ETCS allows us to assert that all the objects with expected universal properties exist without going into irrelevant details of their implementations which reduces the number of distractions.

Admittedly, those are not real “problems”. Those are merely “inconveniences” which are only inconvenient to people who are used to doing things in particular ways (e.g. defining things by their universal properties whenever possible).

Posted by: Karol Szumiło on December 18, 2012 8:10 AM | Permalink | Reply to this

Re: Rethinking Set Theory

You can get from a model of ZF plus a specified set of atoms to a model of ZFA, which is why Zermelo dropped atoms from his original axioms, but going the other way is not so simple.

Posted by: David Roberts on December 18, 2012 9:04 AM | Permalink | Reply to this

Re: Rethinking Set Theory

But is there any way to build mathematics in ZFA in such a way that all the mathematical objects that we don’t think of as sets, such as π\pi, end up being atoms? I can’t think of any way to, say, define the real numbers in ZFA, other than with the usual constructions, in which they end up being sets. There are atoms in ZFA, but since they don’t have any structure given on them, they don’t seem to participate in mathematics.

Of course, you could use the axiom of choice to pick a particular set of atoms which is bijective to the set-constructed real numbers (assuming you have sufficiently many atoms), transport all the structure of the real numbers across that bijection, and then declare that your set of atoms is now “the real numbers”. But that is starting to smell to me like a kludge, kind of like Bourbaki’s tedious definition of what kinds of set-theoretic baggage a “structure” is not allowed to refer to, or the comment of McLarty’s character Tasha that “the advantage of your set theory is that mathematicians never work with your sets!”.

Moreover, if you did that same procedure with every set whose elements you don’t want to think of as sets, then you would have to keep choosing new disjoint sets of atoms forever — unless you want it to be the case that perhaps π\pi is equal to a point on the torus, which is another instance of the same problem. In other words, you can get away from a global membership predicate by working with atoms, but you also have to worry about getting away from a global equality predicate, which is just as meaningless.

[P.S. I agree that it would be good to have more explanation of the text formatting options, but fortunately unless and until that happens there is google.)

Posted by: Mike Shulman on December 18, 2012 1:13 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Mike: yes, and no…

My favourite proof that a properclassworth of atoms is equiconsistent with ZFC: Take your favourite (V,)ZF(V,\in) \vDash ZF and define a relation xxyy on VV by the formula “yy is a \in-singleton and xx is \in the element of yy”. Then € is a well-founded relation, it is extensional-on-\in-singletons, and the atoms of (VV,€) are all the nonsingletons of (V,)(V,\in); and certainly (V,)(V,\in) knows how to build a real line of (VV,€) atoms, say given a set of Dedekind cuts (e.g.); the annoying thing is that (VV,€) obviously doesn’t know what is \in its atoms, so by the time you get there, you’ve forgotten. But maybe you don’t need to forget?

I’m pretty sure you could also build a decent model doing just what you want with Henkin constants, because “if any (R,+,)(R,+,\cdot) is a complete ordered field whose underlying set contains only atoms, then XX is one” is easy enough to say. But again, that doesn’t feel very satisfying, somehow. The real beauty of “everything is a set” is, I think, the definability of equality; with too many atoms you just have to know that they’re distinct — it seems like a heap of sand, only less structured.

(n.b., itex doesn’t like €, the

Posted by: Jesse C. McKeown on December 18, 2012 4:18 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Jesse

ah, very interesting. I was needing to assume the existence of a proper class of atoms in a proof, so I’m glad it doesn’t have stronger consistency strength. Do you have a reference for this?

Posted by: David Roberts on December 18, 2012 10:45 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Reference? No, it was a puzzle one day. Part of the puzzle is to define in \in a morphism from (VV,\in) to (VV,€), but this is straight-forward if you think of it as “doubling braces”. You can recover ZF(C?) by transcribing all quantifiers to mention that the transitive closure of what they bind omits all atoms.

Just today I’ve started trying to figure out how to construe ZFA as a fragment of what one ought to call ZF[Φ\Phi], (just add one predicate symbol), a subfragment of the part that universalizes over all proper-class-satisfiable formulae with a single free variable. The idea behind that was the intuition that, e.g., analysis doesn’t care about the predicate τ\in \tau, only the predicates <τ,τ, \lt \tau, \leq \tau,\dots . One way to get at that is to declare atoms!: for some things x\in x is ungrammar, but another way is to declare we only consider properties that do not depend on π\in \pi for Φ(π)\Phi(\pi). But I don’t know how to make that more precise. Brace-doubling, I’m pretty sure, doesn’t need so much thinking.

Posted by: Jesse McKeown on December 18, 2012 11:46 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Ok, I’ll just cite you for personal communication then :-)

Posted by: David Roberts on December 18, 2012 11:51 PM | Permalink | Reply to this

Re: Rethinking Set Theory

No no no! it’s an exercise!

Posted by: Jesse C. McKeown on December 19, 2012 12:13 AM | Permalink | Reply to this

Re: Rethinking Set Theory

certainly (V,∈) knows how to build a real line of (V,€) atoms

Yes, but (V,€) doesn’t know how to do that. Hence, not when you’re doing mathematics in ZFA.

Posted by: Mike Shulman on December 19, 2012 6:58 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Terry, you can find some information on the various text filters here. I generally use “itex to ML with parbreaks” as my filter. The HTML command <a href=”http://ncatlab.org/nlab/show/ZFA”>(http://ncatlab.org/nlab/show/ZFA)</a> should work to give you (http://ncatlab.org/nlab/show/ZFA), at least in this filter.

Posted by: Todd Trimble on December 18, 2012 3:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Terry wrote:

I think the objection that ZFC requires everything to be a set is basically just a technicality; one can simply move from ZFC to ZFC with atoms

I don’t dispute that one can introduce atoms or urelements (though it seems that Mike is not persuaded that it can be done in a way that reflects ordinary mathematical practice).

What I’d like to ask is: why would one want to choose this option, with its accompanying technicality, over the other options on offer? In particular, what reasons might one have for preferring it to the theory (due to Lawvere) described in my draft?

An aside: I was not able to figure out how to use HTML in comments. Presumably the mysterious “Text filter” options are relevant

Yes, sorry. That aspect of the site could definitely be improved, and I think you’ve remarked on this before. Since you’re familiar with MathOverflow, I suggest that you always choose the second option, “Markdown with itex to MathML”. This allows you to write things pretty much as you would do there.

Posted by: Tom Leinster on December 18, 2012 8:42 PM | Permalink | Reply to this

Re: Rethinking Set Theory

My view is that ZFC with atoms (or more precisely, ZFC with a dynamically evolving collection of types (and operations, constants, etc.), including but not restricted to sets, which is not as clean to axiomatise as ZFC or ZFA, but more accurately reflects the way such frameworks are actually used by mathematicians in practice) is analogous to a standard high-level object-oriented computer languages such as C++, in which one initially has the capability to do a number of powerful but conceptually awkward things (e.g. identify numbers with sets in ZFC, or caste a pointer into a number in C++), but then after installing some standard “constructions” or “libraries” (in which certain operations become encapsulated, and information hidden, into new objects and types, in which only some of the operations available to raw sets continue to be accessible by the user) one ends up with a collection of objects and methods which hew more closely to the way mathematicians/programmers actually think about the objects (or models of objects) that they manipulate. Yes, some of these constructions can be quite messy, but in practice one usually just has to do the mathematical equivalent of “#include “reals.h”“, “#include “pairs.h”” etc. to gain access to the real numbers (or ordered pairs, etc.) together with their methods, axioms, and theorems, and then proceed without further introspection of the implementation of these objects, knowing that someone has at some point tested that these constructions actually “compile” in ZFC. The more “advanced” features of set theory (e.g. the ability to have sets of sets, sets of sets of sets, and so forth) then mostly disappear from view outside of these basic constructions, save in some specialised contexts, e.g. when deploying the theory of ordinals to perform transfinite induction.

For the type of maths that I deal with regularly, this is certainly adequate. I gather though that when dealing with large categories, things can get annoying (unless one invokes “#include “grothendieck_universes.h”” or something, which is not fully supported by the base ZFC language and requires an axiom upgrade). (It’s not just categories, though; set-theoretic foundations are also somewhat imperfectly suited for modeling algorithms in complexity theory, or random variables in information theory, though the issues here are different, having to do instead with how smoothly the foundations deal with dynamic updates to one’s objects, or information about these objects.) So, much as C++ type languages are not ideal for all programming applications, I certainly agree that set theoretic foundations are not ideal for all mathematical applications. Nevertheless, in my opinion, the set theoretic framework (once augmented with the ability to dynamically install new objects and methods) works well for quite a broad slice of mathematics, though certainly it is not always the foundation of choice.

Posted by: Terence Tao on December 19, 2012 1:56 AM | Permalink | Reply to this

Re: Rethinking Set Theory

That’s a very nice perspective, Terry! But I don’t quite see how it answers the question

why would one want to choose this option, with its accompanying technicality, over the other options on offer?

To extend the analogy in the obvious way, there are better languages than C++ around nowadays, particularly functional languages like ML and Haskell. You don’t need to choose a language like C++ that’s implemented as a thin layer on top of assembly code, with all the attendant bizarre quirks and pitfalls. You can work instead in a language where things like pairs, record types, and more general inductive and coinductive datatypes are basic notions, with function defined by pattern-matching, first-class function objects, higher-order polymorphism, etc. Moreover, mathematicians (at least when doing non-formalized mathematics) have the advantage over programmers that they don’t need to maintain backwards compatibility with papers written 30 years ago. C++ and ZFC are certainly adequate, but why would you choose them?

Posted by: Mike Shulman on December 19, 2012 7:05 AM | Permalink | Reply to this

Re: Rethinking Set Theory

One reason is pedagogical; set theory (much like group theory or linear algebra) can be initially taught to students as a specialised subfield of mathematics in which the cloud of basic concepts and results that the student needs to absorb being small enough that it can be managed in a single quarter or semester of an introductory course. (I’m considering more advanced uses of set theory, e.g. Zorn’s lemma, as lying outside this basic cloud.) Later on, it can then be demonstrated that basically all other mathematical concepts can be modeled within set theory, which is really an amazing and non-trivial mathematical phenomenon (a “Zermelo-Frankel thesis”?) which is taken for granted these days, but which I think should be stressed more in higher mathematical education.

Note for similar reasons that introductory programming courses typically begin with a C++ type language (it _was_ C++ in my day, I gather that Python or Java are more popular these days) as one can initially do quite a lot with this language just using the basic features and concepts, without having to understand more advanced topics such as polymorphism or first-class functions or what have you. I don’t know of a programming curriculum (aimed at typical CS students) that starts with Haskell as a _first_ programming course - I think the sheer number of abstract concepts that one has to absorb upfront is too much for all but the brightest of students. (But it would make an excellent second or third course.)

But for a praticising user, the choice of foundations is almost irrelevant. When I use, say, SAGE, I really don’t care whether the software was initially written in C++, Haskell, or some other language, so long as I have reasonable reassurance that the software is reliable (e.g. by having open source code that one can compile oneself). (Similarly if one replaces SAGE by SGA, and C++ and Haskell by ZFC and ETCS.)

Perhaps the one feature of ZFC that I really do rely on in practise, though, is Zorn’s lemma: I can guarantee the existence of maximal objects in any non-empty class X with totally bounded chains, so long as I can first verify the condition that X is a set and not a proper class. So I can’t find a maximal group or a maximal vector space, but I can have maximal ideals and maximal filters and maximally defined linear functionals and so forth. This is perhaps the most common place in practise in ZFC where one actually has to know how to show that something is a set or not (as opposed to a class), and in which one actually uses the full axiom set of ZFC rather than some core set of tools which could be easily replicated in any other reasonable foundational model. So Zorn’s lemma is perhaps the main place where the set theoretic foundations still protrude out onto the surface, rather than being buried under layers of intermediate foundations in which all other core mathematical structures (number systems, categories, universal constructions, etc.) are constructed.

Posted by: Terence Tao on December 20, 2012 4:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Zorn's Lemma is enough like ‘real’ math that it looks the same in both material (like ZFC) and structural (like ETCS) set theories. Certainly when we wrote about it on the nLab, we didn't have to think about this issue. The nLab's tendency to consider constructive mathematics shows up there, but the tendency to use structural set theory is invisible.

Posted by: Toby Bartels on December 20, 2012 7:34 PM | Permalink | Reply to this

Re: Rethinking Set Theory

set theory … can be initially taught to students as a specialised subfield of mathematics in which the cloud of basic concepts and results that the student needs to absorb being small enough that it can be managed in a single quarter or semester of an introductory course.

I think this is equally true of structural set theory (like ETCS and SEAR) as it is of membership-based set theory. In fact, Lawvere initially invented ETCS while designing an introductory set theory course, wanting to teach students to think about sets the way mathematicians actually use them. I don’t see any reason other than the weight of tradition for teaching students ZF-style set theory.

I don’t know of a programming curriculum (aimed at typical CS students) that starts with Haskell as a first programming course

Here’s one that uses ML. One doesn’t need to understand the fancier aspects of a functional programming language to use it in a basic way, any more than one needs to understand the Standard Template Library in order to use C++.

Posted by: Mike Shulman on December 20, 2012 9:17 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Terry, I’m puzzled by your comments, so much so that I wonder if there’s been some miscommunication.

To be clear: I haven’t argued against using set theory as a foundation, or against teaching set theory. I have presented some views about which version of set theory it’s most fruitful to use or teach — but that’s not the same thing.

So, for example, I’m puzzled that when Mike asked:

C++ and ZFC are certainly adequate, but why would you choose them?

you answered with:

One reason is pedagogical; set theory [is a good thing to teach for various reasons].

I don’t think anyone’s disagreeing with this. But Mike’s question, and the question raised in my draft, isn’t whether we should teach set theory: it’s which version we should teach (ZFC, ETCS, etc).

I’m also puzzled by this:

Perhaps the one feature of ZFC that I really do rely on in practise, though, is Zorn’s lemma

I’d definitely go along with the statement that lots of people rely on Zorn’s lemma. But as Toby said, Zorn’s lemma is as much a feature of ETCS as it is of ZFC.

Personally, I don’t find it helpful to think of Zorn’s lemma as belonging to set theory at all: I think it’s more accurate to view it as piece of pure order theory. (See particularly this comment. In summary, one can prove Zorn’s lemma as follows. First prove the Bourbaki–Witt fixed point theorem, which is a tricky piece of order theory but has no noteworthy set-theoretic content; it doesn’t even use choice. From here it takes only a few more lines of order theory to deduce Zorn’s lemma. The only part of this that comes close to involving set theory is in those few more lines, since, inevitably, they do use choice. But they use it in the most straightforward, transparent way: one actually uses the axiom of choice itself, not some sophisticated consequence of it.)

Posted by: Tom Leinster on December 21, 2012 3:10 AM | Permalink | Reply to this

Re: Rethinking Set Theory

People don’t learn ZFC, outside of a set theory course. They learn a naive set theory that can be reasonably interpreted as a fragment of ZFC with atoms. Pedagogically, ETCS is much harder to understand than the naive set theory. Naive set theory has a very simple intuition: a set is an unordered list of things enclosed in brackets. Two sets are equal if the two lists are the same. I honestly understood this notion of set by age 10. The only thing missing is a clear description of the universe of discourse.

Posted by: Walt on December 22, 2012 8:40 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Could you explain why atoms are necessary? I don’t understand this point.

Posted by: Tom Ellis on December 22, 2012 10:37 AM | Permalink | Reply to this

Re: Rethinking Set Theory

They’re not logically necessary, but I think from the naive point of view we think of a bunch of things as atomic. For example is {2} a member of the ordered pair (2, 3)? Naively, I would think of (2, 3) as an atom that has no elements, but under the Kuratowski definition of ordered pairs, {2} is indeed a member of (2, 3).

Posted by: Walt on December 22, 2012 12:03 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Or, to take a more extreme example, I don’t think any mathematician would say that 33 is an element of 55 but, if we are using Von Nuemann’s definition of ordinals, it is.

Posted by: David Speyer on December 23, 2012 4:26 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Walt, I wouldn’t disagree with much of what you wrote, but I’d add some comments.

People don’t learn ZFC, outside a set theory course. They learn a naive set theory that can reasonably be interpreted as a fragment of ZFC with atoms.

What I’d add here is that the naive set theory that everyone learns can also reasonably be interpreted as a fragment (or, more accurately, an informal version) of ETCS or SEAR or any of a number of other set theories. I don’t think there’s anything special about ZFC in this regard.

One can ask which axiomatic set theory is closest to naive set theory. That’s always going to be a subjective judgement, but part of the purpose of my paper is to argue that ETCS is closer than ZFC.

Pedagogically, ETCS is much harder to understand than naive set theory.

Agreed. Any kind of axiomatic set theory is bound to be harder than naive set theory. (Presumably, axiomatic anything is always harder than its naive counterpart.)

Posted by: Tom Leinster on December 22, 2012 6:55 PM | Permalink | Reply to this

Re: Rethinking Set Theory

In lieu of an argument, I have a question about ETCS. Given an arbitrary set, S, can I form the subset of all elements of S that are ordered pairs? Not ordered pairs from a specific product, but ordered pairs from anywhere.

I recognize that maybe I don’t need to ever do this, but I would find it disturbing

Posted by: Walt on December 24, 2012 1:29 PM | Permalink | Reply to this

Re: Rethinking Set Theory

…if I couldn’t.

Posted by: Walt on December 24, 2012 1:30 PM | Permalink | Reply to this

Re: Rethinking Set Theory

In ETCS, it doesn’t make sense to ask whether a given element of an arbitrary set “is” an ordered pair. An element of a set SS only “is” an ordered pair if SS is equipped with projections p:SAp:S\to A and q:SBq:S\to B making it into a product of AA and BB, in which case you can regard any sSs\in S as the ordered pair (p(s),q(s))(p(s),q(s)). But a different choice of AA, BB, pp, and qq might lead you to regard ss as a different “ordered pair”. For instance, if you choose 1 S:SS1_S:S\to S and !:S1!:S\to 1, then you can regard any sSs\in S as the ordered pair (s,)(s,\star).

In ETCS, sets are collections of completely unstructured elements. An element of a set only “is” anything insofar as that set is equipped with structure that gives meaning to it. For instance, any countable set XX can be regarded as “the” natural numbers by choosing an element 0X0\in X and a bijection s:XX{0}s:X \to X\setminus \{0\}, and no such XX is any better than any other: “the” natural numbers are only determined up to unique isomorphism.

Posted by: Mike Shulman on December 24, 2012 3:51 PM | Permalink | Reply to this

Re: Rethinking Set Theory

So that’s much further from ZFC than bounded Zermelo is. This comes down to aesthetics, but I find that incredibly unattractive. Once I label something 0, 1, 2, 3, …, then there is a unique natural numbers object: {0, 1, 2, …}. I’m happy to say that I have to pick something to label that, and that there are many isomorphic choices, but once I pick, then I have definitively labeled the natural numbers, and all of its subsets, and sets of subsets, etc.

Posted by: Walt on December 24, 2012 5:08 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Once I label something 0, 1, 2, 3, …, then there is a unique natural numbers object: {0,1,2,}\{0, 1, 2, \dots\}

That’s really no different from ETCS. The order is just the other way 'round: once you pick the natural numbers object, then there are unique things labeled 0, 1, 2, 3, …. And once you’ve picked a natural numbers object, then you can perfectly well call it the natural numbers, and all of its subsets, sets of subsets, etc. Why should it matter one way or the other?

Posted by: Mike Shulman on December 24, 2012 7:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Walt, I think you’ve raised an important point. Here’s the short version of this long comment: by changing ETCS in an insubstantial way, you can have a distinguished natural numbers object, if you want.

The long version: ETCS (as phrased in my draft) asserts the existence of various sets:

  • a set with exactly one element
  • an empty set
  • a product set X×YX \times Y for each XX and set YY
  • a function set Y XY^X for each XX and set YY
  • an inverse image set f 1(y)f^{-1}(y) for each f:XYf\colon X \to Y and yYy \in Y
  • a truth-value set 2\mathbf{2}
  • a natural numbers set \mathbb{N}.

It also asserts the existence of various bits of extra structure carried by those sets, e.g. the projections X×YXX \times Y \to X and X×YYX \times Y \to Y.

In each of the cases listed above, the set asserted to exist (together with its accompanying structure) is determined uniquely up to structure-preserving isomorphism.

In each case, we have a choice about how to present the axiom asserting existence: do we want to nominate as special one particular set satisfying the condition in question, or should we merely state that at least one set satisfying it exists? In some sense it doesn’t matter (because they’re all isomorphic anyway), but if we’re trying to model how mathematicians actually reason, maybe it does.

This gives rise to many micro-variants of ETCS. Here are the two possible extremes.

At one extreme, the list of primitive concepts is as short as possible:

  • some things called sets
  • some things called functions between sets
  • an operation of composition.

The axioms then look pretty much as they do in my draft, e.g. they assert the existence of a natural number system (with no particular natural number system distinguished as special).

At the other extreme, the list of primitive concepts is as long as possible:

  • some things called sets
  • some things called functions between sets
  • an operation of composition
  • an identity function on each set
  • a distinguished set 1\mathbf{1}
  • a distinguished set \emptyset
  • for each set XX and set YY, a distinguished set X×YX \times Y and functions X×YXX \times Y \to X, X×YYX \times Y \to Y
  • for each set XX and set YY, a distinguished set Y XY^X and function Y X×XYY^X \times X \to Y
  • for each f:XYf\colon X \to Y and yYy \in Y, a distinguished set f 1(y)f^{-1}(y) and function f 1(y)Xf^{-1}(y) \to X
  • a distinguished set 2\mathbf{2} and function t:12t\colon \mathbf{1} \to \mathbf{2}
  • a distinguished set \mathbb{N} and functions 0:10\colon \mathbf{1} \to \mathbb{N} and s:s\colon \mathbb{N} \to \mathbb{N}.

Then the axioms look slightly different, e.g. Axiom 9 states that \mathbb{N}, 00 and ss form a natural number system (rather than merely stating that a natural number system exists). Then you can happily refer to the natural numbers.

There are pros and cons to the two extremes (and all intermediate points). The mathematical vernacular seems to be closer to the second extreme: we talk about the product, the natural numbers, etc. On the other hand, I remember one of my undergraduate tutors writing on the blackboard

1,2,3,4, 1, 2, 3, 4, \ldots

and declaring fiercely:

These are not the natural numbers! These are the Arabic numerals!

He might have continued by writing

I, II, III, IV, \text{I, II, III, IV}, \ldots

and saying that these aren’t the natural numbers either. (For what it’s worth, he was a differential geometer, and to my knowledge had no interest in foundations.)

In the same vein as my ex-tutor’s point, if we have a group GG and normal subgroups H,NH, N with trivial intersection and satisfying G=HNG = H N, we want to be able to say that GG is a (the?) direct product of HH and NN, undeterred by the irrelevant question of whether GG is literally equal to the canonized product H×NH \times N.

These matters don’t have much to do with ETCS in particular: the questions raised can be asked of all set theories. (To some extent we’re engaged in applied mathematics here, a muddy modelling problem: we’re trying to model what real-life flesh-and-blood mathematicians actually do.) For example, the business about products of groups applies to the traditional approach to set theory too, quite apart from the usual points about (x,y)={{x,y},{y}}(x, y) = \{ \{x, y\}, \{y\}\}.

These seem to me to be deep waters. Indeed, one of the many, diverse reasons why higher-dimensional category theory took off is that some people (e.g. Makkai) thought it might help with clarifying questions of equality vs. isomorphism etc. In any case, I don’t think I’ve ever seen any handling of these matters that I’ve found really convincing.

Posted by: Tom Leinster on December 24, 2012 7:58 PM | Permalink | Reply to this

Re: Rethinking Set Theory

… higher-dimensional category theory … might help with clarifying questions of equality vs. isomorphism etc. In any case, I don’t think I’ve ever seen any handling of these matters that I’ve found really convincing.

Okay, with a lead-in like that, I can’t resist: what about the univalence axiom? In univalent foundations, every natural numbers object is equal to every other. Every direct product of two given groups is equal to every other. Etc. (Of course, you have to get used to treating “equality” a bit differently from in ordinary mathematics.)

I’ve been playing around recently with doing some bits of “classical set theory” in univalent foundations. Here’s one nice thing you get: you can define an “ordinal number” to be simply a well-ordered set. By the univalence axiom, any two isomorphic well-orderings are, in fact, equal. So there is no need to bother about “canonicalizing” well-orderings by von Neumann’s trick of requiring the order operation to be set-membership (which we can’t do in type theory anyway), but we still have the nice property that ordinals are unique (in the sense of equality) representatives of well-order types. Moreover, since any two isomorphic well-orderings are uniquely isomorphic, the type of all ordinal numbers is itself a set (i.e. an h-set), and hence itself an ordinal number (in the next higher universe).

There is a nice definition of a “cardinal number” too: a cardinal number is an element of the 0-truncation of the type of h-sets. This captures exactly the intent that isomorphic sets have the same cardinality, but that that “sameness” no longer remembers which isomorphism you might have picked. In particular, the type of cardinal numbers is also a set (in the next higher universe).

Posted by: Mike Shulman on December 24, 2012 10:51 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Mike wrote:

with a lead-in like that, I can’t resist: what about the univalence axiom?

Hard for me to say, as I’ve never understood it. It’s not that I’ve tried and failed, it’s just that I haven’t put the time into it. Will you be talking about this kind of thing at the workshop in Sydney?

Posted by: Tom Leinster on December 24, 2012 11:41 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Well, I’m not sure it’s exactly within the mandate: it’s not really category theory as such, nor is it especially applicable to anything yet. I might say something about it in my talk at the main conference, though.

Posted by: Mike Shulman on December 27, 2012 7:45 AM | Permalink | Reply to this

Re: Rethinking Set Theory

This gets at what I would expect a set theory to provide. Let’s say we go with the minimal version of ETCS you describe. You can still talk about the equality of functions in ETCS, right? Then intuitively, I know what it means to form sets of functions, and I know what it means for two sets of functions to be equal. Once we know what equality for any type of object, intuitively we can form sets of that thing, or sets of sets of sets of sets of that thing, and we know what it means for two sets of sets of sets of sets of that thing to be equal. I find this a compelling feature.

Posted by: Walt on December 26, 2012 9:31 AM | Permalink | Reply to this

Re: Rethinking Set Theory

In ETCS, however, there is no such thing as ‘forming a set of’ anything. A set in ETCS is not a collection of pre-existing things, be they functions or anything else.

Posted by: Mike Shulman on December 27, 2012 7:47 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Right, and that’s what’s wrong with ETCS as a formalization of naive set theory, in my opinion. Sets are sets of things, and I can form them any time I want. Right now, I’m forming the set { {Mike, structural set theory} } and { {Walt, material set theory} }, and no one on God’s green Earth can stop me.

I actually don’t get the appeal of preventing the formation of sets of specific things. The fact that you axiomatize the category of sets with no reference to elements is interesting, but if you’re arguing that something like ETCS should be the foundations of mathematics (and maybe you’re not), then you’re saying that almost everyone would be better off if almost no one ever referred to elements. Which is a bold claim.

Posted by: Walt on December 27, 2012 10:49 AM | Permalink | Reply to this

Re: Rethinking Set Theory

> Sets are sets of things, and I can form them any time I want.
> Right now, I’m forming the set {{Mike, structural set theory}}
> and {{Walt, material set theory}}, and no one on God’s
> green Earth can stop me.

I won’t stop you, but I must confess I think this construction
is the most extraordinary one I have seen in this thread, I am
still struggling to grasp it, honestly. (What do you think
about being in this set, Mike, and what other sets do you belong
to?)

Why on Earth would you form that set and how would you actually
do it? Suppose you have trapped those two ‘specific things’ in
a magnetic field and you have studied them by throwing
negatively charged cashew nuts at them; who would be interested
in your specific results? I think most people would be more
interested in a result about {a,b}, that they can relate to
their own research.

Note to Tom: I apologise for polluting the thread with this
tone, I know you don’t like it. (Tom writes: Thanks. See my comment below: http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042898 – TL.) Since I wrote the first comment I have been following the whole thread. I am quite marvelled
with all these insights about sets, it has opened my eyes to
many interesting questions I had never thought about.
Personally I only use sets as an engineer, as a quick and dirty
device for talking about discrete groupoids. I reckon there is
a lot more to it.

Posted by: Joachim Kock on December 27, 2012 2:19 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I know I’m speaking out of turn (since Joachim’s comment was addressed to Walt), but I’ll take the opportunity to respond myself as an exercise in writing down, as sympathetically as I can, what I think the basic position is.

The root intuition that Walt is pointing to is that if you have any collection of ‘things’ (entertaining for the moment the idea that we can consider ‘Mike Shulman’ and ‘structural set theory’ to be things), then you can imagine bracketing that collection, forming a new thing which is the set of all things in that collection.

(As we know from Russell’s paradox, this naive principle cannot be applied with absolute impunity. The precise scope of the application is the business of a set theory, or at least a set theory of this type, to specify.)

I’m sure Walt would agree that such sets as the ones he named have no mathematical importance whatever. But pedagogically, this idea of set-formation is elementary, and he sees no reason why such things should not be admitted as sets. I mean, why not? The idea is so simple and free, you can teach it to young children: why then muck it up with unnecessary complications and restrictions on freedom? Which is what he and others see ETCS as doing.

I think the position is also that it is not such a huge step to formalize that root-idea, retaining plenty of freedom and with enough constructions available to do mathematics. If we think of all things in the world as divided into either sets or not-sets (not-sets being called ‘atoms’ in the jargon), so that ‘Mike Shulman’ and ‘structural set theory’ are considered atomic things, then the axiom of pairs allows Walt to form the set {MikeShulman,structuralsettheory}\{Mike \; Shulman, structural \; set \; theory\} just as he would like (or at least can’t see why he should be denied).

Pursuing this line of thought, the basic ideas and constructions of traditional set theory (e.g., unions, intersections, even power sets) are simple enough that you can teach them to young children, so that, for example, if you asked them to say what are the elements of the power set of {MikeShulman,structuralsettheory}\{Mike \; Shulman, structural \; set \; theory\}, they would get the right answer, and could easily extrapolate from those experiences.

My guess is that Walt and others believe that the move from the naive root-ideas that we can teach children to axiomatic ZFC is not huge, in fact is fairly natural once certain issues like Russell’s paradox are brought to attention, and this gives ZFC a considerable pedagogical advantage over something like ETCS – something you could easily teach to high-school students.

I think these advocates also have a hard time seeing any single root-idea to ETCS comparable to the root-idea of set-formation that informs ZFC. I am guessing that to them, ETCS could seem more or less like a exercise in structural ‘hygiene’, and perhaps a pointless one at that, in that the point of such hygiene is one you don’t really have to make to mature mathematicians – they have long digested e.g. the important point of the real number system is that it forms a complete ordered field, and they don’t need to be instructed in a new sort of foundations in order to grasp that point. For the ZFC advocates, I think the idea is that the pedagogical advantages of ZFC (or bounded Z, or whatever) vastly outweigh any supposed advantages of the ‘hygiene’.

Posted by: Todd Trimble on December 27, 2012 6:04 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This is well-said, Todd.

Posted by: Walt on December 28, 2012 7:43 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks for this nice summary, Todd. Of course, there are many ways one might reply. Naturality, simplicity, and root-ideas can be in the eye of the beholder, and there’s only so far that discussion can get us there. I think intuition can be developed, and even someone raised on ZFC can eventually come to feel that ETCS is just as simple and natural and obvious, but you have to be motivated to modify your intuition.

I think the best motivation is the reason for ETCS that Tom scrupulously avoided mentioning: it generalizes. Even if we accept for the sake of argument that ZFC is easier to teach to students (at the moment I’m making no claim either way on that), one can still argue that ETCS is a better set theory to teach to (at least some) students, because whatever difficulties there are in learning it are difficulties that a serious student of mathematics will eventually have to overcome anyway. Learning to think structurally and category-theoretically is a valuable — some might say essential — skill for a mathematician, and a course in set theory is a good time to start acquiring that skill. It’s not uncommon in mathematics that there may be an easy way to think about something and also a way that is initially more difficult, but which pays off more in the long run.

Furthermore, if you care about internalizing mathematics in nonstandard models — not only in order to prove formal independence results, as set theorists do, but because you care about the nonstandard models in their own right and you want to use internalization to prove things about them — then ETCS is your friend and ZFC is your enemy. Structural set theory — and its sister, type theory — is very well adapted to internalizing in many different contexts, precisely because those contexts are generally constructed structurally, like most of the rest of mathematics. For instance, a sheaf of sets is a structural notion: the sheaf structure pays no heed to the global \in relation. Sheaves on any particular space form a category, which is in fact a topos, a category which has a lot in common with a model of ETCS, and inside of which a theory closely related to ETCS can be interpreted.

You can, of course, perform the ETCS-to-ZFC wellfounded-trees construction inside that model and obtain a model of ZFC (or, in general, an intuitionistic variant thereof). But if you do this in a naive way, then not every object of the topos will necessarily be visible at all to the ZFC-like model: only those which support some internal “wellfounded-extensional structure”. If you do it rather more carefully, then you can get a model of a ZFC-like theory with atoms, in which every object of the topos can be found as a certain “set of atoms”. However, at this point it is material set theory which is starting to seem like a pointless exercise: why not use the structural set theory (or type theory) which arises much more naturally?

Posted by: Mike Shulman on January 3, 2013 11:57 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I guess it comes as no surprise that I agree with you, Mike. It certainly seems to me that if one is raised on ZFC and then one wants to learn about some more modern developments such as topos theory, type theory, etc., then one really has to retool the way one thinks about sets (and the more entrenched or “ontologically committed” one is to seeing sets in terms of a cumulative hierarchy, the more difficult or painful this relearning or unlearning might be).

Pedagogically, I do have faith that structural set theory could be taught to high-school students, both naively and axiomatically (using SEAR perhaps?). I would be interested to hear about classroom experiences in this regard; it’s one thing to talk about it and another actually doing it. I think it would take a lot of careful thought and planning the first time around.

Posted by: Todd Trimble on January 4, 2013 2:15 AM | Permalink | Reply to this

Re: Rethinking Set Theory

That’s very well put, Mike.

I did actually make some similar points in my paper (under “A broader view” and “What kind of set theory should we teach?”, towards the end). But I think you’ve put it more persuasively.

Todd wrote:

Pedagogically, I do have faith that structural set theory could be taught to high-school students, both naively and axiomatically (using SEAR perhaps?). I would be interested to hear about classroom experiences in this regard; it’s one thing to talk about it and another actually doing it. I think it would take a lot of careful thought and planning the first time around.

Yes indeed. I’d like to have the opportunity to give it a go. But it’s a big enough challenge that I’m not going to do it as a freebie: I’d do it if we had an undergraduate set theory course and I was teaching it, but we don’t and I’m not.

I’m in two minds about SEAR, pedagogically. It certainly has a lot going for it, but what makes me pause is that the axioms refer a couple of times to the notion of first-order formula. Like it or not, most students won’t know what this means and will have to be told, at least if one is going to do the thing with precision. (The intuitive idea may be clear, but I’m talking about a fully rigorous approach.)

I think Mike has said that from his point of view, SEAR comes closer to describing how mathematicians use sets in practice than ETCS does. It could be argued that SEAR is also a little harder to understand (when all the details are included), because it depends on the notion of first-order formula. Whether one agrees or disagrees with these two points, let’s just accept them for the sake of the rest of this comment.

The situation is then that we have two set theories, one of which models what mathematicians do more accurately but is less easy for mathematicians to understand. This isn’t a contradiction. By way of comparison, a mathematical model of the migratory behaviour of wildebeest might be very accurate and yet really quite difficult for a wildebeest to understand.

What makes our situation different from the wildebeest situation is that here, mathematicians are both the modellers and the modelled. We sometimes distinguish the two roles by calling the modellers “logicians” (to be compared to mathematical ecologists) and the modelled “ordinary mathematicians” (to be compared to wildebeest).

Posted by: Tom Leinster on January 4, 2013 12:11 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I did actually make some similar points in my paper

Oops, I misremembered. I should have gone back to check. (-:

I’m in two minds about SEAR, pedagogically…. what makes me pause is that the axioms refer a couple of times to the notion of first-order formula.

This is, of course, equally true for ZFC, and also for ETCS+R. Are you saying that you think ETCS is easier to understand than ZFC as well, because it doesn’t involve first-order formulas?

ETCS doesn’t include the separation axiom, because you can prove a (bounded) separation property from the other axioms. But if I were teaching a course using ETCS, I would feel obligated to do that proof, because I feel like in practice, mathematicians use separation a lot when talking about sets. And I don’t really see how to state the separation property precisely without introducing first-order formulas either. Do you have an alternative in mind?

Posted by: Mike Shulman on January 4, 2013 11:36 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This is, of course, equally true for ZFC, and also for ETCS+R. Are you saying that you think ETCS is easier to understand than ZFC as well, because it doesn’t involve first-order formulas?

Yes, in this respect at least.

And I don’t really see how to state the separation property precisely without introducing first-order formulas either. Do you have an alternative in mind?

No; that’s not something I’ve thought through.

Posted by: Tom Leinster on January 4, 2013 11:56 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This is running two things together. We have little theories, that we try to prove theorems about. Then we have a big universe of possible models. How do we show that a theory is consistent? The easiest way is construct a model. How do we show that something is not a theorem of the theory? The easiest way is to write down a model where it’s not true.

I think somehow category theory has been attached to a philosophical agenda that it only loosely requires. The real split is between constructive and non-constructive mathematics. Constructively, you’re forced to rely on inductively analyzing syntax, where an internal, structural approach makes sense. In non-constructive mathematics, not only are you are not required to work internally, you are better off not trying too hard. It’s proof theory versus model theory. Sometimes proof theory is all you have available, but model theory is easier.

How do you prove that something is not a consequence of the axioms for a Heyting algebra? The easiest way is to construct a model in terms of open sets where it doesn’t hold. How do you prove that there exists a Grothendieck topos that doesn’t have points? You construct an explicit model that doesn’t have points.

It’s telling that people who actually work with sheaves in a non-constructive setting almost never work internally; they just build the models they want and prove theorems about the models. One of the striking features of how (infinity, 1)-category has developed is just how often theorems are proven by working with an explicit class of models, such as topological categories or weak Kan complexes, and showing it for that model.

For applications in non-constructive mathematics, the structuralist viewpoint makes category theory harder to learn, harder to teach, and has slowed down how quickly category-theoretic ideas have diffused into the rest of mathematics. To be a mathematician, you must learn that in many settings you are only interested in objects up to isomorphism, but that’s certainly learnable in a big non-structuralist theory like ZFC, which also teaches you how to think non-structurally and build models extrinsic to your theories.

Basic category theory is an elementary subject, easier to understand than undergraduate complex analysis. But since it’s become linked to this structuralist philosophical stance, the stance and the mathematics get taught together. If you dropped the stance, you could teach the subject quicker, and to a broader audience.

Posted by: Walt on January 5, 2013 12:18 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I have no disagreement with that you say about models, except that I don’t think ‘constructive’ is really the right place to draw the line, since model constructions are also very useful in constructive mathematics (even if not all constructive mathematicians are aware of it). Non-Boolean sheaf toposes, realizability models, and gluing constructions come immediately to mind.

Anyway, I’m not sure what point you meant to make by bringing in syntax vs semantics: I was specifically only talking about models that we care about in their own right, rather than as metatheoretic tools. The syntax/semantics split is completely orthogonal to the structural/material one.

It’s telling that…

It certainly tells us something, but I think one thing it tells us is that sheaf theorists sometimes work harder than they need to because they don’t know the general tools that are available. They are hardly unique in this, of course, and there’s no shame in it; it’s just the way things happen. With (,1)(\infty,1)-categories, the problem is even more basic: so far, essentially all we have are particular explicit models, so it’s no surprise that people prove things by working with the models.

Moreover, it’s a fair point that when the tools are hard to learn, people won’t feel it’s worth their while to learn them, preferring to do the hard work by hand instead. But that’s what Tom’s paper is trying to remedy: making the entry to these tools easier. There was a time when calculus was an esoteric discipline understood by only a few; today most universities teach it to a large fraction of freshmen. There’s no such thing as a tool that is intrinsically too hard to ever be worth learning: as the problems people want to solve grow in difficulty and complexity, they naturally become more open to more powerful, but harder-to-learn, machinery. And, of course, there’s inertia. And, sometimes, personality conflicts, and yes, misguided insistence on philosophy. So at the end of the day, I think the real reason to teach ETCS is not a philosophical one, but a practical one. However, in order to learn it, you have to come to grips with thinking of sets in a different way, and for an audience not already familiar with the generalizations and applications, some philosophy can be useful — as long as the audience is willing to approach it with an open mind.

Posted by: Mike Shulman on January 5, 2013 7:35 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I’m afraid that I recognize hardly anything of Walt’s last post here.

I think somehow category theory has been attached to a philosophical agenda that it only loosely requires.

For applications in non-constructive mathematics, the structuralist viewpoint makes category theory harder to learn, harder to teach, and has slowed down how quickly category-theoretic ideas have diffused into the rest of mathematics.

Basic category theory is an elementary subject… [but] since it’s become linked to this structuralist philosophical stance, the stance and the mathematics get taught together.

I just don’t understand what this is talking about. It might help if Walt could produce some concrete examples of this alleged linking and this alleged hampering effect. Except for books like Sets for Mathematics with avowed concerns about how to do set theory or type theory from a categorical point of view, I don’t know of texts on category theory which push such an agenda.

When I write mathematics, say if I write out a proof in elementary real analysis or in algebra, worrying about whether I’m doing structural or material mathematics is usually the farthest thing from my mind. I imagine the same is true of Walt. On the other hand, such proofs never have assertions of the form 1π1 \in \pi; why would they? I can’t imagine such assertions (on the structure of the membership trees) come up in Walt’s proofs either, whether he is teaching properties of the Gamma function or that a PID is a UFD. And I’ll bet if I look up a proof of his in some journal, what I’d see would be perfectly sensible as perfectly structural mathematics. Being a natural mode in which to write proofs, how could it be so difficult to learn and use? It’s a mode of presentation that we quite naturally and un-self-consciously teach our students and use ourselves.

Constructively, you’re forced to rely on inductively analyzing syntax, where an internal, structural approach makes sense. In non-constructive mathematics, not only are you are not required to work internally, you are better off not trying too hard. It’s proof theory versus model theory. Sometimes proof theory is all you have available, but model theory is easier.

It’s telling that people who actually work with sheaves in a non-constructive setting almost never work internally; they just build the models they want and prove theorems about the models.

I don’t really recognize what Walt is saying here either. People like Andrej Bauer or Paul Taylor who have strong involvements with constructive mathematics consider models all the time. For example, recently at the Café, when we were discussing the proof of Zorn’s lemma, there was reference made to a paper of his that shows that the Bourbaki-Witt theorem cannot be proved constructively. He did this by examining examples in the effective topos: exactly a models-based approach. Quite sensible, obviously. How is this manifesting the divide between “constructive mathematics” (which is allegedly forced to rely on an inductive syntactic analysis) and “non-constructive mathematics”?

Here’s another example. There’s a theorem in constructive mathematics about the initial topos, which category theorists express by saying that the terminal object 11 is projective and connected (which has implications for constructive proofs). Originally, this was proven by an inductive syntactic analysis. But Freyd gave a beautifully simplified model-theoretic proof based on a gluing or sconing construction. What is notable is that a model was built not to provide a counterexample, but to prove a positive statement about constructive proofs.

Posted by: Todd Trimble on January 5, 2013 3:15 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I was trying to pre-concede an objection to my point about the centrality of constructing models, which is that in constructive settings sometimes you can’t construct a model, and you need to induct on syntax. Then working internally is important.

My point – which is strengthened by the examples from constructive mathematics – is that we have a tool of immense power that we use frequently. That tool is to take a theory, and construct models of it in a bigger theory. These models have all kinds of irrelevant features that are meaningless from the point of view of the original theory. In other words, we go outside what’s permitted us by the original structure. We work externally, rather than internally. Mathematicians have to think structurally, sometimes, and non-structurally, sometimes. Collectively, we’re good at both because we learn how to think both categorically and set-theoretically.

The rest of my comment is probably a distraction from this point, but as a matter of personal experience, I found category theory hard to learn until I started ignoring all advice on how to think categorically, and rather to think “what does this look for ordinary sets with with operations defined upon them.” Literally, within several months of adopting thing point of view, I rediscovered the idea of essentially algebraic categories, the fact that set models of limit sketches and essentially algebraic categories are the same thing, and the syntactic approach to locally presentable categories in chapter 5 of Ademek and Rosicky. (The idea of “compact object” never occurred to me, even though it’s pretty natural from this point of view.) Now, I know from long experience that I’m not particularly clever as mathematicians go – if you pointed a gun to my head and told me to prove the Sylow theorem off the top of my head or you’ll shoot, you better have bullets in the gun because you’re going to be using them. It’s just that it’s easy to make stuff out of sets. You just sling some stuff together until you build whatever you want. Sets are the marzipan of mathematics.

Posted by: Walt on January 6, 2013 10:09 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I apologize for the intrusion in the discussion but I find interesting and I wanted to express my personal opinion.

Let me introduce myself, I’m just a student so I’m not a expert and maybe I’ve mistaken the whole thing but it seems to me that here the discussion is about to different topic:
the first one is which one between ZFC and ETCS (or SEAR) is more suited for pedagogical purpose;
the second one is about which one of the two said theories should serve as a better foundation for mathematics.

Let me try to address this two topic.

For the first one, I’ve to admit that in my mind sets must be composed of elements (meaning that a set is an object which has a relation with other objects which are called its element). I think I’m not the only one with this idea of set, and if I understand correctly this is also Walt’s point of view. ETCS consider sets in a very different way, indeed we recover elements of a set just as arrows (i.e. function) from the terminal set into the considered set, and I don’t know how much this idea can see intuitive.
Anyway, as many have already pointed out ZFC has some problem too, indeed I belive that the fact that 2 has elements is as much intuitive as considering an element as a function from a terminal set.
A way to avoid this problem is clearly consider ZFC with atoms which made the theory more “intuitive”, but leave (from my point of view) some problem unsolver: for instance the definition of ordered pair as a set of a particular kind is not so intuitive, indeed there are many possible equivalent defintion. Indeed SEAR seems to me to be more intuive solving a lot of truble via “universal construction”, for instance an ordered pair in SEAR it’s just an element of a cartesian product, this implies that it’s just an object that have a certain relation with two other objects and just with those two, meaning that it’s an object that is entirely determinated by two elements (its coordinates), which captures exactly my intuitive concept of ordered pair. About what Mr.Leinster said above about the problem of first order sentences, this is just a tecnical problem which ZFC have too, but anyway it could be avoided in a intuitive presentation of SEAR if one substitute first order formula with the word property (avoiding the tecnicalities).

I think too the ETCS is not as much intuitive theory of set, anyway it serves an important pedagocial purpouse: it teach to think in arrow theoretic terms in a familiar contexts, that of sets.
This is very important, when I start learing some enriched category theory I’ve get many times stuck trying to understand theorems and proof in this subject, I’ve solved this problems when I started to think how this result were prove in the case of set, made some arrow theoretic abstraction (substituting application of function to point with composition with evaluation morphism etcetc) and use that argument in the more general context of a symmetric monoidal category.
So a really important reason to look at ETCS is that it allows to get familiar with a form of abstraction that help to generalize easily a lot of theorems true for sets to order context.

About the fundational issues, for what I get from the first comment above it seems to me that ETCS (with some minor correction) and ZFC are bi-interpretable and so are logically equivalent, so they can serve both as fundational theories, and this (at least if I get it right) is not a personal opinion just a mathematical theorem.

p.s.: I really want to compliments with Mr.Leinster, I really enjoyed it’s paper and it’s really useful to get the arrow theoretic (i.e. categorical) view of sets and functions (which as I consider fundamental for a lot of reason, some of which I’ve reported above).

Posted by: Giorgio Mossa on January 6, 2013 2:38 PM | Permalink | Reply to this

Re: Rethinking Set Theory

The branches in the comment tree are getting skinnier and skinnier, so I’ll reply as if to my own post, but it’s really to your last post, Walt (here, as probably goes without saying, but just in case).

My point – which is strengthened by the examples from constructive mathematics – is that we have a tool of immense power that we use frequently. That tool is to take a theory, and construct models of it in a bigger theory. These models have all kinds of irrelevant features that are meaningless from the point of view of the original theory. In other words, we go outside what’s permitted us by the original structure. We work externally, rather than internally. Mathematicians have to think structurally, sometimes, and non-structurally, sometimes. Collectively, we’re good at both because we learn how to think both categorically and set-theoretically.

It sounds like you and I have very different pictures of what “structural mathematics” means (but I’m glad for your last comment because it brought out what you were thinking about). My reaction to what I quoted could be put like this (in terms which might be anathematic to you, but I’m going anyway): interpreting a theory in a model is innately structural, because a theory is a model (a freely generated model) and an interpretation of a theory in a model is thereby a homomorphism of models. So to think structurally doesn’t mean we confine ourselves to the free model! (And so I want to say, “gee, where did you get that idea?”)

A simple example of this is where a model of the theory of groups is a product-preserving functor from the theory (the Lawvere algebraic theory, comprising the syntactic terms = elements of free groups) to, say, the category SetSet. The relevant context for algebraic theories and their models is thus the 2-category of categories with products, and product-preserving functors.

So how do I think of “structural mathematics”? If I had to sum it up in an aphorism, I’d say that in mathematics, Form is Substance. That aphorism is of course not original with me, and there have been many fine essays that spin out the meaning and consequences of that conception, but there it is.

As for the rest: great! We all learn mathematics according to our personal lights. But it sounds like either you got bad advice or you misunderstood some advice, because naturally just about the first thing a good student of category theory should do with a new concept is hold it up against SetSet (or AbAb, or whatever) to see what it means. And then go on to contemplate the same concept against a panoply of other examples. (Somewhere in this thread you said something about ETCS as trying to do set theory without elements, and although you didn’t say this yourself, a lot of people have this idea that category theorists “don’t like elements”, which is just a wrong idea that people should jettison!)

Posted by: Todd Trimble on January 6, 2013 12:29 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Todd wrote:

a lot of people have this idea that category theorists “don’t like elements”, which is just a wrong idea that people should jettison!

I’m completely with you, Todd, but I can see how it happened. If you leaf through Categories for the Working Mathematician, you’ll see various places where Mac Lane emphasizes that to frame a construction categorically is to frame it without elements. For instance, it’s there in the introduction where he says this about the group axioms, it’s there when he does the diagram lemmas for abelian categories, and it’s there on the page I have in front of me now (19):

In categorical treatments many properties ordinarily formulated by means of elements (elements of a set or of a group) are instead formulated in terms of arrows. […] We now formulate a few more instances of such methods of “doing without elements”.

I don’t exactly dispute what Mac Lane has written, but if “doing without elements” is to be read as a slogan for category theory, I think it’s misleading.

(It’s plain wrong if you take “element” to mean “generalized element”, but I’m certain Mac Lane wasn’t doing so. Maybe that terminology wasn’t even around then.)

Posted by: Tom Leinster on January 6, 2013 10:19 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I’ll borrow your idea, Todd, and reply at the same indentation level.

I think that at the level of generality you are talking about, “structural” mathematics is not the possession of any one philosophical school, but the joint heritage of all mathematicians, and has been since at least Hilbert’s geometry book, if not before. ZFC is perfectly structural, from this point of view.

I’m going to think aloud with an example, to try to make the point I’d like to make about how the “structural” viewpoint and category viewpoint are not necessarily the same. In universal algebra, it frequently happens that we have a nice theory that simple to axiomatize, but when we forget part of the structure, it becomes much more difficult. An example is the class of (non-commutative) rings that can be embedded into division rings, or special Jordan algebras (ones that can be embedded into rings by (xy + yx)/2). In both these cases, you can work out a very-complicated set of quasi-identities that describe the class of objects you care about. Or you can just work in the bigger class, and apply the forgetful functor as necessary. In either case, we get a category, so from the point of view of category theory it doesn’t matter. From the point of view of structuralism, the first one is better, because it’s internal. There’s no irrelevant fluff. This is exactly the same as the analogy between ETCS and bounded Zermelo with choice. There’s fluff, like a global membership operation, that we can just forget. In either case, the category of sets is the same, but structurally one is “better” than the other.

On the learning category theory viewpoint, I mean something much broader than just “Look, abelian groups are an example of an epireflective subcategory of groups!” There is a pervasive set-flavored viewpoint that goes a long way to explain the structure of cocomplete categories, one that makes many results entirely natural. I don’t think this is a revolutionary viewpoint, and everything you can see from this point of view is probably already in the literature, but it’s a viewpoint that makes it all easy to learn. But I’m sure everyone on this thread is sick of my opinions at this point, so I’ll leave at that – a series of vague yet implausible claims – until another day.

Posted by: Walt on January 7, 2013 4:54 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Joachim wrote:

…most extraordinary…

…Why on Earth…

Note to Tom: I apologise for polluting the thread with this tone, I know you don’t like it.

It’s true, I’d prefer to keep the tone and language rather gentler.

Since I know you, I can easily imagine you saying your comment out loud in a friendly way, with a bit of a smile on your face. (People who don’t know Joachim should imagine this friendly scenario too!) So, knowing you, I know it’s not meant in an inflammatory way. But I confess, I might have edited your comment or asked you to re-word it if it had been someone I didn’t know.

(Some people might wonder why I’m being quite so careful about this, since we haven’t come close to any kind of unpleasantness. As I said in the post, there’s some unfortunate history here, which is probably best not discussed on this thread. It’s not a secret, it’s just that it would probably derail our present fruitful discussions.)

Posted by: Tom Leinster on December 27, 2012 9:48 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Of course Joachim should know (and so should Walt, and all students of foundations) that xx itself doesn’t know what xx\in{} is, nor what x{}\in x is; that’s the job of \in itself.

Posted by: Jesse McKeown on December 27, 2012 3:15 PM | Permalink | Reply to this

Re: Rethinking Set Theory

A quick correction: ETCS does refer to elements, all the time. Tom’s axiom 4 is all about elements. The difference is only that those elements have no identity independent of their being elements of the set under consideration.

Posted by: Mike Shulman on December 27, 2012 6:31 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I appreciate Todd’s summary of a pro-material-set-theory point of view, especially as I suspect it’s not precisely his own point of view.

I want to make three points: one each about ETCS, ZFC, and ZFC with atoms/urelements.

First, ETCS. Mike wrote:

In ETCS, however, there is no such thing as ‘forming a set of’ anything.

While I know what Mike means, I think this could easily be misleading to someone who isn’t familiar with categorical set theory. For example, in ETCS, we can form the set EE of even integers. Or, we can form the set Y XY^X of functions from XX to YY.

It’s true: when we say that the elements of EE are the even integers, the meaning is slightly different from what it would be in ZFC. (It means that EE comes equipped with an injection i:Ei\colon E \to \mathbb{Z} such that for nn \in \mathbb{Z}, we have niEnn \in i E \iff n is even.) But still, in informal usage we talk about ‘forming the set of such-and-such’ all the time in ETCS. Maybe it’s like an evolutionary biologist saying ‘the woodpecker has a sharp beak so that it can make holes in trees’: in strict evolutionary terms that’s nonsense, but everyone knows what’s really meant.

Second, ZFC. Walt wrote:

I’m forming the set {{Mike, structural set theory}}

Walt didn’t claim that this set can be formed in ZFC. But perhaps it’s worth pointing out that it can’t be – at least, not unless Mike is a set (which I expect he’d deny). That’s just because in ZFC, elements of sets are always sets.

Todd mentioned the passage from

  • the naive idea that a set is a collection of ‘things’ of any kind you like

to

  • axiomatic ZFC.

This passage seems problematic, for exactly the reason just mentioned. In ZFC, the only elements that sets are allowed to have are other sets. Sets containing Mike, apples, badgers, etc., as in the naive idea, are specifically not allowed.

Which brings us to…

Third, ZFC with atoms. It’s interesting that this theory has come up so often in this discussion (and it also came up after a seminar I gave on this stuff). Adding in atoms seems to be a way of bringing ZFC’s usage of ‘set’ a bit closer to the ordinary mathematical usage of ‘set’, answering some of the criticisms of ZFC made in the first couple of pages of my draft.

It’s even more interesting, then, that ZFC-with-atoms is not the theory that became the standard. (That was, of course, ZFC.) Moreover, as far as I can tell, set theorists almost exclusively study theories of ‘pure’ sets: those whose elements are always sets themselves.

I don’t know how well ZFC with atoms really does reflect how mathematicians actually use sets. (I’m not sure I’ve ever seen the axioms, which is telling in itself.) Mike voiced some doubts earlier.

Posted by: Tom Leinster on December 27, 2012 10:50 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks for clarifying what I meant, Tom. On the other hand, I do think it’s not unreasonable to object to this aspect: that the familiar notion of ‘forming a set of X’ is technically an abuse of language in ETCS. (Of course, I also think the advantages of ETCS over material set theories outweigh this and other idiosyncracies.)

Also, while I am indeed not a set, I am also not an atom. In fact, I doubt I am any sort of thing that would be admitted as an element of a set in any mathematical theory of sets. (-:

Posted by: Mike Shulman on December 28, 2012 6:52 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Formalizing how mathematicians use atoms is a very interesting question, one that I think about sometimes. The details for ZFC + atoms is in Jech’s set theory book, but I think for what you’re after, it’s disappointing. Set theorists are interested in sets, so once you prove that ZFC + there is a class of atoms is equiconsistent with plain ZFC, then set theorists lose interest.

ZFC + atoms is incomplete in that it doesn’t tell you anything about the atoms. You would add additional axioms for whatever atoms you want. I think it would be very interesting to work out a set of axioms that reflected mathematical practice. The problem is that this is obviously somewhat subjective, and depends on the author, so you would want to describe the kinds of axioms that are allowed. For example, one author would want N to be a subset of C, while another might want them to be disjoint, and a third might want to leave it unspecified. What really matters is which kinds of axioms are equiconsistent with ZFC, or whatever your preferred set theory is.

I would take Mike’s point about ad-hocness to be rather about how ad-hoc a model of ZFC + “my atoms” is. What you really want is the first order theory of ZFC + “my atoms”. The only importance of the model is that it shows you that it’s a consistent extension.

Posted by: Walt on December 28, 2012 4:23 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Do you have some proposed non-ad-hoc way of working with atoms inside some first-order theory?

Posted by: Mike Shulman on December 31, 2012 5:25 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I have multiple conflicting proposals that are fighting it out inside my head. It depends somewhat on the goal.

Let’s set as a goal the idea of only proving statements that mathematicians would generally agree are true. If we go with Tom’s idea of making the list of primitive concepts as short as possible, then all we need is ZFC plus a class of otherwise undistinguished atoms.

When we say that there is a natural numbers object, then we’re saying there exists a set with a certain function defined on it, as you well know. Are the elements of that set atoms? Dunno, depends on the choice of set. We can’t prove that 010 \in 1 for an arbitrary natural numbers object.

Even for things where we normally have a canonical ZFC construction, such as power set, if you take the categorical definition of a power set object, it’s an object that’s only unique up to isomorphism. Could the elements of that set be atoms? Again, it depends on the choice of set, which is only unique up to isomorphism.

In general, from the point of view of category theory you are only asserting the existence of a set with specified operations. ZFC plus a class of atoms can’t prove that set has any definite elements, or whether or not they are atoms. In that sense, it only proves the theorems that mathematicians would expect.

I think if you laid this idea out carefully, you could prove a correspondence between ETCS-like theories, and Zermelo-like set theories with atoms, in such a way that the Zermelo-like theory is a conservative extension of the ETCS-like theory.

(You could also assert the existence of atoms with definite equality properties. I have somewhat vaguer ideas of what you’d want to allow along those lines.)

Posted by: Walt on December 31, 2012 10:32 AM | Permalink | Reply to this

Re: Rethinking Set Theory

It sounds to me like you’re proposing that we start from a model of ZFC+atoms, build the corresponding model of ETCS+R, and then work in that model. In that case, why bother with ZFC+atoms; why not just assume ETCS+R to start from?

Posted by: Mike Shulman on January 3, 2013 6:43 PM | Permalink | Reply to this

Re: Rethinking Set Theory

But this has to be a matter of taste, right? You could argue the other way: you have a perfectly good model in ZFC + atoms. You can cut it down for ETCS, but then you have to give up the ability to form concrete sets of things. Why not just work with ZFC + atoms?

Anyway, what I had in mind was that there should be some small Zermelo-type set theory that is a conservative extension of ETCS. Likewise, there should be an ETCS plus axioms that has ZFC as a conservative extension.

The advantage of the conservative extension is that you recover the intuitive notion that if you know how to compare a certain class of objects for equality, then you know how to compare sets of those objects. In Haskell terms, if type X is an instance of typeclass Eq, then so is Set X.

Posted by: Walt on January 3, 2013 10:01 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Ah, I think I see what you’re getting at: use an ETCS-like definition of structures, but then allow material-sets of elements of those structures, rather than the way ETCS represents subsets as injections. You may be interested in the blog post I’m currently writing. But it also sounds like maybe you’re looking for the same sort of thing that Francois is?

Posted by: Mike Shulman on January 4, 2013 5:18 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Also, what are the atoms really buying you in this approach? ZFC can’t prove that 010\in 1 for an arbitrary NNO, whether or not there are any atoms.

On the other hand, I think your approach can prove that “010\in 1 or 010\notin 1”, which I’m not sure mathematicians would generally agree to be true. I would prefer to call the statement 010\in 1 nonsensical.

Posted by: Mike Shulman on January 3, 2013 6:57 PM | Permalink | Reply to this

Re: Rethinking Set Theory

The atoms rules out accidental theorems like x(x0x1)\exists x (x \in 0 \vee x \in 1). The truth of all tautologies is a general property of first-order logic, which is untyped. Presumably you think comparing a set S and a function f for equality is also meaningless, but in the first-order formulation of ETCS, the statement S=fSfS = f \vee S \neq f is also true.

Anyway, I’m not sure there’s anything like universal consensus of what’s meaningless or not. If two functions have different codomains, can you compare them? If 2 is an integer, and 2.5 is a real, can you compare them? (I guess in ETCS you’d have to code these as two arrows from the one-element set, with different codomains.) There’s a fussy level of detail over when equality or membership, or any predicate is meaningful, which people can have strong opinions on, but where agreement is not actually needed. You can sidestep the issue by simply ensuring that atomic statements that are arguably meaningless are not assigned a definite truth value across models. Then you can say that you require the variables in equality to be well-typed to be comparable, I can say that I don’t care, and we can still communicate.

Also, consider the set theorists natural numbers object, where 010 \in 1 is not only not meaningless, but a theorem. You are forbidding the construction of such an object, even though it is a perfectly good natural numbers object, that satisfies all of the theorems of a natural numbers object. To what end?

Posted by: Walt on January 3, 2013 10:33 PM | Permalink | Reply to this

Re: Rethinking Set Theory

First-order logic doesn’t have to be untyped. It’s much more natural to formulate ETCS in first-order logic with two types for objects and arrows, in which case comparing a set for equality with a function is indeed meaningless. Even more natural is to use a dependently typed logic, in which case comparing functions with different domains or codomains is also meaningless.

In particular, to compare the natural number 2 with the real number 2.5, there needs to be an understood injection from the naturals to the reals. But since there’s a canonical such injection, we can ‘declare it as an implicit coercion’ (which a mathematician usually glosses as ‘by abuse of notation’) so that we don’t need to write it every time. This is just as true in ZFC, where 2={0,1}2=\{0,1\} while 2.5 is either a Dedkind cut or an equivalence class of Cauchy sequences or something (unless we follow Bourbaki in doing violence to mathematics by cutting and pasting).

You are forbidding the construction of such an object…

I think that as long as you think about ETCS as obtained from ZFC by ‘forbidding’ certain things, you aren’t going to like it, and you’ve missed the point. No one likes to be forbidden to do anything! The point is that ETCS is based on a different conception of ‘set’, according to which those thing you keep wanting to do are meaningless.

Posted by: Mike Shulman on January 4, 2013 5:37 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I don’t understand what you mean by “meaningless”, then. allxyz3\exists \all x y \in \in z \neq 3 is meaningless. 010 \in 1 may or many not be meaningless depending on the context.

The cost of the approach here is that you give up perfectly meaningful statements that everyone understands, or at best you have to treat them as abuses of notation. The gain is that you no longer have to regard tautologies evaluated at meaningless statements as true.

Posted by: Walt on January 4, 2013 10:58 PM | Permalink | Reply to this

Re: Rethinking Set Theory

According to the conception of ‘set’ that I consider ETCS to be based on, it is only meaningful to ask whether aba\in b if bb is a set. Since 1 is not a set, it is not meaningful to ask whether 010\in 1. It’d be like asking whether happiness can be purple: it’s a type error.

Obviously, there is a choice to be made in drawing the line between ‘meaningless’ and ‘false’. But I think there are good reasons for putting type errors on the ‘meaningless’ side of the ledger.

Posted by: Mike Shulman on January 5, 2013 6:57 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I don’t like the hard line that certain things are meaningless, simply because this depends on the setting. I don’t object to the idea of saying that an expression is, for your current purposes, well-typed, since this just means you say nothing about non-well-typed expressions. I would say not “meaningless”, but rather “does not have an intended meaning”. There are expressions, such as 010 \in 1 that do not have an intended meaning. If they have a meaning in a certain setting, then so be it.

Let me use a perhaps-stretched analogy. There are two ways you can think of a free group on nn generators. One is as a perfectly concrete group, where you know for a fact that xx 2x \neq x^2. Another way is that it satisfies a universal property, i.e. it’s the “most general” group with nn generators. If you never use inequalities, then any theorem you prove about the free group is automatically a theorem about any group with nn generators.

The same thing applies here. You rarely prove theorems of the form “This term is meaningless therefore X”. (I don’t actually know any examples of a theorem of this sort, though I’m sure there is some, somewhere.) Most of the time, the only thing that matters is the subset of expressions that are well-typed, and that they be assigned the correct meaning. Whether or not they have other meanings outside your setting doesn’t matter one way or the other. So we get that all well-typed theorems about the natural numbers are theorems about the set theorists’ natural numbers, for free.

On a basically unrelated note, I thought of a simple solution to your objection that 010 \in 1 is meaningless. We have a Set(X) predicate that’s true when X is a set. We introduce bounded quantifiers for “for all sets X” and “there exists sets x” (which we can do in terms of ordinary quantifiers and the Set(x) predicate). We say that an \in is well-typed if whenever XYX \in Y occurs in a formula, then X must occur in a bounded quantifier. If you want to encode a more complicated typing relation, then you could refine the kinds of bounded quantifiers. (There must be a fairly general dictionary between types and bounded quantifiers, I would think, which this example and bounded Zermelo are just special cases.)

Posted by: Walt on January 6, 2013 11:57 AM | Permalink | Reply to this

Re: Rethinking Set Theory

At this point I feel we are just arguing about words. I qualified my statement about meaninglessness with “according to the conception of set…”. When working inside a typed system, ill-typed expressions are meaningless, in the sense that the system does not assign to them any meaning. When interpreting that typed system inside some meta-system, there might indeed be a consistent way to extend the meaning of well-typed expressions to assign meaning to some ill-typed expressions as well. But when working inside the system, rather than building models of it, I think the word “meaningless” is perfectly correct.

You rarely prove theorems of the form “This term is meaningless therefore X”.

In fact, if “meaningless” means “ill-typed”, then you cannot possibly prove such a theorem, because typing judgments are judgments, not propositions, and as such cannot be the hypothesis of a theorem. (-:

…We say that an ∈ is well-typed if whenever X∈Y occurs in a formula, then Y must occur in a bounded quantifier…

Yes, that’s a reasonable way to go about constructing a model of the typed sort of system that I prefer inside the untyped sort of system that you prefer. But there’s no particular reason that a typed system should be regarded as constructed inside an untyped system; it might just as well be the other way ‘round.

Posted by: Mike Shulman on January 7, 2013 6:20 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think the point of about judgements is an important point that often gets elided in arguments about type theory, to the disadvantage of making a positive case for type theory. Type theory itself doesn’t prevent you from doing anything. It’s just a set of tools to tell you when a formula is well-typed. It’s open-ended. Tomorrow we might discover that more formulas are well-typed, and that the types make intuitive sense. This process is particularly clear in typed programming languges, where the type systems get increasingly expressive.

The arugment is probably over something even more trivial than words, sadly. I’m fine with embedding untyped systems inside typed systems. I like type theory. I like set theory, topos theory, category theory. What I don’t like is the “versus” arguments that plague the discussion of foundations, like “set theory versus type theory”, or “set theory versus category theory”. It leads to arguments about topics that would seem odd in any other context. For example, how much time do people spend arguing about whether the Dedekind cut definition or the Cauchy sequence construction of the reals is better? Better for what? If I ever met someone who says the Dedekind cut definition is better, I would probably end up taking the other side.

I think is particularly ironic in the category theoretic setting. If I understand the situation correctly, then in the appropriate sense, ETCS and bounded Zermelo with choice are isomorphic. ETCS plus replacement and ZFC are isomorphic. In any other setting than foundations, it would be immediately clear that there’s nothing to argue about. And yet here we are.

Posted by: Walt on January 7, 2013 9:13 AM | Permalink | Reply to this

Re: Rethinking Set Theory

The reason there are so many argues of the form “versus” is that foundation is a language on which you build other languages. Sort of how the way to use Common Lisp (for big enough projects) is to write your own programming language.

Languages dictates how we think. If you language has no word for “sadness” it is because no one using the language needed to express “sadness”. You can always try and translate a word into a phrase elaborating and explaining it. But the fact that a word is missing from the vocabulary means something. You see this often enough when you run into things which “don’t translate well from/into English” (if you’re familiar enough with at least one more language other than English).

So he who controls the spice, controls the universe.

If you teach students, from zero, to think in terms of sets and membership then the majority of them will. If you teach them to think in terms of arrows and functions, or if you teach them to think in terms of types… they will.

These arguments, I feel, are about what sort of approach should people take towards mathematics. Certainly the fact that rigor took over has changed the way people write and think about mathematics. Surely it can happen again if we try.

But no one in these arguments does that for this particular purpose, at least not knowingly. If you think about it, though, then all those discussions about foundational mathematics are ultimately around how do we approach mathematics “naturally”, and which is the “more correct way” (none of the above is the real answer to that, regardless to the contents of the above).

So we argue and bicker and we end up with name calling, and deepening the fragmentation in mathematical terminology, language and notation. I was writing and paper in which I proved some choice principle coming from algebraic set theory is independent of ZF (sans large cardinals). I was going through several papers about this principle and its relatives and I could not, for the life of me, understand it. I did understand the “set theory translation” I was given at first, but I didn’t know where to refer the reader in case they wanted to search for a published reference.

This is a sign of how deep there is a fragmentation between the two fields, and both would be called by their practitioners “set theory”. Both would be considered foundational, and if we augment one (CZF) we have the other too (ZF).

After this heartbreaking story about the fight between the rebels and the empire (or whatever, I’m not going to pick sides because both sides are cool), I will admit to hate these discussions as well. I feel they are interesting and we can learn a lot from them, but at some point they just end up with people writing stories about languages and comparing set theorists to Star Wars.

I agree that mathematically this is a pointless argument since ETCS+R is “isomorphic” to ZFC in a very good sense, but I understand why people are passionate about these things. They want to be able to communicate with others without learning a new language, and they want others to speak in their better-and-improved language (be it set theory, type theory, etc.) so they could understand others as well.

What can you do, that’s life…

Posted by: Asaf Karagila on January 7, 2013 3:36 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Asaf, you seem to have a much more negative and adversarial view of this discussion than I do. I feel that it’s been very productive; I understand the “other side” better than I did before, and I think we’ve made some progress towards understanding the issues and building towards a resolution. My followup blog post about type theory is based on insights that I learned from this discussion, which have inclined me towards a more even-handed view of the structural and material approaches and their individual benefits and problems. Certainly there have been some frustrations, but that’s only natural when people with very different backgrounds are trying to compare and reconcile their viewpoints. Francois also seems to think that we made some significant progress.

ETCS plus replacement and ZFC are isomorphic

Well… there are a 2-category of models of ETCS+R and a category of models of ZFC which are equivalent. But to make that true, you have to choose the morphisms in those categories appropriately, and the two theories each also admit other notions of morphism that are different. In the world of ETCS we have logical functors and geometric morphisms, while in the world of ZFC we have inclusions of transitive models. Francois made the point in the comments to his post that the latter notion in ZFC makes it much easier to describe preservation of well-foundedness, while of course geometric morphisms make contact with topology, algebraic geometry, and all sorts of ideas from topos theory. So I really think there is mathematical content to the difference, as well as philosophy.

Posted by: Mike Shulman on January 7, 2013 6:57 PM | Permalink | Reply to this

Re: Rethinking Set Theory

A long time ago, in a thread far far away …

http://golem.ph.utexas.edu/category/2011/08/the_settheoretic_multiverse.html

Mike you say:

“Since models of ZFC are entirely first-order equivalent to models of ETCS + Replacement, the multiverse of models of ZFC might just as well be considered a multiverse of models of ETCS+R. The latter view, of course, has the advantage that we can consider functors and transformations between models of ETCS+R, making the multiverse into a 2-category.”

How does this compare to the comment you just made?

Are the ZFC and ETCS+R multiverses both 2-categories?

Posted by: Grapr on January 7, 2013 7:10 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Dear Mike,

I read your post and I may reply to it later or tomorrow. I will briefly say that I did not enjoy it as others did. Whether it is my discomfort with type theory, or maybe it’s all the recent discussions which made me extra sensitive to your words. I will re-read it a couple more times before making up my mind.

My comment was a reply to Walt, as an answer to the tangential question why do people keep going into these seemingly-pointless discussions. If we know that ETCS+R is equivalent to ZFC is a very strong sense, why does it matter which one is foundational? It matters, as I pointed out, from a philosophical point of view.

Those who “believe” in ETCS+R and those who believe in ZFC essentially “believe the same god”, but they practice this belief in a very different way.

I read several of the comments on this discussions, and when I first thought about writing a comment I realized that it might be better to blog about it, so I did. I’m engaged in a very interesting discussion with Todd over there. And I did learn a lot about the other side of foundations. I also learned a lot about the philosophy guiding type theory and structural set theory. At this point in my life, I find my philosophy very much in sync with that of ZF and very much not with that of type theory and structural set theory.

Not a single time I said that the discussion here, or over at Francois’ or in my own blog is useless or an exercise in futility. I am fully aware that this is the only actual way to try and develop a common foundational theory. But I think that the so-called quibble over which is a better foundational theory, ETCS+R or ZFC exactly stems from what I wrote in the previous comment. He who controls the spice controls the universe.

I will apologize if I am negative and adversarial to you. That was not my intent. My intention was to point out that the futile argument is actually very non-futile. Personally, I will continue to root for ZF as a foundational theory, because I believe it’s more than just fine. I believe that the type cast errors which people nitpick to are the wrong things to nitpick. Much like ZF will never prove its own consistency (unless it turns inconsistent), no foundational theory will be innocent of junk. And if it will, then it will probably be too weak to express what I feel is an adequate power for a foundational theory.

I could write more and more, but my point is essentially made. These discussions are not futile, and even after two theories have a very nice bi-interpretation there is still a point to decide which one is better to use as meta-theory. I will continue to hold this view, and probably for a long time, mostly because I have peculiar views about mathematics. But I have no choice about that.

Regards,

Asaf.

Posted by: Asaf Karagila on January 7, 2013 8:42 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks for clarifying! But I still think you have a more adversarial view of these discussions than I am happy with. I don’t agree that we have to decide which of them is “the best”; I think we should get used to the idea that each can be better for different purposes. Andrej Bauer had a nice post about this a little bit ago. Coming at it from that point of view, I think there is a lot less worry about who “controls the universe” — except for the unfortunate fact that at present, the universe is mostly controlled by ZFC, so that those of us who prefer to even sometimes use something different are made to feel like rebels! (-:

Posted by: Mike Shulman on January 8, 2013 4:34 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think the discussion with Francois has broadened my point of view since then. In that comment I mentioned the additional morphisms available on the ETCS side as an advantage; I think Francois has argued persuasively that there are also different additional morphisms available on the ZFC side, that are also useful for different things.

Posted by: Mike Shulman on January 7, 2013 10:00 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Sorry about the “me too”, but I agree with Mike’s view of the productivity of these discussions. Also, despite the fact that I might appear to have been crabby or adversarial here and there (at François’s blog and your blog too, Asaf), I’ve actually really enjoyed the discussions on a personal level, and have felt much more relaxed in conversation on these matters than at any time in the past.

All four blog posts (this, Mike’s most recent on type theory, François’s, and yours), plus some recent MathOverflow discussions, have definitely heightened my sensitivity to certain issues. Some of François’s comments on well-foundedness below his own post contain some of the most insightful criticisms of ETCS I’ve ever seen.

Posted by: Todd Trimble on January 7, 2013 7:54 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I am very glad to hear that you have enjoyed these discussions. I have enjoyed them as well.

To avoid repeating too much over my previous reply to Mike, let me summarize by saying that these discussions are not futile, as I commented.

They appear futile, and in some sense of course they are (it’s not like now people in PDE will say “Oh, fine! We’ll do mathematics like this.” all of a sudden), but these discussions are actually less about the mathematics and more about the philosophical approach towards mathematics.

Which are the more important parts, and which are less important. In ZFC we put emphasis on x,y,z and in ETCS the emphasis is put on u,v,w. These can be related or unrelated. But even if the foundation is proved to be essentially the same, it never is. It’s a different thought process and a different approach.

I’ll cut this here before writing another monograph. I will just add that much like you I have learned a lot about the approach categorists take towards set theory, and even mathematics in general.

Posted by: Asaf Karagila on January 7, 2013 9:52 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Evidently the revolution needs to begin at a much earlier age, if people are already being taught about ZF-style sets at age 10!

Posted by: Mike Shulman on December 22, 2012 9:31 PM | Permalink | Reply to this

Re: Rethinking Set Theory

The first sets that people learn are usually sets of some specific (and non-set) type of thing (such as real numbers), what I'd call concrete sets. You then make this naïve notion of set into the material (ZFC-style) notion by telling students that in modern mathematics, everything is encoded as a set, so that ultimately all sets are sets of sets (very heady stuff). Alternatively, you make this into the structural (ETCS-style) notion of set by telling students that each type of thing forms its own abstract set and one can consider subsets of any abstract set (but should not compare elements of two unrelated abstract sets, which is where this can get heady).

Posted by: Toby Bartels on December 23, 2012 12:35 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I don’t know of a programming curriculum (aimed at typical CS students) that starts with Haskell as a first programming course - I think the sheer number of abstract concepts that one has to absorb upfront is too much for all but the brightest of students. (But it would make an excellent second or third course.)

As it turns out, the Cambridge (and I think Edinburgh; so both of the recent academic affiliations of Tom) computer science curricula start with ML as the first programming language. I believe that Oxford starts with Haskell (ironic, since the GHC development team is in Cambridge…)

The belief is indeed exactly that dealing with the minutiae of machine and history dependent choices made in C/C++ is anti-pedagogical, where as the purity of structural recursion and algebraic types (which is to say, initial (viz. co-initial in Haskell) algebras with all their universal goodness) is much easier to reason about for practical applications.

It is, of course, an open question whether this belief is actually true.

Posted by: Gen Zhang on December 24, 2012 8:50 PM | Permalink | Reply to this

Re: Rethinking Set Theory

It is, of course, an open question whether this belief is actually true.

Some people’s experience suggests that it is.

Posted by: Mike Shulman on December 25, 2012 12:19 AM | Permalink | Reply to this

Re: Rethinking Set Theory

This is a wonderful piece, Tom. I enjoyed it a lot and I really appreciate that you took the time to write this. Although I am somewhat from the other side of the fence, I think that I do have some feedback that fits your criteria for admissibility.


I found one mathematical inaccuracy. In the last paragraph of the section titled ‘How strong are the axioms?’ you wrote that axioms 1-11 are equivalent to ZFC. This is incorrect, the two theories are equiconsistent and, in fact, biinterpretable, but not equivalent. Of course, the use of such a technical terms is not necessary; I suggest writing “interpretable in each other,” which has the advantage of conveying the actual nature of the relationship between the two theories.


I think that your brushing aside of replacement is overdone and perhaps a little misguided. I think replacement is lacking from ETCS. In fact, I think replacement is essential for ETCS to be considered as a robust foundational theory. In order for ETCS to be a serious foundation, it must accurately reflect the universe that mathematicians actually work in. In set theory, comprehension plays the most important part of that role. In its second-order formulation, it simply says that every subcollection of a set is a set. Thus, since nothing is missing, the formal sets do correspond to the intuitive sets we play with in everyday mathematics (provided we restrict out attention a little). Replacement is the obvious candidate to play the same role for ETCS since it is meant to capture the (second-order) idea that every mapping whose domain is a set is actually a function (in the internal sense). There is probably some work to be done in order to get the right (first-order) formulation, but it is a necessity if ETCS is intended to be used as a foundation for mathematics.


I am reluctant to mention the next item, since it can easily be perceived the wrong way and, if misinterpreted, could lead to the type of polemic you and I both want to avoid. I much prefer calling ETCS a theory of functions rather than a theory of sets. Functions are the primary citizens of ETCS, it is wonderful how easily elements and membership can be interpreted in ETCS but it is strange and perhaps misleading to give them center stage by calling ETCS a set theory. (Note that, by the same token, functions are merely interpreted in ZFC. In my opinion, it is a significant advantage of ETCS that this interpretation is much more complicated than the interpretation of sets in ETCS.) Think how less apologetic your piece would be if you did not need to explain that interpreting elements the way ETCS does is an acceptable thing to do and could instead present it as yet another neat thing you can do using functions. I’m sure you’re not inclined to do this change and I concede that I may be over thinking this but, from the perspective of someone who works with set theories all the time, it’s very difficult for me to use “set theory” to describe a theory that does not rest on an extensional membership relation and does not even have one as a formal part.


Finally, I really liked how you are presenting ETCS as a serious foundation that mathematicians are already unknowingly using (more or less). This is one of the most important arguments in favor of ETCS. The other strong point for ETCS is that it is a rigorous foundation that you can teach to very young mathematicians, and you also do a great job explaining that. Poor logicians like myself are likely to keep on using ZFC because of its many conveniences, but that’s fine since the bridge between ETCS and ZFC is well understood.

Posted by: François G. Dorais on December 18, 2012 9:02 AM | Permalink | Reply to this

Re: Rethinking Set Theory

the two theories are equiconsistent and, in fact, biinterpretable, but not equivalent.

They are equivalent in the following sense:

  • If you start from a model of ZFC, build a model of ETCS+R, and then build a model of ZFC from that, you obtain a model that is isomorphic to the one you started with.

  • If you start from a model of ETCS+R, build a model of ZFC, and then build a model of ETCS+R from that, you obtain a model that is an equivalent category to the one you started with.

What more would you ask for?

I think replacement is essential for ETCS to be considered as a robust foundational theory.

Tom makes a good argument in the paper that mathematicians almost never use replacement. But it sounds like you’re saying instead that mathematicians need separation and replacement in order to believe that a theory of sets “captures their intuitive notion of set”?

ETCS does, of course, include separation: you just have to prove it rather than taking it as an axiom. It’s a “bounded” separation by default, but it’s not hard to add an unbounded version if you want it. SEAR includes (unbounded) separation as a basic axiom, as well as a collection axiom. In this paper I considered the unbounded separation axiom for ETCS-like theories, and also what I think are the right “collection axiom” and “replacement axiom” in those formulations.

Posted by: Mike Shulman on December 18, 2012 12:57 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Hi Mike,

I was correcting the term that Tom used, not what he meant. What you wrote is (a strong form of) biinterpretability. Equivalence is stronger as it normally means that two axiomatizations have the same deductive closures. I don’t think Tom was using equivalence in this sense, but I think it’s best to avoid confusion.

Yes, that is what I am saying about the need for replacement. As it stands, I think ETCS is not sufficiently robust to be used as a foundation. With replacement, I think that it would be. At least, there would be a lot fewer “illegitimate” models.

Thanks for pointing out your paper and your detailed analysis of structural collection and replacement!

Posted by: François G. Dorais on December 18, 2012 2:24 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Equivalence is stronger as it normally means that two axiomatizations have the same deductive closures.

I’m not sure exactly what the technical language means here, but I don’t see how that could fail to be the case either, to whatever degree it makes sense. ZFC and ETCS+R are theories in different languages, so we can’t ask directly whether they prove “the same theorems”. But the equivalence of models that I described means that if a statement in the language of ETCS+R is provable from ZFC, when interpreted as a statement in the language of ZFC along the standard model construction, then it is also provable from ETCS+R, and vice versa in all possible ways. What sort of notion of “equivalence” is there that makes sense between ZFC and ETCS+R but isn’t true?

At least, there would be a lot fewer “illegitimate” models.

If you’ll forgive me, I am about to go on a rant (in the politest possible way, of course (-: ). Bear in mind that I have been dealing with (what I regard as) this same misconception among lots of other people as well recently, so this rant is not entirely directed at you (or at anyone in particular).

I don’t believe there is any such thing as an “illegitimate” model.

When you learn in your abstract algebra course that all the familiar laws of arithmetic apply not only to familiar things like real numbers and complex numbers, but also to elements of arbitrary fields, from pp-adic numbers to rational functions to finite fields to the surreal numbers, do you say “oh no, those models are illegitimate”?

I figure this has been the direction of mathematics ever since Bolyai and Lobachevsky discovered non-Euclidean geometry. Euclid thought he intended one model, but surprisingly, his axioms also applied to other models. And the other models are interesting! They are just as valid, give rise to just as deep mathematics (or deeper), and even turned out to be relevant to the physical world. So Euclid was right to avoid the parallel postulate as long as he could, because by doing so he proved his theorems in more generality. The same principle can be applied to the axiom of choice, the axiom of replacement, the law of excluded middle, etc.

I also figure this is the real message of Gödel’s Incompleteness Theorem. No formal system can completely describe a single model. There will always be lots and lots of models. Thinking that you have in your head some particular model that you are trying to axiomatize is a fool’s game: your intuitive picture can never be precise enough. And it’s self-defeating, because if you accept the fact that your axioms have lots of models, then you realize immediately that all of your theorems are more general than you thought they were.

And isn’t that a good thing? Isn’t mathematics all about looking at concrete things and finding abstract structures which apply more generally than in the original examples?

Posted by: Mike Shulman on December 19, 2012 7:38 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think another example, where the languages are the same, will illustrate better. ZF is biinterpretable with Aczel’s AFA (biinterpretable in just as strong a sense as ZFC and ETCS+R). However, ZF includes foundation and AFA refutes it, so they are not equivalent theories: you can’t take a textbook, replace ZF by AFA, and expect that nothing will go wrong (though that may happen more often than not). Equivalence is usually meant in a very strong sense, such as ZF + Zorn’s Lemma is equivalent to ZF + Wellordering Principle. Biinterpretability is an equivalence relation but, even if we forget about the customary meaning, “equivalence” (without qualification or explanation) is still too strong a word to use to describe this relation. Biinterpretability is subtle and it’s easy to fall into traps. (See this exchange on MO for an example of a subtle trap.)

I meant something specific by “illegitimate” but I didn’t explain, so the blame is on me for suggesting that some models are less interesting than others. (Since I spend large parts of my days concocting peculiar models of set theory and arithmetic, that’s certainly not what I meant.) Part of the role of a foundational theory is to standardize communication. ZFC does that very well. There are many models of ZFC, all of which are interesting, but the core is very standard. You may believe in V=L and I may believe in supercompact cardinals or that 2 0= 172^{\aleph_0} = \aleph_{17}, we can’t live in the same ZFC universe but that doesn’t stop us from talking about mathematics in a meaningful way since our disagreements are all very far from core mathematics. In fact, even if you don’t really believe in ZFC or are agnostic about it, we can still have meaningful conversation because ZFC has a very robust core. ETCS is not that robust, it has lots of models that differ in ways that are too close to home.

For a foundation to be useful for everyday mathematics, we need to be able to (explicitly or tacitly) agree upon it, then have a meaningful discussion without ever mentioning our foundation again, except in very rare cases. How does this happen? Well, we need to make sure that our foundation does accurately capture everything we normally do. In the case of ZFC: some of us have done that explicitly by carefully studying the axioms; some of us are taking that on faith; some of us don’t worry about it at all. ZFC is so standardizing that this strange situation hasn’t been a problem for a really long time. Can ETCS do the same?

Posted by: François G. Dorais on December 19, 2012 11:30 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks for clarifying! It sounds to me like you’re saying that ETCS is just not powerful enough, is that right? I’m not sure what ‘robust’ means — I would have guessed it meant something very different than ‘powerful’, such as ‘stable under more model constuctions’ or ‘admits more consistent extensions’. But I agree that ETCS is not powerful enough. Even though it may be true that most mathematics can be done in it, or can be coded in such a way as to be done in it, mathematicians are used to thinking in ways that are hard to explain in ETCS.

I do think that a lot of ‘uses’ of the axiom of replacement are due to using the wrong notion of ‘family of sets’. To paraphrase Bishop, the axiom of replacement is used to put elements back into sets that they should never have been taken out of in the first place. The point of view of indexed categories clarifies that issue a lot. Unfortunately, it is a bit complicated for the average mathematician to accept as part of a foundational system.

But even accounting for that, I do agree that there are ‘real’ uses of replacement in math. Transfinite inductive constructions are a good example. (If one uses the ‘right’ notion of ‘family’, then really what’s getting used here is the axiom of separation, but in that case it carries all the power normally accorded to replacement, so the point is the same.) One can argue that there’s still a ‘wrong notion of family’ lurking here, but it’s hard to correct while remaining in a first-order-axiomatized theory. Type theory, with dependent types and propositions-as-types and (higher) inductive types, is, I think, the only really sensible way to deal with this at the end of the day. But I’m doing my best not to take over Tom’s blog post about set theory by prosyletizing for type theory. (-:

Posted by: Mike Shulman on December 19, 2012 3:00 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I guess “robust” might be meant in a sociological sense of being stable, i.e., less subject to a change of mind that it’s not yet enough for a foundations? That if history is any guide, that ZFC has been stable (and staple) for quite a long time now, and has proved adequate as a foundations?

If so, it seems to me any such sense must be relative, and not a precise mathematical notion. A judgment call.

Related to this, I do perceive some slight impatience with ETCS (such as in the first comment below David Roberts’s response at MO), particularly with the oft-repeated claim that it is “enough for the needs of working mathematicians, outside of logic and set theory”. That impatience has a point to it: what does that claim mean precisely? What is the exact scope? I personally have faith that there is some substance behind the claim, but it’s never been carefully articulated to the best of my knowledge. Category theorists (and I definitely include myself here) ought to take note of this fact, and beware the dangers of being too hand-wavy about this claim.

Posted by: Todd Trimble on December 19, 2012 4:17 PM | Permalink | Reply to this

Re: Rethinking Set Theory

You guys are forcing me to formalize my thoughts on what makes a good foundation more than I ever have. Sadly, it’s not a very common question these days, perhaps as a result of the ZFC hegemony.

I think I use “robust” as a combination of two things:

  1. A foundation must be rigid enough to permit reasonable communication among mathematicians, even if they disagree about unspecified details. The theory must be strong enough to ensure that all standard objects behave in standard ways. The usual behavior of standard objects should not be affected by choices beyond the ones made by the foundational theory.

  2. A foundation must be strong enough to meet everyone’s needs, provided they are not actively testing limits. (I think that phrase is much more reasonable than “except logicians and set theorists”, which always makes me feel a little guilty for ruining the party.) It should do that without excess but not necessarily with that much restraint.

Mike was allowed a small rant, so I guess I’ll have one too. :-) Gödel’s Incompleteness Theorem is the perhaps the only theorem that strikes fear among mathematicians. I think that’s a strange overreaction. A more reasonable, but still cautious, approach is to go as far as possible without jeopardizing the possibility of falling back to a more stable point in case of emergency. Gödel was not afraid of large cardinals (for most of his life); even with regular reminders about Reinhardt cardinals, most set theorist are not very concerned about the consistency of large cardinals. That’s not because set theorists like living dangerously, it’s because they know better. It’s true there is probably no general need for supercompact cardinals or even measurable cardinals (which nevertheless do occasionally pop up outside the boundaries of pure set theory), but I don’t think anyone needs to be excessively worried about inaccessibles and such, especially if they are only used for convenience. Logicians are always there to find workarounds and they are likely to find them before we bump into any problems. Instead of worrying about Grothendieck universes and such, people should be more worried about having only one proof for this or that theorem they care about. Statistically speaking, that lone proof is much more likely to collapse than any known large cardinal hypothesis.

Posted by: François G. Dorais on December 19, 2012 10:06 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Do you have any ideas regarding how one might go about articulating such a claim precisely? Mathematicians seem to be comfortable with the analogous claim that ZFC is enough for the needs of working mathematicians. What does that claim mean precisely?

Posted by: Mike Shulman on December 19, 2012 10:12 PM | Permalink | Reply to this

Re: Rethinking Set Theory

In case it’s not clear (since Francois’ comment snuck in between), this was intended as a reply to Todd.

Posted by: Mike Shulman on December 20, 2012 2:22 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think Todd is correct that these are sociological criteria. In fact, I would more precisely say that while a theory is a mathematical concept but a foundation is a sociological one. I think the only reasonable measure is to have a critical mass of mathematicians agree with these statements. With this in mind I recommend against aiming for just enough. Your question, which basically asks for exactly what you need to do, is still in the same spirit. I think you need to let go of that idea and see what comes out.

Note that ZFC is not without critics! Category theorists are renowned for saying that ZFC is not cutting it for them. I’m glad to see a genuine push for ETCS and other alternatives coming from Tom, Mike, Todd and others. I think you need to come up with what you need but be ready to adjust when others express needs that aren’t met with your initial choices. Remember that ZFC started out without the F and the C took a long long time to get anchored. Indeed, even the Z wasn’t there at the very beginning! I suspect ETCS will undergo similar alphabetic changes. In fact, one can view Tom’s piece as an effort to suppress the C…

Posted by: François G. Dorais on December 20, 2012 2:39 AM | Permalink | Reply to this

Re: Rethinking Set Theory

In fact, one can view Tom’s piece as an effort to suppress the C…

I suspect François had his tongue in his cheek, but I’ll take the opportunity to clarify and explain some things anyway.

It’s interesting, I think, to speculate on why, in its nearly 50 years of existence, ETCS hasn’t become more popular or well-known. Here are some possible explanations:

  • It’s not very good. Obviously I disagree with this.

  • It’s too weak. But it’s been known for forty years that if you add replacement, it has the same strength as ZFC.

  • ZFC was there first. That, I think, is a very important factor.

  • It hasn’t been as well explained as it might have been. Again, I think there’s some truth in this, otherwise I wouldn’t have written this article — but see below.

I’m sure one could add many more possibilities, but I want to expand on the last one.

There are good explanations of ETCS in the literature and on the web, many of which I cite. However, as far as I know, almost all of them either assume the reader knows what a category is or introduce categories before stating the ETCS axioms. (For example, Lawvere and Rosebrugh adopt the second strategy in their book Sets for Mathematics.) Since some people seem to be allergic to categories, I thought it would be useful to write an explanation that avoided the c-word as far as possible.

Certainly I think of ETCS in categorical terms, and it positively helps me to summarize the axioms as “well-pointed topos with NNO and choice”. But, of course, 99% of mathematicians won’t understand what this phrase means. I think the association with topos theory has given categorical set theory a reputation for being fearsome, and one of my goals was to undo this.

(Part of the reason why I think it has a fearsome reputation is personal experience. I’m just old enough to have seen Saunders Mac Lane speak at a few conferences, and the last time was in Como in 2000, where he expressed the wish for someone to write a short, elementary book on categorical set theory. At the time I thought that sounded pretty crazy, because even as a postdoc in category theory, my impression was that categorical set theory was an enormously sophisticated subject that couldn’t possibly be made elementary. I was wrong!)

I think there are some category theorists who won’t like what I’ve done, because they’ll think it’s too much of a compromise: they’d say that everyone should learn about categories, and to explain ETCS without categories is somehow a misrepresentation. I suppose what I’d say to such a person is that for a mathematician who doesn’t know anything about categories or actively distrusts them, a category-free account of ETCS could provide an attractive way in.

Posted by: Tom Leinster on December 23, 2012 3:27 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I agree that this is a sociological issue! I thought Todd was saying instead that he felt we needed to state and prove some precise theorem with a meaning like “ETCS is enough for the needs of working mathematicians”, and I couldn’t imagine how to do that.

(Personally, I’m not pushing for ETCS any more. While I prefer ETCS+R to ZFC, I prefer SEAR to ETCS+R, and I prefer homotopy type theory to both of them. So insofar as I’m going to spend any effort pushing for a new foundation, right now it’s going to be HoTT. But we need people to push for everything!)

Posted by: Mike Shulman on December 20, 2012 4:10 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Just to respond very briefly (I wish I had more time these days) – no, I didn’t at all have in mind a formal theorem. On the other hand, I still don’t like the weasel words “enough for working mathematicians except for logicians and set theorists” – what I want are really convincing examples of the exceptions that ETCS advocates should take note of, examples of theorems important to “working mathematicians” but that really require replacement.

Yes, I know about the set X+PX+PPX+X + P X + P P X + \ldots, but such a set doesn’t really appear in any important theorem I know of. More seriously, there is a general transfinite recursion principle in ZFC that crucially involves replacement, but the question remains whether there aren’t enough instances of recursive constructions already available in ETCS to satisfy those “working mathematicians”. Anyway, what I’d like to do is adopt a skeptical perspective and subject this slogan about the sufficiency of ETCS to the acid test: let’s produce a theorem that working mathematicians use that cannot be suitably formulated and proved in ETCS.

Posted by: Todd Trimble on December 23, 2012 12:43 PM | Permalink | Reply to this

Re: Rethinking Set Theory

If a category theorist counts as a working mathematician, then I think one example is the transfinite construction of free algebras. I expect that this is not possible in ETCS in generality, although I don’t know of a proof.

Of course, one may also ask whether or not there are particular instances of this theorem that one wants which fail to be true in ETCS. That I have less intuition for: it could be that most or all examples which arise in practice do exist. However, it seems likely that any version of the general theorem which could be proven in ETCS would be rather more complicated to state and apply, and perhaps no single version would suffice for all examples. I think it’s fair for the “working mathematician” to want the ability to state and prove theorems at the most natural level of generality, even if most particular applications could make do with less.

Posted by: Mike Shulman on December 23, 2012 2:50 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Type theory, with dependent types and propositions-as-types and (higher) inductive types, is, I think, the only really sensible way to deal with this at the end of the day. But I’m doing my best not to take over Tom’s blog post about set theory by prosyletizing for type theory.

Looking briefly over this discussion only now, I searched the comments for “type theory” in the hope to find this kind of comment.

These days, in front of a backdrop of higher categories, rethinking sets seems to make one want to think types.

I, for one, would enjoy seeing a separate post, such as not to hijack this one, on “Rethinking sets by thinking homotopy types.”

On the other hand, Egbert Rijke should have a nice article on this out soon. Maybe we should wait until then.

Posted by: Urs Schreiber on December 28, 2012 3:16 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Regarding ‘equivalence’, I see the point, but since ZFC and ETCS are not expressed in the same language, it doesn’t seem that there is any potential for confusion, since the other notion of ‘equivalence’ doesn’t make sense. I find the word ‘biinterpretable’ to be somewhat opaque, in addition to not capturing what’s going on here – we really do have an equivalence of something, in the sense that category theorists and other mathematicians always use the word, which is not the case for other cases of biinterpretability (including even ETCS+R-AC and ZF). What if we said something like ‘models of ETCS+R are equivalent to models of ZFC)?

Posted by: Mike Shulman on December 19, 2012 3:07 PM | Permalink | Reply to this

Re: Rethinking Set Theory

You’re right, what you have here is actually much stronger than biinterpretability. (I also agree that biinterpretability is not very congenial and I do not recommend using that term in this document.) I don’t think there is a name for this kind of situation. I still don’t like “equivalence” since that usually entails “drop-in replacement” which is too strong. I’m afraid I don’t have a good solution here…

Posted by: François G. Dorais on December 19, 2012 4:54 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This seems to me like the same sort of issue as the following more familiar ones:

  • Two group structures on the same set can be different, yet isomorphic as abstract groups.

  • Two atlases on the same space can be inequivalent, yet diffeomorphic as abstract manifolds.

An axiom system can be thought of as extra structure on top of a “signature” of some sort. And so two axiom systems with the same signature (like ZF and AFA) may be inequivalent as axiom systems (prove different theorems), yet be equivalent as “abstract theories” in the sense that there is an equivalence between their models.

From the homotopy type theory point of view, this amounts to saying that if we have two elements of a Sigma-type x:AB(x) \sum_{x:A} B(x) with the same first component, say (a,b 1)(a,b_1) and (a,b 2)(a,b_2), we can have an equality (a,b 1)=(a,b 2)(a,b_1) = (a,b_2) (in the type x:AB(x) \sum_{x:A} B(x) ) without necessarily having an equality b 1=b 2b_1=b_2 (in the type B(a)B(a)). The point is that in general, an equality (a 1,b 1)=(a 2,b 2)(a_1,b_1) = (a_2,b_2) consists of an equality p:a 1=a 2p:a_1 =a_2 and an equality q:p *(b 1)=b 2q : p_*(b_1) = b_2, and just because a 1a_1 and a 2a_2 may happen to be the same, it doesn’t follow that pp is trivial.

(Sorry for the type theory, I couldn’t resist. (-: )

Posted by: Mike Shulman on December 20, 2012 12:23 AM | Permalink | Reply to this

Re: Rethinking Set Theory

We could use “Morita equivalence”, which means by definition that there is an equivalence of categories of models. Admittedly it doesn’t capture the equivalence of signatures part, but I sense this is too much to ask for: in the case of algebraic theories, if the categories of models are equivalent in a way that respects the forgetful functors, then the theories must be equivalent in the logical sense.

Posted by: Zhen Lin on December 22, 2012 11:29 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Morita equivalence isn’t a bad idea. Is there any chance it already means something in logic that we would be clashing with?

Posted by: Mike Shulman on December 22, 2012 9:33 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks very much, François. I’m really glad to have your comments in particular.

(That might just sound like me obeying my own pleas for politeness, but actually I mean it.)

As you guessed, I didn’t mean “equivalence” in the precise sense that you had in mind: I was being somewhat vague. (In fact, I wasn’t aware of that precise usage.) I’ll have to reword it.

I’m not sure I understand what you say about replacement. As you know, ETCS has the logical strength of Zermelo set theory with bounded comprehension and choice. For a long time, people in category theory have been saying things like “no more than ETCS is needed anywhere in undergraduate mathematics”, though I don’t know of any places where such claims are written down, and I certainly can’t point to a written justification.

More recently, work of Colin McLarty, and I think also Angus Macintyre (?), seems to show that very large chunks of twentieth century mathematics can rest on ETCS as a set-theoretic foundation. I say “seems to” not to cast any doubt, but because this is way beyond my expertise, and (as you know) there was some scepticism expressed in response to this MathOverflow question.

This appears to suggest that bounded comprehension (i.e. ETCS) is enough for almost all purposes. Do you think that’s true? Of course, “almost all” is terribly vague, but let’s say “all the research that’s done in your department apart from logic and set theory”.

That’s not to deny, of course, that for a few purposes we might want to assume full replacement. But can’t we think of that as a kind of optional extra, in the same way that we might think of large cardinal axioms?

Posted by: Tom Leinster on December 18, 2012 9:20 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Even better than assuming full replacement as a ‘added axiom’, we could assume the existence of the set we actually needed (for example ω\aleph_\omega), which is more along the lines of large cardinals. However, I’m sure there are times when the technique of proof requires replacement multiple times, and in this instance assuming the existence of certain sets would get cumbersome.

However, I’m curious to know what sort of results one can arrive at using replacement of bounded complexity, since the ability to take any given formula in the language of set theory doesn’t seem strictly necessary for a large number of results (this is a hereditary notion, obviously).

Posted by: David Roberts on December 18, 2012 11:19 PM | Permalink | Reply to this

Re: Rethinking Set Theory

David, “admissible sets” and “Kripke-Platek set theory” are the two key words for your query in the second paragraph.

Posted by: François G. Dorais on December 19, 2012 12:13 AM | Permalink | Reply to this

Re: Rethinking Set Theory

A little more regarding the second paragraph…

It is a consequence of compactness that any single theorem of ZFC depends only on finitely many instances of replacement and comprehension. However, the fact that neither replacement nor comprehension can be reduced to finitely many instances is tougher to argue. The only way to make essential use of full replacement or full comprehension is to prove a theorem scheme. One example of this is the Reflection Theorem which consists of infinitely many theorems, one for each formula in the language of set theory.

Posted by: François G. Dorais on December 20, 2012 6:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I’m glad you appreciated my comments, Tom. Let me add some more!

The work of Colin McLarty is part of a reverse analysis of EGA and SGA. For this purpose, using as weak a theory as possible is the goal. Avoiding replacement is indeed one of the first things to try since it is often not used or at least substitutable in some way or another. In fact, much less than ETCS is necessary for most things. This is actually my selfish motivation for seeing you write this piece. I have been using some very weak categories to do these kind of reverse analysis for a while. This work would be much better motivated and easier to sell if people were actually using something like ETCS in everyday mathematics like you are proposing.

That said your goals are very different. As you pointed out elsewhere, the word “foundation” doesn’t appear anywhere in your draft even if that is precisely the goal. Minimalist approaches to foundations tend to fail or wither away. I think the reason is summarized by this Woody Allen quote: “It’s better to be rich than poor if only for financial reasons.” So the general goal is to accommodate everyone but to stay away from excess to avoid inconsistency. ETCS is just too small to accommodate everyone, ETCS with replacement is more than enough to accommodate everyone and is not excessive.

The main use of replacement in everyday mathematics is to prove “there is a large enough gadget.” Sadly, replacement is rarely used explicitly in such arguments. This weekend, I came across Section 3.9 of the stacks project, which happens to make many important uses of replacement but never mentions it once. Replacement is often right there but it’s hard to see. It’s also often possible to circumvent replacement on a case-by-case basis, but doing that is rarely of any interest for everyday mathematics.

The other point that I made earlier is that a foundational theory needs to be believable. You should be able to see how it does capture your intuitive mathematical universe. ETCS is not that convincing and replacement (or perhaps collection) would definitely help. This appears to be difficult to explain. The tell for me is that ETCS has too many “natural” models that are much to small and cramped to serve as actual universes. ETCS with replacement has no such models. (It has plenty of small models, of course, but they are not “natural” models.)

Posted by: François G. Dorais on December 18, 2012 11:51 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This weekend, I came across Section 3.9 of the stacks project

That’s an interesting point, because there is a lot of bending over backwards to show that there is a small category of schemes closed under all the usual operations, given an initial set of schemes. However, one can think of the category of schemes as being small sheaves on the opposite of the category of rings (e.g. remark 9.10 in that article). However, I’m not sure of the foundational needs to discuss such things. My intuition is that should work as a proof in topos theory, only referring to the category of sets and other toposes, but Mike would know better than me.

That said, one then needs to consider stacks on the opposite of the category of rings, hence ‘small stacks’, which I think is bleeding-edge research.

Posted by: David Roberts on December 19, 2012 12:55 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Very nice! (But why two columns?)

Of course, I’m a little biased, but I think that SEAR is also useful to consider, especially when addressing the three misconceptions that you mention about structural set theory. Instead of ETCS’ two basic notions of “sets” and “functions”, SEAR’s basic notions are “set”, “element of a set”, and “binary relation between sets”. (An alternative formulation uses “sets”, “elements”, “subsets”, and “pairing” instead.) I think it feels more familiar to mathematicians to have elements of a set as a basic thing rather than a defined notion. Moreover, in SEAR there is a “separation axiom” taken as basic, which also fits the way mathematicians think about sets. Plus, you don’t need to assert things like composition of functions as part of the axioms, which to a non-category-theorist may smell a little fishy: in SEAR you can define the composition of functions (which, of course, are defined as functional binary relations), and prove that it is associative.

Finally, since SEAR is completely equivalent to ETCS, I think it shows that Francois’ objection that ETCS is a “theory of functions” rather than sets is not correct. Both of them are theories of sets; it’s just that in order to have a good theory of sets, you need some extra structure around in order to say anything about sets. Functions are one choice. Relations are another.

Posted by: Mike Shulman on December 18, 2012 12:45 PM | Permalink | Reply to this

Re: Rethinking Set Theory

It’s a nitpick, but I also don’t favor the two-column format for anything I have to read online. For example, I don’t enjoy this feature that is to be found in anything appearing in the Notices of the AMS.

Posted by: Todd Trimble on December 18, 2012 3:08 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Mike wrote:

why two columns?

So that you can read it on your phone, of course!

Sasha Borovik told me that it makes his students happy when he produces his lecture notes in two-column format, for exactly this reason. I’m not sure we should be encouraging students to read lecture notes on phones, but there we are.

Actually, I wasn’t thinking about phones. People like me don’t have smartphones: personally, I use yoghurt pots and some really tight string. But newspapers and magazines are nearly always in multi-column format, whereas textbooks and literature are nearly always in one column. Multiple columns somehow seem to go with lighter, more expository writing. But I note your preference!

Posted by: Tom Leinster on December 18, 2012 9:30 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I don’t really like two columns for anything. I suppose this might have something to do with the fact that I do almost all my reading on electronic devices now (computer, tablet, ereader).

Posted by: Mike Shulman on December 19, 2012 7:33 AM | Permalink | Reply to this

Re: Rethinking Set Theory

One last comment on the set vs function issue. I won’t add more since I think this issue is potentially too volatile. Thankfully, it hasn’t flared and I hope this comment will help keep it that way.

I think the issue is a cultural one, so there is no right and wrong, correct or incorrect, only differences. To me, in the broadest sense of the word, a set is a container with no distinguishing features other than its contents. Therefore, I think that a set theory must have an extensional membership relation. Anything goes after that, but extensionality is essential. So I do not think of ETCS and SEAR are set theories, though SEAR is interesting since it does not have equality for “sets”.

Mike and Tom are from a different culture and have a different perspective on what a set is. That is perfectly fine, I understand why that is and I respect their point of view. I do hope that I raised awareness of my point of view and that Tom will understand that ETCS might be more difficult to sell as a set theory for some. (I’m saying that because I do want people to buy into ETCS. It’s a very nice theory with very good potential!)

Posted by: François G. Dorais on December 18, 2012 3:28 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This is not meant to refute what you say, François – because after all it doesn’t, and in fact you have pointed to a core difference between membership-based set theories and other set theories. I just wish to point out that there is an extensionality principle in ETCS that says that given two subsets i:ASi: A \hookrightarrow S, j:BSj: B \hookrightarrow S of a given set, they are the same (in the sense of an isomorphism ABA \to B completing a commutative triangle) if they have the same elements (i.e., elements s:1Ss: 1 \to S which are included in both, again in a sense of commutative triangles).

One could argue that this extensionality principle is the one used most often in mathematical practice.

Posted by: Todd Trimble on December 18, 2012 4:25 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks, François. Part of the reason for airing this draft here is that I wanted to get some indication of what to expect people’s reactions to be, and you’ve helped with that.

Over the last few days I’ve been thinking about what to say regarding the question “is ETCS a set theory?”. To be honest, it took me by surprise that you raised this, because although I know some people unthinkingly use “set theory” to mean exclusively membership-based set theory, more or less through habit, it hadn’t really occurred to me that someone might have actual thought-out reasons for doing so. Again, it’s useful to know this.

The reason why I didn’t comment sooner isn’t that I was worried about incivility, but that I simply hadn’t figured out how to arrange my thoughts. I still haven’t, but I’ll give it a go.

Up here, you wrote:

I think that your brushing aside of replacement is overdone

I’m beginning to agree, if only because the matter of logical strength is a distraction from what I think are much more interesting questions. I wouldn’t want people to go away thinking that the main difference between ETCS and ZFC was that one is weaker than the other, when much more importantly, it’s a radically different way of thinking about sets. (And, after all, if one wants replacement, one can have it.)

But I do think the question of what one counts as “set theory”, or maybe what one counts as “a set theory”, is interesting and worth discussing, even though it’s obviously subjective.

To me, in the broadest sense of the word, a set is a container with no distinguishing features other than its contents. Therefore, I think that a set theory must have an extensional membership relation.

I think this gets to the heart of the difference. If I remember correctly, Lawvere uses “abstract set” for a set conceived as a bag of electrons or identity-less points — “pure cardinality” — and “general set” for something closer to what you describe. My grip on what’s meant here is a bit shaky, since, for example, in ETCS the elements of a set XX don’t seem to be anonymous: they’re named by the maps 1X1 \to X. But anyway, between ZFC (say) and ETCS there’s a genuine difference in conception of what a set is. That’s what makes the question interesting.

There are theories of sets-and-membership (such as ZFC), theories of sets-and-functions (such as ETCS), theories of sets-membership-and-relations (such as SEAR), and so on. Each can look strange and alien from the point of view of the others. Taking the first two:

  • From the point of view of membership-based set theory, categorical set theory looks like a theory of functions. The unfamiliar features that strike a membership-based set theorist are categories, toposes, a weird treatment of elements, and maybe more besides which I’m not thinking of because of my own background.

  • From the point of view of categorical set theory, membership-based set theory looks like a theory of… well, membership. The unfamiliar features that strike a categorical set theorist sees are the cumulative hierarchy and the way that each set is given the structure of a (possibly infinite) tree, via a global membership relation.

But this is to emphasize the differences. There’s also a common core. Most fundamentally, all these systems seek to axiomatize sets. Then there are the theorems we’ve been discussing, asserting equality of proof-theoretic strength, bi-interpretability, etc. Maybe there’s a case to be made for being inclusive and calling them all set theory.

Perhaps this wider viewpoint could even help with questions of direct concern to (membership-based) set theorists. I don’t know enough about set theory to pronounce on this myself, but here’s a bit about forcing from Mac Lane and Moerdijk’s Sheaves in Geometry and Logic, Section VI.2, just after they’ve given a proof of the independence of the Continuum Hypothesis:

Nevertheless, it is our clear understanding that the ultimate mathematical content of all these methods (generic sets, Boolean-valued models, and double-negation sheaves) is essentially the same. Indeed, a reading of the original paper by Paul Cohen clearly reveals the role there of double-negation. And sheafification has a wraith-like presence in Cohen’s paper.

Perhaps a full understanding makes use of all three approaches — generic sets, sheaves, Boolean-valued models!

There’s a sense in which everything I’ve said in this comment so far is navel-gazing, because the use of sets in set theory and category theory is dwarfed by the use of sets elsewhere in mathematics. My view is that any study of sets as broadly used deserves to be called set theory (and any axiomatization arising from this deserves to be called a set theory). Since I believe that ETCS more closely models how most mathematicians use sets than ZFC does, I think it has at least as much right to be called a set theory.

(As I keep saying, I know this is an entirely subjective judgement: how the terms “set” and “set theory” are used is a matter of social convention, not mathematical fact. It’s just a point of view.)

Incidentally, the people who I would least expect to benefit from thinking about sets in terms of ETCS(+R) are in fact set theorists. That’s exactly because (as I understand it) set theory in the traditional mould is so much about the membership relation. E.g. Joel David Hamkins wrote this just recently:

of course set theorists don’t care what their sets are made out of either, as long as the set-membership relation has its characteristic properties, which is the relevant structure for set-theorists.

One interesting question to which I definitely don’t know the answer is how essential that membership relation really is to current set theory research. Perhaps it’s less essential than it seems. For example, in his paper ‘Exploring categorical structuralism’, Colin McLarty writes:

Large-cardinal axioms are usually given, by ZF set theorists, in isomorphism-invariant form […] Large cardinals are routinely pursued in isomorphism-invariant terms.

I don’t mean to imply that no one should think about sets in the treelike way of ZF; on the contrary, it seems to be a very interesting subject. I’m just curious about how necessary the global membership structure is to the central concerns of research-level set theory.

Posted by: Tom Leinster on December 23, 2012 6:50 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Another very important difference between traditional set theory and categorical/structural set theory resides in how each thinks what a function is.

It is absolutely crucial to categorical thinking that functions and more generally morphisms have both a domain and a codomain. Whereas traditionally, a function is just a collection of ordered pairs with a specified domain and a unique existence property – no codomain need be specified.

This difference of course has far-reaching consequences. If for example we treat “elements” as instances of morphisms (viz., morphisms whose domain is terminal), then on the categorical side it follows that an element x:1Xx: 1 \to X belongs to a unique set, namely the specified codomain XX. This consequence fits in well with a principle (which I think is also seen in type theory) which in one of my blogs on ETCS I referred to as “context-dependence”. I tried to describe it thus:

… It corresponds e.g. to a decision never to consider a number like ‘3’ in isolation or as some Platonic essence, but always with respect to an ambient system to which it is bound, as in ‘3 qua natural number’, ‘3 qua rational number’, etc. It is a firm resolve to always honor context-dependence. Naturally, we can in a sense transport ‘3’ from one context to another via a specified function like [an inclusion] \mathbb{N} \to \mathbb{Q}, but strictly speaking we’ve then changed the element. This raises interesting questions, like “what if anything plays the role of extensionality?”, or “what does it mean to take the intersection of sets?”. (Globally speaking, in ETCS we don’t – but we can, with a bit of care, speak of the intersection of two “subsets” of a given set. For any real mathematical purpose, this is good enough.)

This conception of sets and elements is quite a radical break from membership-based set theory! Naturally, in ZFC we could if we want also identify elements with certain functions with codomain 11, but since functions aren’t considered to have specified codomains, we have instead context-independence where an element can happily belong to many different sets.

I think too this difference between how one considers functions shows up in the fact that the replacement axiom scheme is straightforward to write down in ZFC terms, but slightly awkward in terms of categorical set theory.

I wonder whether it would be worthwhile to mention any of this in your paper, Tom?

Posted by: Todd Trimble on December 23, 2012 1:28 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks for this excellent comment, Todd. I first began to understand the differences you’re describing when I read your Topological Musings blog entries, and to be honest I’m still absorbing the ramifications. (For example, I don’t yet have a settled point of view on subsets versus what Lawvere and Rosebrugh call “parts”.)

I wonder whether it would be worthwhile to mention any of this in your paper, Tom?

Once again, this is something that would definitely be useful to mention (at least if I could express it as well as you), but which I decided against purely for reasons of space. I really want to keep this short. My self-imposed limit is eight pages in the current formatting, and even a couple more lines could tip me over.

the replacement axiom scheme is straightforward to write down in ZFC terms, but slightly awkward in terms of categorical set theory.

You think so? It seems completely straightforward to me — am I just overfamiliar with it?

Well, maybe there’s one place where it is a bit awkward, which is where you say that the sets X iX_i of which you’re taking the coproduct are only specified up to isomorphism. Here I’m working with the replacement scheme described in Section 8 of McLarty’s Exploring categorical structuralism. Actually, I’m fuzzy on the relationship between McLarty’s replacement scheme and the much earlier schemes of Osius etc., which I don’t think involve this “up to isomorphism” bit. Do you know what’s going on?

Posted by: Tom Leinster on December 23, 2012 5:47 PM | Permalink | Reply to this

Re: Rethinking Set Theory

There are theories of sets-and-membership (such as ZFC), theories of sets-and-functions (such as ETCS), theories of sets-membership-and-relations (such as SEAR), and so on.

While I agree with this, I think Francois and Walt have a point that the ZF-style sets-and-membership conception of set is closer to the non-mathematical one. For instance, as definitions of “set” we find

a collection of articles designed for use together: a set of china; a chess set

and

a collection, each member of which is adapted for a special use in a particular operation: a set of golf clubs; a set of carving knives

and

a number, group, or combination of things of similar nature, design, or function: a set of ideas.

I think this probably has more to do with the non-mathematical nature of things than it does with the notion of set. The idea of “abstract points” with “no internal structure” is alien to everyday thinking: everything in the “real world” is a thing with a unique identity, pre-existing before it is collected into a “set”.

I particular, I think it’s entirely natural that when Cantor, Zermelo, etc. first began to speak about “sets” mathematically, they had this conception of “set” in mind, and produced corresponding axiomatic theories. However, it has emerged, over the past hundred years of experience using this sort of set theory as a foundation for mathematics, that this sort of set is not what most mathematicians need or want. Since sets were what was on offer, mathematicians used them, but they simply ignored all the unneeded extra membership structure whenever they didn’t want it. Thus, in mathematics outside of set theory, the word “set” has largely come to mean something different, even if most mathematicians are not aware of that. Hence, the impetus to formulate new “set theories” whose “sets” behave in the way that mathematicians actually use them.

It’s a shame that we didn’t realize early on that what mathematicians need is not “sets” in the original non-mathematical sense. If we had, then we could have chosen a different name for those “bags of points”, and then all this confusion would be unnecessary.

Fortunately, there is a solution. Here’s the relevant definition of “set” from MW:

a number of things of the same kind that belong or are used together

(emphasis added). In other words, sets are always sets of elements of some type. Thus it makes sense to consider two very different sorts of “collections”:

  • A type is the collection of all “things” which have that type. Of course, that sounds tautologous. The point is that an element of a type by its very nature belongs to that type. You can’t pick and choose what to “put into” a type. Outside mathematics, we might have the type of people, or the type of ideas. Inside mathematics, we have the type of real numbers, or the type of smooth manifolds.

  • A set is a collection of some of the elements of a particular type. Here we get to choose which elements of the ambient type to put in or take out. We may have the set of United States Senators, or the set of thoughts that I had yesterday; the set of real numbers whose square is less than 2, or the set of manifolds admitting a hyperbolic metric.

ZF-style theories formally ignore the existence of types. Or, rather, as Bob Harper would say, they suppose that there is only a single type. The only sort of collection we can form is a set — a set of elements of the unique type. We then have to recover the difference by treating some sets as type-like. For instance, after constructing the real numbers, we forget that its elements are anything but “real numbers”. In this world of hyper-reductionism, it turns out to also be possible to “define” other important structures such as functions and relations as particular sets.

By contrast, ETCS formally ignores the existence of sets: it has only types. Of course, it then reuses the word “set” to mean “type”, as mathematicians have largely come to do over the past century. In this case, we define a “set of elements of some type AA” to consist of another type equipped with an injection into AA. Since this approach is less hyper-reductionist, it makes sense that we need some additional structure relating types to other types, such as functions.

I think that both sorts of collections arise naturally all the time in mathematics, and of course because of the ZF hegemony both are confusingly called “sets”. Category theorists tend to see “sets-as-types” more frequently, since we work in a more abstract top-down world. Hence we naturally think that that’s what “set” should mean, and invent theories like ETCS. But just as ZF is awkward for structural mathematics because of all the superfluous membership that has to be forgotten, ETCS has its own awkwardnesses, such as the treatment of subsets, power sets, and function sets. In ETCS, for instance, elements of “the power set of XX” are not intrinsically subsets of XX in any sense; we can only view them that way when P(X)P(X) is equipped with the additional structure of some other sets and functions relating it to XX.

I would personally argue instead for a foundational theory which includes both types and sets as basic objects. SEAR is one attempt at such a theory, which speaks of “sets and subsets” rather than what I have here been calling “types and sets”. I think SEAR is somewhat better than ETCS in this regard, but it still has some of the same issues with power sets and function sets.

Of course, I’ve given away the punchline by using the word “type”. In a type-theoretic foundation, the basic objects are types, as in ETCS and SEAR, but we can also have sets. The most natural definition of a set of elements of type AA is a function APropA\to Prop, i.e. a predicate. (I’ve learned recently that type theorists sometimes call such a thing a “refinement type”.) Moreover, “APropA\to Prop” is itself a type, whose elements are by their very nature sets of elements of AA (or predicates on AA).

Of course, sometimes we want to regard a set B:APropB:A\to Prop as a type in its own right. Type theory also has an operation for that: the Sigma-type x:AB(x)\sum_{x:A} B(x). It’s often helpful for clarity to separate the view of BB as a set of elements of AA from the view of “BB” as a new type in its own right. In fact, we just saw something similar happening here.

Posted by: Mike Shulman on December 23, 2012 2:42 PM | Permalink | Reply to this

Re: Rethinking Set Theory

In particular, I think it’s entirely natural that when Cantor, Zermelo, etc. first began to speak about “sets” mathematically, they had this conception of “set” in mind, and produced corresponding axiomatic theories.

Colin McLarty (who I keep referring to, because he’s done so much excellent work on this) has often pointed out a difference of opinion between Cantor and Zermelo. This is from McLarty’s introduction to the long version of Lawvere’s ETCS paper:

Cantor gave an isomorphism-invariant account of sets, where elements of sets are “mere units” distinct from one another but not individually identifiable. Zermelo sharply faulted him for this and followed Frege in saying set theory must be founded on a membership relation between sets.

Here McLarty cites Cantor’s collected works, which were edited by Zermelo. I looked up one of the pages cited (p.351). This seems to be the relevant bit, from an editorial comment by Zermelo:

[1] Zu S. 282. Unter “Teilmenge” versteht Cantor hier nur eine echte Teilmenge, die von der Menge selbst verschieden ist. Auch die Definition der “Vereinigungsmenge” wird hier (unnötigerweise) auf den Fall unter sich elementefremder (exklusiver) Mengen eingeschränkt im Gegensatz zu dem früher (S. 145) eingeführten “kleinsten gemeinsamen Multiplum”.

Der Versuch, den zur “Kardinalzahl” führenden Abstraktionsprozeß dadurch scheinbar zu erläutern, daß die Kardinalzahl als eine “aus lauter Einsen zusammengesetzte Menge” aufgefaßt wird, war kein glücklicher. Denn wenn die “Einsen”, wie es doch sein muß, alle untereinander verschieden sind, so sind sie eben weiter nichts als die Elemente einer neu eingeführten und mit der ersten äquivalenten Menge, und in der nun doch erforderlichen Abstraktion sind wir um keinen Schritt weiter gekommen.

Unfortunately I don’t have remotely enough German to read this. The Google translation is pretty garbled:

[1] pp.282: Under a “subset” Cantor sees only a real subset, which is different from the quantity itself. The definition the “union” is here (unnecessarily) in the case foreign elements (exclusive) as opposed to the limited quantities earlier (p. 145) introduced the “lowest common Multiplum”.

The attempt for the “cardinal number” leading process of abstraction in to explain seemingly that the cardinal number as an “out of all ones combined amount” is understood, was not a happy one. because if the “ones”, as there must be, among all are different, so are they give nothing but the elements of a newly introduced and the first equivalent amount, and are now still necessary abstraction we come to any further.

Can anyone provide a decent translation?

Posted by: Tom Leinster on December 23, 2012 6:31 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Here’s an attempt:

[1] p. 282. By “subset” Cantor means here only a real subset, which is different from the set itself. Even the definition of “union” is (unnecessarily) limited here to the case of disjoint sets, in contrast to the earlier (p. 145) introduced “least common multiple”.

The attempt to elucidate thereby the process of abstraction leading to “cardinality”, that cardinality is interpreted as a “set of all units combined”, did not go well. Since if the “units” must all be different from each other, then they are nothing but the elements of a newly introduced set equivalent with the first one, and we have made no progress in the still necessary abstraction.

Posted by: Mark Meckes on December 23, 2012 8:01 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks very much!

Posted by: Tom Leinster on December 23, 2012 8:16 PM | Permalink | Reply to this

Re: Rethinking Set Theory

A lot has happened here over the past few days. I have a lot to say and I’ll make more comments later.

Cantor’s view of sets is indeed much closer to the structural view than one might think. This is very clear when one reads Cantor’s conception of cardinal number from his Beiträge zur Begründung der transfiniten Mengenlehre:

Every set MM has a definite “power,” which we will also call its “cardinal number.”

We will call by the name “power” or “cardinal number” of MM the general concept by which, by means of our active faculty of thought, arises from the set MM when we make abstraction of the nature of its various elements mm and of the order in which they are given.

We denote the result of this double act of abstraction, the cardinal number or power of MM, by M¯¯\overline\overline{M}.

Since every single element mm, if we abstract from its nature, becomes a “unit,” the cardinal number M¯¯\overline\overline{M} is a definite set composed of units, and this number has existence in our mind as an intellectual image or projection of the given set MM.

I used this quote in an intro set theory class I taught a while back as part of the motivation for the idea of cardinality and the difficulties involved in formalizing it. There is an important and subtle aspect of the very last part. When he says “this number has existence in our mind,” he is actually justifying the existence of sets made of anonymous “units,” linking directly to his earlier definition of set:

By a “set” we understand any collection into a whole MM of definite and separate objects mm of our intuition or our thought. These objects are called the “elements” of MM.

Bottom line: Cantor’s universe clearly contained both structural and material sets. In fact, I would argue that Cantor was much more interested in structural sets than material sets. I don’t think Cantor was very fond of Zermelo’s reduction of set theory to material sets. It would be fun to see if and when Cantor may have explicitly criticized that aspect of Zermelo’s work.

Zermelo’s quote is hard to understand since it criticizes technical iotas (whether subsets are to be proper or not) and Cantor’s use of structural sets on the same level. Did Zermelo really think that these were on the same level? That seems bizarre but it’s hard to actually understand the mindset of the time.

Posted by: François G. Dorais on December 25, 2012 11:08 PM | Permalink | Reply to this

Re: Rethinking Set Theory

What Cantor calls forming the cardinal number of a set does sound a lot like replacing a material set with an isomorphic structural one. But I’m not sure I would jump from that to say that Cantor’s universe contained either structural or material sets, in the sense that we now use the terms. For one thing, replacing a material set by a structural one doesn’t really have the properties you expect from the ‘cardinal number’ operation, so if he wanted that, then Cantor must have meant something at least slightly different. Similarly, Cantor says the cardinal number abstracts not only the nature of the elements of a set but ‘the order in which they are given’, suggesting that for him, all sets were (well?) ordered — except, I guess, the ‘sets’ that he calls ‘cardinal numbers’, although it’s not entirely clear to me how some sets could be by nature ordered and some not be. (Interesting, then, that modern material set theorists have chosen oppositely, making cardinals always well-ordered, but not arbitrary sets.)

The main thing I get from that passage is that Cantor’s ideas about sets were notably different from ours, and that from a modern perspective, maybe he was confusing some things that are actually different (or, at least, that it pays to realize the difference between, even if ultimately you decide you want to try to unify them somehow). But I think my point about the distinction between types and sets is valid, regardless of what Cantor may have historically meant by ‘set’, and that was the point I was trying to make, not a historical one.

Posted by: Mike Shulman on December 27, 2012 8:20 AM | Permalink | Reply to this

Re: Rethinking Set Theory

When Cantor abstracts away “the order in which they are given”, I wouldn’t infer too much about his ideas about sets. He definitely didn’t assume every set to be equipped with a well-order. I take the passage in quotes to be essentially an emphasis on the difference between the notions of equivalence that define ordinal and cardinal numbers, respectively, which together constitute his centre of interest.

Posted by: maltem on December 27, 2012 7:14 PM | Permalink | Reply to this

Re: Rethinking Set Theory

[Mike:] What Cantor calls forming the cardinal number of a set does sound a lot like replacing a material set with an isomorphic structural one. But I’m not sure I would jump from that to say that Cantor’s universe contained either structural or material sets, in the sense that we now use the terms.

It’s pretty clear to me that Cantor’s universe contains both material sets and structural sets. I reread Cantor’s paper with this in mind and it’s absolutely remarkable the way he anticipates the usefulness of structural set theory.

[Mike:] The main thing I get from that passage is that Cantor’s ideas about sets were notably different from ours, and that from a modern perspective, maybe he was confusing some things that are actually different.

It’s really difficult for us to understand what Cantor was writing since we incorporate a lot of later knowledge in our reading. Cantor was struggling with a lot of things that are now considered simple or even insignificant.

In the initial part of the paper, Cantor is concerned with cardinal arithmetic and the ideas he presents are basically the same as those we have today. However, Cantor is lacking some very essential tools. Notably, Cantor does not have a reasonable encoding of ordered pairs, which arrived more than a decade later. In addition to not being able to form the product of two sets, Cantor also doesn’t know how to disjointify two sets to form the coproduct.

Remarkably, it’s the structural view of sets that allows Cantor to formulate basic cardinal arithmetic. He doesn’t make a big fuss about it since it’s kind of obvious: if two sets are made of anonymous units, they are also disjoint from each other since there is no reason for them to share any anonymous units. So the plain union of two such sets is their coproduct. It’s clear to Cantor that two sets can always be replaced by disjoint sets when necessary.

Note how Cantor talks about multiplication of cardinals:

We now come to multiplication. Any element mm of a set MM can be thought to be bound up with any element nn of another set NN so as to form a new element (m,n)(m,n); we denote by (M.N)(M . N) the set of all these pairs (m,n)(m, n) and call it the “set of pairs (Verbindungsmenge) of MM and NN.

Cantor doesn’t care what the pairs (m,n)(m,n) are made of, he only cares that we can think of the two coordinates in some way or another. The product (M.N)(M . N) is only defined up to isomorphism. In modern terms, Cantor only cares that we have the two coordinate projections and that all possible pairs are in (M.N)(M . N), which is a weak attempt to capture the universal property of the product.

One can hardly fault Cantor for not thinking in terms of functions since he didn’t have a very firm grasp of these. Indeed, his treatment of cardinal exponentiation begins as follows:

By a “covering of the set NN with elements of the set MM,” or, more simply, by a “covering of NN with MM,” we understand a law by which with every element nn of NN a definite element of MM is bound up, where one and the same element of MM can come repeatedly into application. The element of MM bound up with nn is, in a way, a one-valued function of nn, and may be denoted by f(n)f(n); it is called a “covering function of nn.” The corresponding covering of NN will be called f(N)f(N).

Note how apologetic he is for having such an abstract view of functions! I don’t think Cantor would have inevitably be led to some form of category theory, but his views were already leaning that way, in a crude and awkward manner.

Anyway, this is mostly a digression: Cantor’s thoughts are not really relevant to ETCS. Still, I find Cantor’s highly structural perspective very enlightening. I am currently writing something (for my blog since it’s aimed at set theorists) about Cantor and Tom’s article. It may take a few days to get it done but stay tuned…

[Mike:] But I think my point about the distinction between types and sets is valid, regardless of what Cantor may have historically meant by ‘set’, and that was the point I was trying to make, not a historical one.

I don’t think anyone was thinking that way. Personally, I’ve been ignoring all talk of types throughout since it’s mostly a distraction from ETCS. But since we’re on the topic, note that Russell’s type theory and Zermelo’s set theory both came out in 1908. They were competing foundations for a while and Zermelo eventually won, though types never died out. The consensus at the time was that Russel’s type theory was more expressive and sophisticated while Zermelo’s was aimed at the working mathematician. This has changed a bit, but probably not enough; one can always hope…

Posted by: François G. Dorais on December 28, 2012 12:56 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Why is comparing ETCS to type theory any more of a distraction than comparing it to ZFC?

(What I do think is a distraction is Russelian type theory, which has as far as I can tell almost nothing to do with what is now called type theory.)

Posted by: Mike Shulman on December 28, 2012 6:56 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Well, my draft does compare ETCS with ZFC, but it doesn’t even mention type theory. So to the extent that this post is a discussion of my draft, it’s more of a distraction. But of course, discussion of type theory is welcome here too!

Posted by: Tom Leinster on December 28, 2012 7:20 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Why is comparing ETCS to type theory any more of a distraction than comparing it to ZFC?

Because it’s too interesting! I’m avoiding type theory (as well as some other topics, like what non-mythical set theorists actually do) to avoid derailing the discussion of ETCS. Like Urs, I think another place would be better to talk about this.

(Regarding Russell, we were talking about the situation in 1908, many decades before Martin-Löf type theory and other major breakthroughs in type theory. In my classical meiotic style, indicating that I don’t intend to dwell on the topic, I only said that “this has changed a bit.”)

Posted by: François G. Dorais on December 28, 2012 5:12 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I’m sorry, I said I was trying not to take over the discussion of your draft by talking about type theory, but then I guess as the discussion grew to seem more about structural vs material set theory more broady, I failed in my resolve. (-: Maybe I’ll start another discussion when I have a moment.

Posted by: Mike Shulman on December 28, 2012 8:02 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Just on the historical aspect: I too was quite mystified by Zermelo’s comment. I don’t doubt the accuracy of Colin’s scholarship, but personally I don’t see how what Zermelo writes here justifies the comment of Colin’s that I quoted previously.

However, Colin cites several pages from Cantor’s collected works, whereas I only looked at one of them (because my negligible German makes this very slow work). It could be that Zermelo’s remarks on the pages that I didn’t look at are more enlightening. If anyone who reads German wants to look at the pages concerned (351 and 440–442), they can find them here.

Posted by: Tom Leinster on December 26, 2012 12:21 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Here’s a very rough summary of what happens on p. 440-442:

Cantor identifies Frege’s “notion” (Begriff) with his “set” (Menge), and explains how he finds Frege’s exposition of the term Anzahl (cardinal number) deficient. Namely, he says that Frege explains it by means of the Umfang (Cantor reads: size) of a set, without ever actually defining Umfang, apparently taking it to be an inherently logical term. Cantor then goes on to explain how he defines the cardinal number of a set as, in modern words, equivalence classes of sets (or sets up to equivalence). He also treats the difference between cardinal and ordinal number (mainly a promotion of his own works).

Zermelo’s (?) comment below says that Cantor’s critique of Frege’s paper was too sharp, failing to account for its clarity on the account of cardinals, and goes on to reconcile their perspectives. Zermelo says that Frege’s and Cantor’s views of cardinals are after all not very different, both seeing them as “class invariants” (!). To this end, he reads Umfang not as “size” but as something like “totality”.

Posted by: maltem on December 26, 2012 3:03 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks! To respond to your “(?)”, the notes (Anmerkungen) in smaller type are by Zermelo, I think. Partly I think this because Colin McLarty’s citations wouldn’t make sense otherwise, and partly because on the front cover of the book which these pages are taken from (Cantor’s collected works), it says that it’s edited by (Herausgegeben von) Ernst Zermelo.

Posted by: Tom Leinster on December 27, 2012 12:50 AM | Permalink | Reply to this

Re: Rethinking Set Theory

This doesn’t go very far to helping how necessary the cumulative/membership/the-things-in-VV-are-the-small-subsets-of-VV set theory — but one thing it is at least handy for is proving universals by induction on von-Neumann levels, which is of course very much like induction on naturally-indexed things, and for at least the very good reason that ZFC minus infinity is modeled very well by HF sets which are themselves in a natural correspondence with the natural numbers, via totally-base-2 trees; so one might say ZFC is trying to do infinitary arithmetic in a manner as close as possible to finitary arithmetic, but focusing on bitwise operations rather than ++ and ×\times.

In a way, the sets of ZFC are both memory states and addresses, similar to the way pure lambda combinators are both programs and input data.

Posted by: Jesse McKeown on December 24, 2012 1:37 AM | Permalink | Reply to this

Re: Rethinking Set Theory

That’s a very interesting thought. It reminds me of something I’ve been noticing recently when trying to do homotopy theory in homotopy type theory. Namely, in classical homotopy theory, some standard arguments proceed by induction on a cell decomposition of a space. In homotopy type theory, not every type has a cell decomposition of any sort. However, many do, such as spheres, tori, and any other space presented using higher inductive types as a “cell complex”. So one approach would be to define what it means for a type to be “cellularly presented” or “inductively generated” or something, and then prove these theorems in a classical way under the additional hypothesis that the space is inductively generated.

Philosophically, the point would be that classical homotopy theory implicitly assumes that all spaces are inductively generated, but homotopy type theory frees us from that implicit assumption, allowing us to talk both about inductively generated spaces and non-inductively-generated ones. In sort of the same way that constructive mathematics generalizes classical mathematics by making its language more expressive, and homotopy type theory generalizes extensional type theory by expanding our field of view to include not just the h-sets, we could say that homotopy type theory generalizes classical homotopy theory by expanding our field of view to non-inductively-generated spaces.

This seems a bit analogous to what you are saying. ZFC implicitly (well, actually fairly explicitly, depending on how you formulate the axiom of foundation) assumes that all sets are “inductively generated” in a certain sense. If we view a well-founded relation as somewhat analogous to a cell decomposition (which I think is not very far-fetched), then this is analogous to the implicit assumption of classical homotopy theory that all spaces have cell decompositions. (The analogy would be closer if homotopy theorists regarded their spaces as always coming with specified cell decompositions, which they don’t usually.) Categorical/structural set theory frees us from this assumption, expanding our field of view to include sets that may not admit any “inductive presentation”. But as always with such a generalization, all the old theorems are still there; they just have an extra hypothesis that the set in question is inductively generated.

(Ill-founded set theories such as Aczel’s AFA might be said to instead assume that all sets are coinductively generated. I wonder whether there is anything analogous to this in homotopy theory.)

Posted by: Mike Shulman on December 24, 2012 5:13 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Mike, perhaps the cellular side of things is like ‘singular homotopy theory’ whilst the coinductive stuff is a strong shape theory. The basic objects of really classical homotopy theory are spaces only, the CW-complexes being introduced precisely to have a ‘combinatorial homotopy theory’ as in the title of Whitehead’s famous two papers.

Posted by: Tim Porter on December 24, 2012 6:40 AM | Permalink | Reply to this

Re: Rethinking Set Theory

We had a not very fruitful chat about coalgebaic tangles once.

And we had a chat about coinductively defined spaces here.

Posted by: David Corfield on December 24, 2012 10:45 AM | Permalink | Reply to this

Re: Rethinking Set Theory

What I have vaguely gathered from reading Bob Harper’s blog suggests that coinductive types are defined to support generalized cohomology operations, while inductive types are defined to support generalized homotopy operations… hmmm… so I wonder if

HigerCoInductive X (n:nat) := C : cocyle n X.

ought to be a K(Z,n)K(Z,n)? Probably not, as that sounds like begging the question; unless perhaps “cocycle” can be considered singularly, too.

Posted by: Jesse McKeown on December 24, 2012 4:58 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks for the thoughts, Tim, David, and Jesse! I think the duality between cell complexes and Postnikov decompositions does seem like the right one to be looking at: the one is built by pushouts and the other by pullbacks. (This duality, and the perspective of Postnikov decompositions as “cocell complexes”, is of course already fruitful in classical homotopy theory, e.g. in the theory of localization and completion.)

It’s not clear yet what the right notion of “higher coinductive type” is (in fact, arguably it’s not even clear what the right notion of ordinary coinductive type is), but it seems likely that it would include at least finite Postnikov systems, at least once given the K(G,n)K(G,n)s. In fact, though, you don’t even need any sort of coinductive type to build ordinary finite Postnikov systems given the K(G,n)K(G,n)s, because type theory already has pullbacks built in automatically; higher inductive types are only necessary to build cell complexes because traditional type theory doesn’t come with pushouts.

Anyway, perhaps the analogous statement that I was looking for would be that not all types have Postnikov decompositions — or, at least, are not recoverable from them — which is roughly the already-known statement that not all (,1)(\infty,1)-toposes are hypercomplete. There is a bit of a difference, though, in that you would have to specify a much wider class of “generating cocells”, namely all the K(G,n)K(G,n)s.

Posted by: Mike Shulman on December 24, 2012 10:40 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Can hypercompletion usefully be seen as a modality?

Posted by: David Corfield on December 26, 2012 11:23 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Absolutely! It’s even a left exact modality, i.e. a subtopos.

Posted by: Mike Shulman on December 27, 2012 8:22 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Mike wrote:

Of course, I’m a little biased, but I think that SEAR is also useful to consider

I agree! The current draft is dramatically slimmed down from earlier drafts. At one point it was 27 pages long; it’s now eight. The slimming process cut out a lot of things that I was rather attached to, including a passage about SEAR. So I’m glad you’ve brought it up here.

Posted by: Tom Leinster on December 18, 2012 9:59 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Caveat: I’m not even a semi-specialist in set theory or category theory, just an interested generalist.

I think this is nicely done. I found it very readable. Not an objection really, but there was one part that made me wonder.

In your “Reactions to an earthquake” section, you write:
“[T]he ten axioms above are such core mathematical principles that an inconsistency in them would be devastating.”

But what about choice? As we all know, choice leads to some strange consequences. So I wouldn’t be surprised that if ZFC were found to be inconsistent, choice might be part of the issue, and that maybe mathematicians would retreat to some weaker form of choice. Even I’ve heard that the consistency of ZFC is equivalent to the consistency of ZF, so I get that weakening choice couldn’t be a solution in itself: it would have to be combined with weakening something else. In particular, I was wondering is that consistency result also true for bounded ZFC?

In other words, is it possible that bounded ZF is consistent, but bounded ZFC is not? I have no idea whether that would be a common question from readers, or idiosyncratic to me.

Posted by: Crust on December 18, 2012 3:59 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Is it possible that bounded ZF is consistent, but bounded ZFC is not?

No, ZF and ZFC are equiconsistent. This was shown by Gödel: in every model of ZF the constructible sets form a model of ZFC.

Posted by: François G. Dorais on December 18, 2012 4:10 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks, Francois. I think I may have misstated my question. I’m curious: are Tom’s first 9 axioms known to be equiconsistent with the list of 10 including choice? (I said “bounded ZF” but I see the correct term is “bounded Zermelo” if that makes a difference.) Or are you saying this equiconsistency follows from Godel’s proof of the equiconsistency of ZF and ZFC? (Note per Tom, bounded Zermelo is not known to be equiconsistent with ZF.)

Tom, a typo: On p.8, “there is only place” should read “there is only one place”.

Posted by: Crust on December 18, 2012 5:10 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Ah, I had somehow missed bounded. The construction of L goes through in very weak subsystems of set theory, so adding choice is not often an issue. For bounded Z with collection, everything is fine. For bounded Z, there are serious issues with the construction of L and many other things. See A. R. D. Mathias, The Strength of Mac Lane Set Theory, for a detailed account.

Posted by: François G. Dorais on December 18, 2012 5:44 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Tom, a typo

Thanks very much! Fixed now.

Posted by: Tom Leinster on December 18, 2012 7:47 PM | Permalink | Reply to this

Re: Rethinking Set Theory

As a neophyte, I may be getting a bit ahead of myself, but if I’m understanding things correctly…
If there’s a contradiction in ETCS, then we can get a contradiction in ZFC by building a model of ETCS in ZFC. So the answer to your question should be “choice is not a problem.” Is there something wrong with this intuition?

On another note, I found this incredibly easy to digest. Almost too easy considering my initial perception of ETCS as something deep and mysterious. So clearly it was a job well done!

Posted by: Cory on December 18, 2012 8:32 PM | Permalink | Reply to this

Re: Rethinking Set Theory

If you are interested in making these axioms even more mundane looking, you might consider rephrasing axiom 7 in terms of set-builder notation.

Then you can explain ETCS as saying that sets support products, powersets, and comprehension, all of which are utterly familiar operations. I believe Paul Taylor suggests an approach like this in Chapter 2 of his Practical Foundations of Mathematics, which he dubs “Zermelo Type Theory”.

Also, is axiom 3 really necessary? It seems to be implied by 9 and 7, by taking the subset of the natural numbers {x|s(x)=0}\{x \in \mathbb{N} \;|\; \mathrm{s}(x) = 0\}.

On a related note, you might want to explicitly show the construction of disjoint unions. Since it involves a double-powerset construction, I find it to be a surprisingly big hammer for cracking a rather small nut.

Posted by: Neel Krishnaswami on December 19, 2012 8:48 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Hi Neel, nice to see you here!

Also, is axiom 3 really necessary?

Good point! I think you also need to invoke Axiom 4 to make sure s 1(0)s^{-1}(0) is actually initial. This is worth looking into…

On a related note, you might want to explicitly show the construction of disjoint unions. Since it involves a double-powerset construction, I find it to be a surprisingly big hammer for cracking a rather small nut.

Yes, but that construction is absolutely fascinating!

The construction is much too long if done carefully, but I think it’s worth outlining it. Pointing out that XX and YY embed disjointly into P(X)×P(Y)P(X)\times P(Y) is easy. Since the existence of the union of two subobjects in ETCS is very believable, I think a parenthetical remark explaining that this is more complicated to prove in ETCS than one would think is enough.

Posted by: François G. Dorais on December 19, 2012 12:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

The construction is much too long if done carefully, but I think it’s worth outlining it. Pointing out that XX and YY embed disjointly into P(X)×P(Y)P(X) \times P(Y) is easy. Since the existence of the union of two subobjects in ETCS is very believable, I think a parenthetical remark explaining that this is more complicated to prove in ETCS than one would think is enough.

Assuming that people are referring to the proof given in the notes I wrote up, I’d like to add that it’s quite possible (even likely) that that proof is much more complicated (or tormented) than it should be, that it probably could be improved if someone would take the trouble. (And still retain the elementary and “common-sense” character, rather than take the usual detours through Beck’s theorem on monadicity, etc.). Part of the problem could be notational.

Category theorists seem generally to be very proud of the extent to which Occam’s razor has been applied to the topos axioms, that you get so much for seemingly so little (finite limits and power sets). The impression I get is that most everyone else is acutely uncomfortable with the amount of labor (or technical ingenuity) required just to get the basic comforts in life like coproducts. I confess that I’ve never gone through Lawvere-Rosebrugh’s Sets for Mathematics, but I take it they chart a much less demanding course, as is the case for the original article on ETCS (as reprinted in TAC).

Posted by: Todd Trimble on December 19, 2012 3:30 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I really don't like the 1900-era fascination with minimising axioms. Yes, disjoint unions and quotient sets can be constructed from power sets, cartesian products, and solution sets of equations (and that's very interesting to know), but that doesn't mean that they should be. I would include them as separate axioms. In predicative mathematics (where you don't have power sets), you have to do it this way.

(This is like making the empty set an axiom rather than deducing it from the axiom of infinity, which I discussed earlier; finitists still believe in the empty set.)

Posted by: Toby Bartels on December 20, 2012 7:53 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Of course, the empty set, disjoint unions, and quotient sets are all just particular inductive types (well, quotients are a higher inductive type).

Posted by: Mike Shulman on December 20, 2012 9:12 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I really don’t like the 1900-era fascination with minimising axioms.

I wouldn’t say I’m fascinated, but eliminating redundancy in a list of axioms is surely a standard thing to do. Of course, there’s a trade-off. The more economical your axioms are, the more time you have to spend proving lemmas. On the other hand, you only have to do that once, and the benefit of economy is that whenever you meet something that you think might satisfy your axioms, you’ve got less to check.

I have had idle daydreams about teaching a course or writing a book on ETCS. I reckon what I’d do is state the existence of disjoint unions as a theorem, but omit the proof (for a course) or relegate it to an appendix (for a book). This would encourage the student/reader to treat it more like an axiom.

Posted by: Tom Leinster on December 21, 2012 5:54 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I would do the opposite. I would put down all of the basic things that ought to hold (at least if there's only finitely many of them), and let my definition state that all of them must hold. Then I would have a lemma (proof deferred to the appendix maybe) that anything satisfying axioms 1–6 must also satisfy axioms 7–12 (just making up numbers here). This is a useful lemma, after all, when checking that one has a model.

One reason is that the minimal list of axioms is not unique. Another useful lemma may be that anything satisfying axioms 3–8 must also satisfy the others. There may be a few useful lemmas like this. You can see this in action in the defintion of linear order on the nLab.

Posted by: Toby Bartels on December 23, 2012 11:48 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think there’s some point to this. One thing the usual “parsimonious” definition of topos does is privilege constructions on the “right adjoint side” (finite limits and power sets) over those on the “left adjoint side” (e.g., finite colimits). I have a vague memory of a conversation I once had with Lawvere about a possible “left adjoint” presentation of the notion of topos (sorry I don’t recall details).

Posted by: Todd Trimble on December 23, 2012 12:52 PM | Permalink | Reply to this

Re: Rethinking Set Theory

It's pretty common that the axiom of empty set follows from the axiom of infinity; we have that in ZFC too. But I don't like removing empty set from the list. You don't want to tempt people to say things like ‘Finitist mathematics is useless, because without infinity, you don't even have the empty set.’.

Posted by: Toby Bartels on December 20, 2012 6:57 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Neel wrote:

is axiom 3 really necessary?

Yes. The terminal category is a model of the other 9 axioms, but it doesn’t satisfy Axiom 3. The sole purpose of this axiom is to outlaw that trivial model.

I don’t know what goes wrong if you attempt to deduce it from Axioms 7 and 9, but something must — unless you’ve just discovered an inconsistency.

On a related note, you might want to explicitly show the construction of disjoint unions.

I might, I might; I probably do! I think this is a really interesting point. But, like a diligent dieter, I’m struggling hard to keep my pagecount down, and this means restraining myself from indulging in too many interesting points. If I were going to do it at all, it would be a very quick summary along the lines that François suggests.

Posted by: Tom Leinster on December 21, 2012 5:43 AM | Permalink | Reply to this

Re: Rethinking Set Theory

There’s an interesting tension here too between internal and external notions. The other axioms do imply the existence of an initial object, as part of the theorem that any elementary topos has finite colimits: concretely, you take the equalizer of a couple of canonical maps P1PPP1P 1\rightrightarrows P P P 1. However, this only gives you a set which ‘has no elements’ in the internal sense. The role of axiom 3 is to identify this ‘internal emptiness’ with the ‘external emptiness’ as expressed by the language in which you are talking about the sets.

Axiom 4 can be seen a playing a similar role. It’s always true internally that a function is determined by its action on elements: axiom 4 ‘externalizes’ this property. And there are also some hidden companions to axiom 3 relating to other colimit notions: every element of A+BA+B comes from A or from B, and if XYX\to Y is epi then every element of Y comes from some element of X. These follow accidentally from the other axioms when the logic is classical, but not constructively – I think making them explicit also carifies the role of axiom 3.

I also have to say, this discussion is making clear to me in a new way the advantage of a type-theoretic approach in which logic isn’t taken as an external given before you start stating axioms. Otherwise, so much work has to go into managing the interface between the logic and the sets! (-:

Posted by: Mike Shulman on December 21, 2012 12:41 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks – that was a very helpful comment!

I was indeed thinking in the internal logic, and so was surprised by the fact that internal existence of an empty set didn’t imply external existence.

Posted by: Neel Krishnaswami on December 21, 2012 1:48 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I spent some time trying to write out what I interpreted as Neel’s proof while thinking through what it said about the terminal category. Here is a roughly outline of how it went for me:

In this version of the natural numbers axiom, we don’t take it as axiomatic that 00 is not in the image of SS. So I better prove that. How do I do that…

Let XX be a set with two elements, {0,}\{ 0, \infty \}, and the map r:XXr: X \to X giving r(0)=r(0) = \infty, r()=r(\infty) = \infty. Then, if I give the axioms their standard interpretation and apply Axiom 9, I can see that there is no place to map a predecessor of 00 within XX. Maybe I can make that proof work within the theory.

I need to prove that there is a set with 22 elements in the first place. Axiom 88 conveniently has a set called 2\boldsymbol{2}. But Tom says that’s it’s not obvious that 2\boldsymbol{2} has two elements. And, in the terminal category, it has only one element.

Can I prove that 2\boldsymbol{2} has two elements? I need to build two maps 12\boldsymbol{1} \to \boldsymbol{2}. By Axiom 88, I need two injections into 1\boldsymbol{1} (and I need to show they are different). One of them can be 11\boldsymbol{1} \hookrightarrow \boldsymbol{1}, and the other one is…

Ah, now I need Axiom 3.

I second the statement that Mike’s comment is very useful. I’m used to thinking in schemes over a base SS, so I am used to internal products being a little funny, but I’m not used to the internal empty set being funny! For me, it takes some getting used to to treat something internally which is so basic to logic.

Posted by: David Speyer on December 21, 2012 3:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

The paper says “For instance, not every continuous surjection between topological spaces has a section…” This is the only use of ‘section’ to refer to what is otherwise carefully referred to as a ‘right inverse’. It’s a minor point, but it distracts from what is otherwise a very smoothly written paper.

Posted by: Carl Feynman on December 20, 2012 6:32 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks. I need to think about this whole right inverse/section terminology business, in the light of this conversation. What I had in mind was that “section” is most often used in the context of topology. (I see that Wikipedia appears to agree.) But anyway, thanks for alerting me to this bump in the road.

Posted by: Tom Leinster on December 21, 2012 3:17 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I think category theory makes replacement particularly natural, even though it’s avoidable. Category theory naturally leads to the distinction between diagrams that are “small” and “large”. Small versus large suggests a kind of cardinality distinction, and in VBG you get a clean distinction: Every diagram that is the same size as a set is small, otherwise it is large.

Without replacement or some substitute, you can form diagrams that are countable, and yet are “large”, in that you can’t realize them as sets. For example, the limit diagram for X x PX x PPX x … is not a set. (By which, I mean there are models where it’s a set, and models where it isn’t.) As infinite diagrams go, countable ones seem small to me. This isn’t fatal, but it seems less attractive as foundations to me.

Posted by: Walt on December 20, 2012 9:15 AM | Permalink | Reply to this

Re: Rethinking Set Theory

A good example! This is related to what I meant in my comment above by ‘using the wrong notion of family of sets’. Arguably, the ‘right’ notion of ‘I-indexed family of sets’ is not a formula expressing a relationship between elements of I and sets, but rather a function p:XIp:X\to I (whose fibers are the sets being indexed). This (or something equivalent) is really the only sensible meaning if a ‘family of sets’ is to be a notion within the theory. Membership-based set theory is usually done with an uneasy marriage between notions in the theory, which are sets, and notions outside the theory (particularly first-order formulas), which forces you to use replacement to bridge the gap; categorical set theory promotes a cleaner point of view. (And type theory enforces a cleaner point of view.)

With this notion of ‘family of sets’ as the basis for a notion of ‘diagram’, it is immediate that every small (i.e. set-indexed) diagram has a limit and a colimit. The problem with X×PX×PPX×...X \times PX\times PPX\times ... is then not that the limit doesn’t exist, but that the diagram doesn’t exist. This isn’t of course very different from how you described it as ‘countable yet large’, but I think it’s a slightly better point of view — there just is no such thing as a ‘large diagram on a small category’. This makes abstract category theory, for instance, a lot more comfortable.

I do agree, though, that that countable diagram should exist! But I’ve come to regard its nonexistence not so much in terms of a missing collection/replacement axiom, but in terms of an insufficiently powerful induction principle. For the natural numbers to be worthy of the name, you should be able to define anything you like recursively, including not just functions, but families of sets. (In type theory, the latter is called a ‘large elim’, and usually derived from the existence of a universe type, but it can also be postulated separately.)

Posted by: Mike Shulman on December 20, 2012 1:32 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Interesting thoughts, Mike. I was thinking of something tangentially related…

I was trying to find good practical test cases for ETCS. An interesting one I found this morning is:

To what extent does ETCS prove the existence of free algebras for endofunctors (W-types)?

I don’t know the answer to this.

Mike seems to suggest that postulating the existence of all these and similar stuff might be a viable alternative to replacement.

Posted by: François G. Dorais on December 20, 2012 4:55 PM | Permalink | Reply to this

Re: Rethinking Set Theory

W-types can be constructed in any elementary topos, hence a fortiori in ETCS: you can code up trees as sets of finite sequences.

What can’t be constructed in ETCS, and in fact not even in ZF, is free algebras for arbitrary (infinitary) algebraic theories. Andreas Blass proved that if all uncountable cardinals are singular (which is consistent with ZF, assuming the consistency of some large cardinal principle), then there is an infinitary algebraic theory without an initial algebra.

Mike seems to suggest that postulating the existence of all these and similar stuff might be a viable alternative to replacement.

Indeed, that is exactly what we do in type theory, and there I don’t think anyone has ever felt the need for a “replacement axiom”. In type theory with higher inductive types, we can even construct free algebras for algebraic theories as above, hence going beyond ZF without needing any choice principles.

The more we explore what higher inductive types can do, the more I am convinced that many or most uses of axioms like replacement and choice are just workarounds that you’re forced into because of not having higher inductive types. (-:

Posted by: Mike Shulman on December 20, 2012 9:09 PM | Permalink | Reply to this

Re: Rethinking Set Theory

What I was thinking about is actually a broader question. To be more specific: how much of Max Kelly’s A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on survives if we work in ETCS instead? (Kelly uses ZFC with an inaccessible, but that’s only a matter of convenience, so we can ignore that.) I’m not expecting a full analysis of this huge paper, I just want to point in a direction for relevant test cases.

Posted by: François G. Dorais on December 20, 2012 9:46 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Well, Kelly’s construction is essentially how you prove in ZFC that all algebraic theories have free algebras. So certainly not all of it survives in ETCS or ZF. I’m not sure what more could be said. I mean, certainly the conclusions are true in some cases, but I don’t see any natural restrictions one might impose that would make the method work.

Posted by: Mike Shulman on December 21, 2012 1:34 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Yes, I struggled for some time trying to figure out what, if anything, replacement means in type theory. When I realised that it meant that one could construct types or sets (not just subsets and elements) recursively, it felt like a great secret had just been revealed.

Posted by: Toby Bartels on December 20, 2012 7:04 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Hoping not to hijack this multicoloured thread, I’d like to get a clear picture of this systematically seeing a family of sets as the fibres of a map, with an eye towards sheaf theory (of which I’m currently trying to get an idea).

The standard way to talk about sheaves is the presheaf notation; so the sheaf of smooth functions on a smooth manifold XX, say, is a functor τXSets\tau X \to \mathrm{Sets}. This is, to me, already a dissatisfying notation because it mentions the large category of sets even though the data involved is small. For more or less this very reason, it composes badly: Considering also the sheaf of 1-forms on XX, which is equally a functor τXSets\tau X \to \mathrm{Sets}, on what object do you define the differential?

The germ/stalk notation answers this question: It packages all the data into the space over XX of germs of smooth functions (1-forms, respectively), and the differential is now at least a morphism in Top/X\mathrm{Top}/X.

But if we didn’t know that our presheaves are actually sheaves, we could still decide for the following notation: Let EE be the disjoint union UτXC (U)\bigsqcup_{U \in \tau X} C^\infty(U), and let p:EτXp : E \to \tau X be the projection according to that disjoint union. Let similarly EE' be the disjoint union UτXΩ 1(U)\bigsqcup_{U \in \tau X} \Omega^1(U), with projection p:EτXp' : E' \to \tau X. Those sets E,EE,E' over XX are even more “spread out” (hah) than the spaces of germs.

My question now being, can EE and be EE' be endowed with some obvious structure such that the differential becomes a morphism in SomeCategory/τX\mathrm{SomeCategory}/\tau X? Or would this even be a sensible thing to do?

Posted by: maltem on December 22, 2012 1:17 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Perhaps you are looking for the notion of internal presheaf?

Posted by: Mike Shulman on December 22, 2012 6:55 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I’ll look into it.

Posted by: maltem on December 23, 2012 11:41 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Hi Tom, thank you for your clear introductory account on ETCS. From time to time I’m also thinking about foundations but for a different reason, see 2 below. Here are my two cents.

1. This has already been mentioned. From the first day on we are taught to insert elements x into functions f from the right, f(x). So composition, too, is from right to left. But, we are writing from left to right, and so are composed arrows if we draw them. So what is the history behind right to left composition?

2. I think the section “Why rethink?” doesn’t answer this question fully. What makes me feel uncomfortable whenever I think about foundations is, that there are plenty of statements which cannot be decided in ZFC. See http://en.wikipedia.org/wiki/List_of_statements_undecidable_in_ZFC. For example, given an abelian group G, which has the property that whenever you have a surjective homomorpism B->G with kernel isomorphic to Z then this homomorphism has a section, you cannot decide whether G is free or not (which it is, if you demand countability of G). So this leads me to wonder about

3. possible reasons of undecidability. I have read of scenarios of inconsistency of the Axiom of Choice in comments above. But I want to take a step further. I was thinking of your paper on codensity monads and ultrafilters. Since you need a weak version of AC for proving the existence of non-principle ultrafilters, does this mean, that the codensity of FinSet->Set is undecidable in ZF? Or does it mean that ZF is necessarily a theory with finite sets? But then you demand in ZF the existence of a honest infinite Set N and I wonder whether such a honest infinite set really makes sense? What I want to point at is the difference between pro-finiteness and honest finiteness. Here
http://en.wikipedia.org/wiki/Potential_infinity
the latter is called “actual infinity”. I mean, it is a difference if you can repeat something indefinitely or whether you actually can finish such a never ending repetition. And I think the last thing is something that is quite not real, at least unnatural. On the other hand, we just write down those truly infinite sets every day, but we’re always just working and thinking in strictly finite ranges therein.

4. Another thing that reminded my of your paper about codensity monads and ultrafilters: In Axioms 2 and 8, the numbers 1 and 2 play a prominent role. Whereas in the codensity paper, the number 3 pops up several times. So is there a way to model pro-finiteness in terms of 3? (Don’t take this last question too serious.) ;)

Posted by: Werner Thumann on December 20, 2012 2:33 PM | Permalink | Reply to this

Re: Rethinking Set Theory

what is the history behind right to left composition?

I don’t know. My impression is that the movement to reverse the convention, writing (x)f(x)f or xfx f instead of f(x)f(x), was strongest in the early 1970s. I know there are some readers here who prefer it, but I imagine they feel quite lonely in that preference.

(You may have noticed that this corresponds to two different idioms for certain types of software. I first noticed it when I was using a “paint” type program as an undergraduate. In some such programs, you choose the tool [function] first and then the object to apply it to — e.g. choose “bucket fill” and then the area you’re filling. In others, it’s the opposite way round: object then function.)

  1. I think the section “Why rethink?” doesn’t answer this question fully. What makes me feel uncomfortable whenever I think about foundations is, that there are plenty of statements which cannot be decided in ZFC.

Elsewhere on this thread, Mike evoked a helpful comparison between set theory and classical geometry, which I think makes the existence of undecidable statements seem less exotic. I also find it demystifying to consider the analogy (and more!) between undecidable statements and non-computable functions.

The “Why rethink?” bit was only about the disagreement between the meanings of “set” as used by most mathematicians and “set” as used in ZFC. It’s a somewhat subjective matter and I’m sure some people disagree with what I wrote, but to me it provides a good reason for “rethinking” — that is, finding an approach to set theory that reflects how mathematicians actually treat sets more accurately than ZFC does.

Since you need a weak version of AC for proving the existence of non-principle ultrafilters, does this mean, that the codensity of FinSet->Set is undecidable in ZF?

It’s provable without any form of choice that the codensity monad is the ultrafilter monad. The inclusion FinSetSetFinSet \hookrightarrow Set is codense iff the codensity monad is the identity (more or less by definition), iff every ultrafilter is principal (by the previous sentence). Thus, FinSetSetFinSet \hookrightarrow Set is codense iff every ultrafilter is principal. So, the answer to your question is yes.

As for the role of the number 3, I don’t have anything intelligent to say!

Posted by: Tom Leinster on December 21, 2012 6:19 AM | Permalink | Reply to this

Re: Rethinking Set Theory

That’s a nice draft Tom, I like it.

My only other feedback is about the typesetting. I found the emboldened, centred, unnumbered subsection heading difficult to parse as headings; I got confused in Section 2 between the headings and the numbered axioms. The subsection headings almost look like midsection ‘slogans’. I don’t know what would have lessened the confusion, maybe left-justifying the headings, or numbering them.

Posted by: Simon Willerton on December 20, 2012 10:22 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks. I tinkered with the formatting for a long time, and I’m still not sure I like it: page 4 in particular (in the section you mention) looks messy.

For those subsection headings, I took my cue from newspapers, which sometimes split up long stories with centred, bold subheadings. Then again, I’ve seen magazines do the same thing but left-justified. Perhaps I’ll follow your suggestion and try that (again!).

Posted by: Tom Leinster on December 21, 2012 3:28 AM | Permalink | Reply to this

Re: Rethinking Set Theory

After Axiom 6, do you want to note that function sets are essentially unique, as you do after Axiom 7 for inverse images?

Posted by: Toby Bartels on December 23, 2012 12:39 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Good question. It’s something I wondered about for a while (and ditto for axiom 8 and even axiom 3). My decision was not to, simply because it gets repetitive saying the same thing so many times. But I’m not sure I’ve made the right decision. I should think about it some more; thanks for flagging it up.

Posted by: Tom Leinster on December 23, 2012 5:27 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I just posted something related on my research site: Back to Cantor?

Though it is intended as part of this discussion, I posted it elsewhere since the aim diverges a little from the intended topic here and I also wanted to reach out to set theorists.

Posted by: François G. Dorais on December 28, 2012 7:13 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Materialistic structural set theory

Is material set theory vs structural set theory analogous to quantitative vs qualitative, or geometry vs topology? There are metric spaces, topological spaces and metrizable spaces. So what about material sets (or labelled sets), structural sets (or unlabelled sets) and materializable sets (or labelable sets). An atom is the same as a singleton lablelled set. Questions of membership and inclusion require labellings. What is a labelling? Is a labelling just a function from something to something? When does it make sense to talk about the automorphisms of a group if the elements aren’t labelled and relabelled? In “Combinatorial Species and Tree-like Structures” can the definition of species be extended to infinite sets. Would infinite species have anything to do with unifying structural and material viewpoints.

Sets are unstructured but surely “unstructure” is a form of structure in the same way that zero is a number or that a totally disconnected graph with no edges is still a graph.

From the “Back to Cantor?” post:

“find a reasonable unified foundation where structural sets and material sets happily live together as equals.”

Is an unlabelled set just a labelled set with the empty labelling?

Some quotes from “Species and Functors and Types, Oh My!” by Brent A. Yorgey:

“The theory of combinatorial species, although invented as a purely
mathematical formalism to unify much of combinatorics, can also
serve as a powerful and expressive language for talking about
data types.”

“The ability to relabel structures means that the actual labels we
use don’t matter; we get “the same structures”, up to relabeling,
for any label sets of the same size.”

“it is tempting to assume that labels play the role of the “data” held by data structures. Instead, however, labels should be thought of as names for the locations within a structure.”

“Although the formal definition of species is good to keep in mind
as a source of intuition, in practice we take an algebraic approach,
building up complex species from a small set of primitive species
and species operations.”

Posted by: Matstruc on December 28, 2012 11:28 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Dear Tom,

I am having hard time to think of your axiomatization as a real axiomatical system because it does not specify an alphabet and rules of constructing terms and propositions. For instance, your first data statement is, “Some things called sets,” but what are those things?

In the same vein, it is not clear to me where you speak in the language of your axiomatic system vs. speaking in a metalanguage. (It is even possible that you sneak through the back door some parts of the very set theory you want to axiomatize.) It looks like your four data statements on page 3 are formulated in the metalanguage (since they precede axioms), but it makes using phrases like “each set” and “all sets” suspect.

Max

Posted by: max on December 29, 2012 10:50 AM | Permalink | Reply to this

Re: Rethinking Set Theory

You seem to suggest that, in the ZFC view, you do know, or have some sense, of “what the sets are”. I would modify that notion, that you have names for lots of the sets, and imagine most of the rest as having generalized names in a similar way; but that most of your names for ZFsets are actually just fragments (on one side) of the \in relation. Now, that may sound strange, except that when building models for exotic variations of ZF (or others) one frequently starts with a subclass or particular set and restricts the standard \in to that — and it may well occur that the resulting \in-structure is not \in-transitive in the original universe, which means that the old names for everything in the new model are wrong with respect to the new model. This is one of those things set theorists do that most mathematicians need never worry about. Another such thing is to change the \in-relation of interest (as here).

On the other hand, there are plenty of basic (and suggestive) names for many sets in Tom’s presentation of ETCS; for instance, 0,1,2,\mathbf{0},\mathbf{1},\mathbf{2},\mathbb{N}; and plenty of ways for building sets that fit in particular diagrams, such as f 1(z)f^{-1}(z) whenever ff is the name for a function and zz is the name for a (possibly generalized) element of ff’s codomain.

Posted by: Jesse C. McKeown on December 29, 2012 4:09 PM | Permalink | Reply to this

Re: Rethinking Set Theory

The theory has an ordinary first-order language formalization. Tom is just trying to provide an intuitive pedagogical presentation.

Posted by: Walt on December 29, 2012 5:38 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Max: there’s nothing hidden. The short answer (as Walt mentioned) is that this is a first order theory, just as ZFC is. The last paragraph of the introduction says a bit more along these lines. It sounds as if your points of confusion about this are really points of confusion over first order theories in general.

If you want to see a presentation of ETCS in pure logical syntax, here’s one by Colin McLarty. It’s not the same in every detail as mine, but it’s equivalent and it should give you the idea.

Walt goes a little further than I would: while I do hope I’ve conveyed some intuition and my paper is intended to be pedagogical, it’s also intended to be precise. It’s true that “some things” doesn’t sound precise, but I think it has exactly the same content as the corresponding formal logical expression.

If that doesn’t clarify things, I suggest the following. Don’t think of set theories (such as ZFC or this) as describing a world of sets that “exists” in some sense, because while you may indeed hold the opinion that they do exist, that leads into unnecessarily murky philosophical waters.

Instead, simply interpret them as a declaration of what the word “set” (and related words such as “element” and “function”) will be taken to mean. For example, if someone says “we will assume ZFC”, they’re really saying “I will use the words set and element to mean any things satisfying the ZFC axioms”. Ditto for ETCS, with “function” in place of “element”.

Posted by: Tom Leinster on December 31, 2012 12:24 AM | Permalink | Reply to this

Re: Rethinking Set Theory

For what it’s worth, I didn’t mean to imply that your paper was imprecise.

Posted by: Walt on December 31, 2012 11:37 AM | Permalink | Reply to this

Re: Rethinking Set Theory

No problem. And Happy New Year, all!

Posted by: Tom Leinster on December 31, 2012 3:07 PM | Permalink | Reply to this
Read the post On Leinster’s “Rethinking set theory”
Weblog: Asaf Karagila
Excerpt: There has been a lot of recent discussions regarding Tom Leinster’s paper “Rethinking set theory” (arXiv). Being an opinionated person, I only found it natural that I had an opinion on the paper. Now that I have a blog, I have a place...
Tracked: January 4, 2013 10:24 PM
Read the post Back to Cantor?
Weblog: François G. Dorais
Excerpt: Set Theory has a fantastic and legendary history. At the end, it left us with ZFC, which is currently recognized as the foundation of mathematics. This state of affairs is arguably one of the best possible outcomes for the foundational crisis that plag...
Tracked: January 4, 2013 11:12 PM
Read the post From Set Theory to Type Theory
Weblog: The n-Category Café
Excerpt: Starting from set theories like ZFC and ETCS, trying to take the best of both worlds leads us naturally to univalent type theory.
Tracked: January 7, 2013 6:58 AM

Re: Rethinking Set Theory

Interesting; I believe I know what the intersection of Π and R is: it is empty.

Meaning, when we model real numbers in ZFC, we represent them as equivalent classes of sequences of rational numbers. Π consists of such sequences that converge… well, you know. R consists of such classes. This is one model, of course.

Sorry, this sounds primitive, but at least it answers the question in your article.

Posted by: Vlad Patryshev on January 9, 2013 7:34 AM | Permalink | Reply to this

Re: Rethinking Set Theory

when we model real numbers in ZFC, we represent them as equivalent classes of sequences of rational numbers.

A couple of years ago I gave a seminar about this stuff at the University of Barcelona, and got an unexpectedly hot reception from some of the set theorists in attendance. This didn’t make for the easiest afternoon, but I’m glad it happened that way, because it taught me a lot about how to present this material without unnecessarily fanning flames.

One of the comments was from the set theorist Joan Bagaria (who, I hasten to add, was absolutely calm and polite). He helpfully pointed out that ZFC itself is simply an axiomatic system, and says nothing about how to encode mathematical objects as sets. I knew this perfectly well, but I’m sorry to say that in my talk I’d been sloppily using the term “ZFC” to encompass both things at once. (In my paper, I use terms like “the traditional approach to set theory” instead.)

So, “when we model real numbers in ZFC” doesn’t really make sense. There’s no modelling of anything going on in ZFC. I guess you really mean “when we model real numbers as sets”, but then ZFC hasn’t got a lot to do with it. For example, in ETCS (the axiomatization explained in my paper), real numbers are modelled in the same way.

As I guess you know, there are actually many ways of modelling real numbers as sets. The way you describe is one. Dedekind cuts are another (giving rise to a few specific options, depending on exactly what you take the definition of cut to be). There are others too.

at least it answers the question in your article.

I wouldn’t agree. You’ve taken a particular set S πS_\pi encoding the real number π\pi, and a particular set S S_{\mathbb{R}} encoding the set \mathbb{R}, and you’ve answered the question “what is S πS S_\pi \cap S_{\mathbb{R}}?” This isn’t necessarily the same question as “what is π\pi \cap \mathbb{R}?” That is, whether one regards those as the same questions reflects one’s opinions about foundations; I would say not.

Posted by: Tom Leinster on January 10, 2013 3:39 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Let me respond on something which you wrote here. I agree with Joan Bagaria (whom I had the absolute pleasure of meeting when he came to Israel last year). ZFC merely described what are the properties we expects from sets to have. How we use them is a whole other story.

But what you said in your comment. The question $\pi\cap\mathbb R$ requires further clarification: how do you encode $\pi$ and how do you encode $\mathbb R$? Depending on the encoding we chose for each set. It is further the point that we only care that the underlying set is going to be of the correct cardinality, so we can stick whatever elements we want in there as long as they don’t contradict the axioms.

We can decide to use an encoding of $\mathbb R$ in which $\pi\cap\mathbb R=\mathbb Q$. Strangely sound decision, but we can make all sort of changes and replacements and have certain numbers hold all sort of crazy data (we can encode the algebraic field extensions of $\mathbb Q$ which are subextensions of $\mathbb R$ as transcendental numbers. How nuts is that?? :-))

But the point, it seems to me, that many people “on the other side of the fence” (so to speak) have a problem with the fact that the question $\pi\cap\mathbb R$ can be given an appropriate context. They want to eradicate this possibility. Under no circumstances one should ask what is the intersection of a real number with the collection of real numbers; or whether or not an ordered pair is a subset of an integer.

There are reasons to favour and reject each of the sides, and ultimately one should do what one feels is right. If type casting “errors” are troubling your sleep at night, no one is stopping you from using type theory; but if you have no problem with them then no one is stopping you from thinking about everything in terms of sets.

Posted by: Asaf Karagila on January 10, 2013 11:18 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Just a quick little note: if you want the LaTeX to render, you need to use an appropriate text filter. I usually use “itex to MathML with parbreaks”, but Markdown with itex to MathML also works (with some slight differences in handling paragraph breaks).

Posted by: Todd Trimble on January 11, 2013 1:31 AM | Permalink | Reply to this

Re: Rethinking Set Theory

I very much enjoyed the paper. It’s one of the most accessible expositions of ETCS I have read and it deserves to be read widely.

In particular I am quite happy that next time I teach our “Introduction to proofs” course, I will not feel guilty about treating functions as primitives rather than as a set-theoretic constructs.

I have a question: ETCS seems silent on how to treat collections of large size, e.g., the collection of all groups or the forgetful functor from groups to sets. Is there an axiomatic system that is like ETCS in spirit and handles universes?

Posted by: Eugene Lerman on January 11, 2013 4:23 PM | Permalink | Reply to this

Re: Rethinking Set Theory

It’s very kind of you to say so. Thanks.

I have a question: ETCS seems silent on how to treat collections of large size, e.g., the collection of all groups or the forgetful functor from groups to sets.

Yes, indeed.

Is there an axiomatic system that is like ETCS in spirit and handles universes?

Others here will do a better job of answering that than I could. In short, (i) people have certainly tried to create such a system, and (ii) there is a point of view that this isn’t the right thing to do. That point of view says that it would be better to axiomatize the category of categories (as opposed to classes, say). Lawvere proposed such an axiomatization (e.g. see this MathOverflow question); it had some mistakes that I think later got fixed. A variant of that viewpoint is that one should axiomatize the 2-category of categories instead (e.g. see Mike Shulman’s answer to that MO question).

Posted by: Tom Leinster on January 11, 2013 5:18 PM | Permalink | Reply to this

Re: Rethinking Set Theory

On (i), one key phrase to look for is algebraic set theory. However, AST in general is analogous to general topos theory, and I don’t know whether anyone has distilled out of it a “well-pointed” axiomatic system analogous to ETCS. The situation with 2-topos theory is similar. On the other hand, I should also point out that ETCS (and topos theory in general) has no problem with universes.

Posted by: Mike Shulman on January 12, 2013 6:54 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Thanks. Just to make sure I undrestand what you are saying, let me repeat what I think you have said.

One can add 4 axioms to ETCS and then, within this new augmented system, one can talk about functors say from the collection of all UU-small groups to the collection of all UU-small sets.

But for various reasons Algebraic Set Theory is prefered.

Is this roughly accurate?

Posted by: Eugene on January 13, 2013 6:22 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I think the first part is roughly accurate. Regarding the second, the line between AST and ETCS-with-universes is kind of fuzzy, just like the line between NBG/MK and ZFC-with-universes. I wouldn’t presume to say that one of them “is preferred” — certainly many people prefer to use universes, since that allows the “large objects” to behave just like the small ones. The merit of set/class theories like NBG/MK and AST’s “categories of classes” seems to be that it encourages a more conceptual separation between small and large, by making them behave differently. That is, you feel more free to think of the category of small groups as the category of “all” groups: since you’ve defined “set” to mean “small set” and used a different word “class” instead of “large set”, you can say that a group is a “set” with a group structure and then the category of small groups is the category of all groups.

Posted by: Mike Shulman on January 14, 2013 4:56 AM | Permalink | Reply to this

Re: Rethinking Set Theory

In particular I am quite happy that next time I teach our “Introduction to proofs” course, I will not feel guilty about treating functions as primitives rather than as a set-theoretic constructs.

I haven’t read the draft yet, but this was one of my main reactions to the post.

Posted by: Mark Meckes on January 13, 2013 2:36 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Does anyone have good ideas for where I might submit this?

(I tried Notices of the AMS, but they’re not interested.)

Posted by: Tom Leinster on January 14, 2013 2:36 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Posted by: Eugene on January 14, 2013 3:33 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Do you think the tone is right for l’Enseignement? I’m not familiar with many papers in there, but those I’ve seen are written in a style rather more formal and less journalistic than that of my own paper. I see you’ve got a couple of papers in l’Enseignement yourself, so you’re probably a good person to ask.

Does anyone think American Mathematical Monthly is a good idea? Would my article fit? It’s hard to see what the articles they publish are like, as they don’t seem to be available except to subscribers.

Posted by: Tom Leinster on January 14, 2013 5:22 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I think it’s a very good fit for the Monthly, although I understand they’re highly selective.

Posted by: Mark Meckes on January 14, 2013 7:30 PM | Permalink | Reply to this

Re: Rethinking Set Theory

For what it’s worth this arXiv search mostly returns papers that were published in the Monthly.

Posted by: Mark Meckes on January 15, 2013 2:23 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Clever! Thanks.

Posted by: Tom Leinster on January 15, 2013 2:53 PM | Permalink | Reply to this

Re: Rethinking Set Theory

By the way, there’s an excellent list of journals publishing expository work at MathOverflow. (Well, it’s excellent in the sense that it’s probably quite comprehensive, but it’s perhaps disheartening how sparse the field is.)

What I really want to know is whether there are any journals where my article’s likely to fit, in terms of level, style, length etc.

Posted by: Tom Leinster on January 14, 2013 5:30 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Having read the discussion of “expository journals” on at MathOverflow, let me say why I think L’Enseignement Mathématique is would be interested in an expository paper. On a number of occasions an editor there asked to have a look at a manusript and tell him if it was trully expository and of interest to a broad audience or was simply proving something.

I also have an experience with L’Enseignement Mathématique as an author. I have published two papers there. One wrote up and extended a little a result that was known but not available in literature. So while a number of people were using it, they had nothing to refer to.

The other dealt with a question that obsessed me awhile back — why would you want to think of orbifolds as stacks?

I am not a great fan of the Monthly. As an undergraduate, I found the papers there too hard. Nowdays, I mostly find them too recreational.

Posted by: Eugene on January 20, 2013 5:16 PM | Permalink | Reply to this

Re: Rethinking Set Theory

This paper may be of interest: http://www.jyb-logic.org/ens-cat.pdf
AT http://www.jyb-logic.org/start1.html

There seems to be some convergence between this author’s ways and yours.
The author Beziau (whom I do not know personally) may have some idea as your paper is good company with his.

Posted by: Jérôme JEAN-CHARLES on January 14, 2013 1:32 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Hi!

I do not understand why you put the “reactions to an earthquake”-section into the article. I do not see any objection in this section which distinguishes classical set theory from categorical set theory. You write “As the weaker system, the ten axioms are less likely to be inconsistent than ZFC”. Why do you contrast classical with categorical set theory here? It’s as easy to drop the axiom of replacement and I guess most people (set theorists or not) would agree that this axiom would be the first choice for dropping in the case of the earthquake.

Another question: “For example, McLarty [13] argues that no more is needed anywhere in the canons of the Grothendieck school of algebraic geometry…” But in the SGA universes are used, weren’t they introduced especially for SGA?

Best regards

Posted by: The User on January 18, 2013 6:49 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Hi!

Hi!

I do not understand why you put the “reactions to an earthquake”-section into the article. I do not see any objection in this section which distinguishes classical set theory from categorical set theory.

The point was that people’s reaction to the discovery of an inconsistency in a list of set-theoretic axioms is illuminating: it tells us something about how much they think their work actually depends on those axioms. It’s informative even as a thought experiment.

Suppose I make up a new set theory that has no connection with how anyone actually uses sets, then I discover an inconsistency in it. No one will care.

Now suppose I make up a new set theory consisting entirely of statements that mathematicians of all types use routinely, then discover an inconsistency in it. Everyone will care.

I argued at the beginning of the article that in certain respects, ZFC fails to reflect how non-set-theorists actually use sets — indeed, not only fails to reflect it but actively conflicts with it. This is why, I believe, most mathematicians wouldn’t feel that threatened if an inconsistency were found. (To be clear, I don’t claim ZFC has no connection with how anyone uses sets, just that it’s further from reflecting ordinary usage than is generally appreciated.)

On the other hand, every axiom of ETCS is a statement about sets that everyone believes makes sense. They are all principles used by mathematicians all the time. Were any one to fail, it would cause the most enormous upheaval.

As I said in the last paragraph of my paper, the question of strength is peripheral. Let’s say we adjust ETCS and/or ZFC so that the proof-theoretic strengths match exactly, in one of the ways described. An inconsistency can be found in one iff it can be found in the other.

Still, people can feel differently about an inconsistency in one versus an inconsistency in the other. I think that if ETCS was more widely known, people would be way more shocked by an inconsistency in it than an inconsistency in the equivalent fragment of ZFC, simply because the usage of “set” in ZFC is so different from how most people use it.

Posted by: Tom Leinster on January 19, 2013 12:46 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Hi,

But in the SGA universes are used, weren’t they introduced especially for SGA?

yes, they were used, but apparently not necessary. McLarty shows that derived functor cohomology only requires a reasonably weak set theory, and for concrete applications (including using etale cohomology) even only third order arithmetic or so is needed (plus the assumption of some standard uncountable ring like the complex numbers). I gather that this is the only (or at most, one of very few) place(s) in SGA where universes were really necessary. There is some discussion by knowledgeable experts at this MO question.

Posted by: David Roberts on January 21, 2013 1:28 AM | Permalink | Reply to this

Re: Rethinking Set Theory

Hello. Since a few years I was working on the same purpose of writing down a clean expression of set theory and the foundations of mathematics that more directly reflects and usefully inspires mathematical practice.

I had roughly the same criticism towards ZF(C), that is, mainly, that the encoding of everything as sets is awkward, so that a cleaner formalization should also accept pure elements, oriented pairs and functions in a more natural and practically useful manner.

My work is not finished yet but the first chapters are now ready and sufficient for a start.
(I just gave there an introductory “cheap” solution to represent the set of natural numbers, that consists in just adding to set theory the symbols and axioms of arithmetic ; I intend to give a more elaborate “justified” solution when coming to the exposition of universal algebra)

And I still remained satisfied of my approach, not even considering to change anything of it, after reading Tom Leinster’s article, who, in my opinion, beyond the mere merit of pointing out that ZF(C) is’nt perfect, doesn’t really have a better solution to offer.
I mean, while he avoids some aspects of the awkwardness of ZF as a representation of ordinary mathematics, he introduces some other cases of awkwarness instead. In other words, while I agree that
“ZFC fails to reflect how non-set-theorists actually use sets”
I would not agree with the idea that ETCS does any better for that same purpose.

[Three sentences removed here. I repeat: comments must be scrupulously polite. — TL.] Any ordinary mathematician, I guess, would think: of course composition isn’t a primitive concept ! Instead it is the fruit of a definition. Indeed, we first need to introduce functions in a way or another, somehow express that “functions can be defined by formulas”, and finally give a definition of composition by a formula. In these conditions obviously required for any approach that claims to fit with the ordinary practice of mathematics, I see no sensible way in which the associativity of composition can be regarded as an axiom. Instead, it is of course an easy theorem.

As a justification, it is proposed to reconstruct elements as “a special case of functions”. Well, sorry but, while it technically works, I cannot see how this can be seen less artificial than the traditional construction of ordered pairs as sets. (You may say this concept of “element” is technically simpler to define and use than the set for an ordered pair, but a fair comparison needs to relate these to the complexity of their intended meanings !)

I agree that categories are an interesting concept that can be used as a source of inspiration and tools to rebuild mathematics. I did it myself in my work. But it is just one concept among others that can be inspiring as well. Not THE concept that should be forcefully put forward as if it had to be the main concept, when in practice this one-sided enterprise sometimes complicates things away from ordinary mathematical practice, more than it simplifies them. (You can see my approach takes many other concepts, especially those of model theory, to provide more complete and balanced explanations and tools)

The article claims to not “[try] to replace set theory with category theory” and that “The approach described here is not a rival to set theory: it is set theory”. And prides itself of not putting the word “category” in its axioms, as if this alone would suffice to cancel its category-theoretical bias. Sorry to disagree, but in my view (and I guess many mathematicians would say the same), just deleting the word “category” cannot suffice to delete the fact: this approach has a much too strong category-theoretical bias, that can only remain unnoticed (among mathematicians) by, well, category theorists themselves, who developed such a professional bias of believing everything to be a category, that they no more notice this as a bias.

The article claims ETCS to be simple and natural, fitting the ordinary mathematical practice. But I think only category theorists can believe this, seeing it as fitting their own practice as category theorists. I guess the rest of mathematicians won’t find it preferable, as it does not reflect their practice any better than ZF does, and that this reaction will have good justifications, not just a matter of habbit or conformism.

Posted by: Sylvain Poirier on February 16, 2013 8:08 PM | Permalink | Reply to this

Re: Rethinking Set Theory

Sylvain, as Tom pointed out in his original post, it’s easy for these kinds of discussions to be heated, so it’s important to be extra-extra-polite. (I’ve been as guilty of violating this as anyone.)

In some ways, phrasing topics in terms of foundations detract from the mathematical content of them. For example, ETCS shows that there a first-order theory of “sets identified only up to isomorphism” that is equivalent to bounded Zermelo with choice set theory, and therefore can prove most results in mathematics. That means that you could rewrite those proofs into proofs entirely in the logic of “sets up to isomorphism” and functions between them. I would rather be set on fire than write out such a proof, but that is a perfectly interesting mathematical result, one that illustrates the extent to which mathematical results are invariant up to arbitrary choices of labeling. You could probably even state this as a precise theorem: if you have a theorem of bounded Zermelo with choice that does not mention elements, then it has a proof that does not mention elements.

Posted by: Walt on February 17, 2013 5:07 PM | Permalink | Reply to this

Re: Rethinking Set Theory

I posted a quote from your paper (about the infinite descent into subsets) to twitter and @michiexile brought up Dedekind cuts. Suppose you define π to be the set containing all rationals smaller than π. These rationals are in turn equivalence-classes of ordered pairs of integers; integers are equivalence-classes of ordered pairs of naturals; naturals use the Peano construction which terminates in {}. So the problem of infinite descent or circularity seems to end there. No?

Posted by: isomorphismes on August 10, 2013 11:39 PM | Permalink | Reply to this

Post a New Comment