## How would set theory research be affected by using ETCS instead of ZFC?

### Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

In "Rethinking Set Theory", Tom Leinster argues in favor of teaching axiomatic set theory via Lawvere's Elementary Theory of the Category of Sets with 10 axioms (but phrased in a way that requires no knowledge of category theory) which uses sets and functions as primitive elements compared to ZFC which uses sets and elements as primitives. (although if you really insist you can reintroduce elements as primitives at the expense of more clauses). This is weaker than ZFC but can be made equivalent to ZFC (or equiconsistent according to François G. Dorais) with the addition of a hardly ever needed 11th axiom.

http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html

How would set theory research be affected by using ETCS instead of ZFC?

Is ETCS less cumbersome than ZFC or more, or does it not matter? Does it make proofs longer/shorter or easier/harder?

Would automated theorem provers work better with ETCS?

To clarify, the question is not about the strength of ETCS: assume whatever is needed to bring ETCS up to strength with ZFC. The question is about practicalities of working with the ETCS axioms. I guess most mathematicians don't directly work with axioms of set-theory at all. So the question is: if your work does involve working directly with such axioms then what difference (if any) does it practically make to you as a set-theory researcher to use a different set of axioms that have equal strength. If I understand correctly the goal of Tom Leinster's paper was to reflect actual (non-set-theoretical)-mathematical practice but my question is about what set-theorists would do if they used these axioms. Assume also that for the purposes of this question ETCS refers specifically to the rephrasing used in this paper that is free of category and topos terminology. Perhaps this rephrasing should be renamed ETS. Adding replacement would give the name ETSR.

-

7
This seems a bit vague as an MO question (seen in its totally, parts might not be). In addition, this blog post was made today (or yesterday) and there is some discussion in the comments there. Why don't you participate in it or at least wait until that disucssion is over? (I did not yet vote to close but am considering it.) – quid Dec 18 at 14:19

1
Martin, what's not to love about the current definition of ordinals? It's wunderbar! – Asaf Karagila Dec 19 at 17:42

2
It's debatable that ETCS reflects actual non-set-theoretic mathematical practice, since it has a very restricted notion of object identity. For example, two sets don't share elements, since two functions with different codomains are not equal. The number 2 as a membrer of the natural numbers and the number 2 in the even numbers are not equal. There are standard ways around this, so maybe it's not important, but it is a departure from standard mathematical practice. – arsmath Jan 6 at 22:20

2
@arsmath: Even in ZFC, the natural number 2 is not the same as the real number 2; the former is usually the set $\{\emptyset,\{\emptyset\}\}$ while the latter is something like the set of all rational numbers less than 2. I think this is best considered an issue of "implicit coercions" which can even be made precise in a computer proof assistant; it's not really something specific to ZFC or ETCS. – Mike Shulman Jan 7 at 7:28

2
Mike Shulman has written new blog post "From Set Theory to Type Theory" golem.ph.utexas.edu/category/2013/01/… "My goal for this post is to start from material set theories (like ZFC) and structural set theories (like ETCS), and show how type theory can arise naturally out of an attempt to take the best of both worlds. At the end, I’ll argue that to really resolve all the problems, we need univalent type theory." – unknown (yahoo) Jan 7 at 14:04
show 13 more comments

## 7 Answers

No one has really addressed the question about automated theorem provers. I'm going to take this to refer more generally to computer-assisted mathematics, since fully automated theorem provers are still of very limited usefulness to a mathematician. There are a lot of good arguments that the best foundational system for these is neither ZFC (or its relatives) nor ETCS (or its relatives), but some variety of type theory.

This is mainly because type theory is so closely connected with programming and has good computation behavior, thus meshing very well with computers. Since the question is not about type theory, I won't say much about it; I just want to point out that ETCS is more like type theory than ZFC is. So although I kind of doubt that actually using ETCS in a computer proof assistant would be much better than using ZFC, learning to think in ETCS and do mathematics therein will probably stand you in better stead when you try to use a proof assistant based on type theory.

-

2
Isabelle/HOL is a concrete example of a proof assistant using type theory. I completely agree that ETCS is easier to understand as variety of type theory, in the sense that ETCS regards each set as its own type, and the "element" relation as a fact about the type of the element. However, I'm not yet convinced that learning to do mathematics in ETCS specifically is likely to help with proof assistant use. Natural-language math is done in a complex type theory already, so most mathematicians are accustomed to thinking this way. Learning formal type theory might be a better preparation. – Carl Mummert Jan 7 at 13:15
Learning formal type theory would undoubtedly be a better preparation! – Mike Shulman Jan 9 at 9:22

### You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

Some quotes:

"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’." , John Baez http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042716

"There are some problems with this sort of compromise where material and structural set theories cohabitate as equal alternative foundations. ... this kind of cohabitation model is actually not the best possible way to accommodate both the material and the structural perspective at the foundational level. ... what we end up doing is moving all the annoyances from both sides into the translation between the two ... it would be much more satisfactory to have a greater overarching foundation similar to Cantor’s universe that comprises both the material and structural views.", François G. Dorais http://dorais.org/archives/1135

"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" , Mike Shulman http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042933

"with ZFC is that it allows things like ⟨0,1⟩⊆3 which make no sense mathematically. I can assure you, though, that after you write one piece of code in x86 assembler which rewrites itself as it runs that manipulating all objects as binary and manipulating all objects as sets make perfect sense. This is what annoys me, in some sense, that people have an issue that in a system which allows you to encode everything as sets you can write some weird junk. Equivalently, this would be baffling to those people that if you write a piece of code in Common Lisp then the code itself is just a list and the program can manipulate itself (easier than to do that in assembler, I have to admit).", Asaf Karagila http://boolesrings.org/asafk/2013/on-leinsters-rethinking-set-theory/#comment-789

"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 0∈1 that do not have an intended meaning. If they have a meaning in a certain setting, then so be it.", Walt http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042992

"ETCS is one, but apparently not one that is very congenial to many traditional set theorists, for a variety of reasons, maybe one being that many set theorists “don’t like categories” (well, okay, but again I think that’s a pity). Maybe some set theorists don’t like the privileging of functions over elements (although one take is that functions are generalized elements).", Todd Trimble, http://boolesrings.org/asafk/2013/on-leinsters-rethinking-set-theory/#comment-798

"The same arrows aimed at ZFC can be easily turned at ETCS. It is equally easy to ask about “senseless things” which happen in ETCS but not in general mathematics. And this is not a critique against ETCS, but rather against the critique aimed at ZFC.", Asaf Karagila http://boolesrings.org/asafk/2013/on-leinsters-rethinking-set-theory/#comment-815

"the issue is that first-order logic is not “type safe”, and I would suspect that people who have had exposure to first-order logic take this for granted, while those who have not may find it surprising. The reason is that syntax, in first-order logic, is defined independently of semantics, so that whether a formula is well-formed (syntactically correct) is independent of what the formula means. ... This issue of “type safety” arises also in programming languages. Some languages, such as C, have little run-time type checking. I can take a 64 bit integer and treat it as an array of eight 8-bit characters – with implementation-defined results. ... In working mathematics we have humans to check that the formulas we actually write make sense – nobody accidentally writes 1∈sin in an analysis paper – so it is not clear that there is any real advantage to stronger “type checking” in the foundations.", Carl Mummert http://boolesrings.org/asafk/2013/on-leinsters-rethinking-set-theory/#comment-794

-
Dear Unknown, I think this should be a community wiki since others might want to add to this interesting sequence of quotes. (You can find the community wiki checkbox at the bottom right of the edit box.) – François G. Dorais♦ Jan 6 at 22:23
Good idea. Done. – unknown (yahoo) Jan 6 at 22:31

1
I have to admit a certain excitation to see quotes from the comments on my blog. Huzzah. :-) – Asaf Karagila Jan 6 at 22:35

In principle, nothing would be lost by working in ETCS+R instead of ZFC since the two theories are very nicely interpretable in each other. However, after talking it through with Mike Shulman (whom I thank very much) here, I came to the conclusion that much would be lost in practice.

The problem lies with the notion of wellfoundedness. Recall that a binary relation $R$ on a set $A$ is wellfounded if every nonempty subset $B$ of $A$ has an $R$-minimal element (an $x \in B$ such that $y \not\mathrel{R} x$ for all $y \in B$); this is a $\Pi_1$ statement in the Lévy hierarchy. In ZFC, an equivalent statement is that there is an ordinal valued rank function for $R$ on $A$ (a function $r:A \to \mathrm{Ord}$ such that $x \mathrel{R} y \Rightarrow f(x) \lt f(y)$ for all $x,y\in A$). This is a $\Sigma_1$ statement in the Lévy hierarchy due to the fact that being an ordinal is $\Delta_0$. In ETCS+R, there is no suitable equivalent to ordinals: two wellorderings of the same type are indistinguishable from each other. Because of this, in ETCS+R, the equivalent rank function statement is much more complex since one must explicitly say that the codomain of the rank function is a wellordering (for which we must use the $\Pi_1$ definition).

Since wellfoundedness is $\Delta_1$ in ZFC, it is absolute for transitive models (of a small fragment) of ZFC. In other words, transitive embeddings between models of ZFC preserve wellfoundedness. (An embedding $f:M \to N$ is transitive if $f$ maps the elements of $x$ in $M$ onto the elements of $f(x)$ in $N$ for every $x \in M$; so the range of $f$ is a transitive substructure of $N$ isomorphic to $M$.) For models of ETCS+R, there is no natural equivalent to transitive embeddings so if one wants to preserve wellfoundedness then one must explicitly require that. In practice, it is very difficult to check that an embedding preserves wellfoundedness, especially when compared to checking that an embedding is transitive.

Therefore, ETCS+R does not have a very good grasp of wellfoundedness compared to ZFC. Since the study of wellfoundedness is so central to modern set theory, the framework of ZFC is much more appropriate than ETCS+R for set theorists to work with. To rephrase an analogy I used elsewhere, asking a set theorist to work in ETCS+R instead of ZFC is like asking a ring theorist to work with ternary relations $A(x,y,z)$ for addition $x+y = z$ and $M(x,y,z)$ for multiplication $x \cdot y = z$: it's essentially the same, in principle, but it's simply not the right thing to do!

-

1
Hear hear! In September I worked a bit with Misha Gavrilovich on his model-categorical construction QtNaamen, and I realized that diagrams are simply not the right language to talk about models of ZFC, and in particular when you want to talk about elementary embeddings or so. There are some semi-positive conjectures, and we came up with an idea on how to fine tune it to allow the elementarity to slip through the cracks, but it's still very much unfit as a language. (I read your blog post and liked it, and it reminded me to write a post on the work with Misha...) – Asaf Karagila Jan 4 at 1:27

1
For the record, let me repeat here my essential agreement, and also my linguistic objection. I would say the problem isn't that ETCS has a "weak grasp of well-foundedness; ETCS understands well-founded relations perfectly well as a structural concept. The problem is more like that in ETCS the "universe" is not well-founded in any sense: ZFC only knows about well-founded things, while ETCS knows about other things as well, and that makes it more complicated to use if all you care about are the well-founded ones. – Mike Shulman Jan 7 at 7:32

There are several relatives (typically: subtheories and supertheories) of ZFC that are used in set-theoretic research. If somebody wants to do set theory based on ETCS or a related base theory, these theories would have to be translated to this new base (or, in the case of theories that are not so canonical, such as ZFC*, substitutes would have to be found).

Such a translation seems to be rather straightforward in the case of supertheories; a good translation would of course use the idioms of the target language.

• Examples of supertheories:
• ZFC plus large cardinals
• ZFC plus definable determinacy (e.g., projective determinacy, or some consequences thereof - related to large cardinals).
• ZF plus AD, or ZF + $V=L(\mathbb R)$ (supertheory of ZF only)
• ZF(C) plus "V is a certain inner model". Weaker versions include:
• ZFC plus cardinal arithmetic assumptions (GCH, SCH)
• ZFC plus combinatorial principles ($\diamondsuit$, etc)
• ZFC plus forcing axioms (MA, PFA etc)
• others, including combinations (conjunctions) of the above
• Examples of subtheories
• KP and related theories, which do not have full comprehension. (I think they are usually associated with proof theory rather than set theory)
• ZFC minus infinity (this is more closely associated with arithmetic than with set theory)
• ZF, or ZF plus weak versions of choice
• ZFC minus power set (plus instances of power set). Typical models are of the form $H(\chi)$.
• ZFC minus replacement (plus finitely many instance of replacement). Typical models are $V_\delta$.
• ZFC*, an often unspecified finite subset of ZFC, used to get around the "undefinability of truth", or to apply the reflection theorem. (Morally the same as the previous item.)
• ZFC minus Foundation, reflecting the fact that Foundation is hardly used outside set theory.
• Others, including combinations (intersections) of the above
• Other relatives:
• ZF(C) with atoms, perhaps closer to mathematical practice than ZFC itself.
• NBG. The relation between NBG and ZFC is very well understood, as are the advantages and disadvantages: On the plus side, NBG can naturally talk about classes, and is finitely axiomatized (which might make it more amenable to automated theorem proving). On the other hand, the fact that not every subclass of $\mathbb N$ is a set can be inconvenient.
• MK and others.
• NF and NFU, sometimes claimed to be more natural than ZFC. While ZFC makes it awkward to talk about classes, NFU has problems with the function `$x\mapsto \{x\}$`.
-

Is there a simple example of a subclass of $\omega$ which is not a set? (I suspect it will be something related to undefinability of the truth or so?) – Asaf Karagila Jan 4 at 1:49
Unless I'm confused (which is possible), there is no refutation in NBG of the claim that every subclass of a set X is a set; there just is no proof (not even if we require X to be ω, although there is if we require X to be finite).  If you add this claim (as an axiom scheme, and then the result is no longer finitely axiomatisable) to NBG, then you get the consistent (assuming that ZFC plus one inaccessible cardinal, or even something weaker than that, is consistent) theory MK (Morse–Kelley). – Toby Bartels Jan 7 at 9:56

Well, one would just add a just strong enough instance of replacement, or the consequence one actually needs, to the assumptions of the theorem one was proving. For instance, one could take the existence of $\aleph_\omega$ as an assumption (like a large cardinal) rather than proving it exists. There are models of ETCS in which this exists and in which it doesn't. In this instance, one is just lowering the level at which one considers a cardinal 'large'.

I'm reminded of McLarty's recent work on weak set theories, and doing algebraic geometry in them. One can prove strong results about cohomology, but can't prove the existence of an uncountable ring like $\mathbb{R}$ or $\mathbb{C}$. He says you can just simply posit the existence of such a thing on top of the weak set theory, and then all the theorems go through.

Of course, in set theory there are a whole stack of results that rely on the strength of ZFC beyond ETCS, and it would entail a whole lot of reverse mathematical effort to find out what is actually necessary for swathes of theory, that many would say it is easier to just assume what ZFC gives you. But it isn't strictly necessary, just a lot easier.

-

4
I have to admit often that I am weirded out by all those theories which are like "We are better than ZF, but we can't prove anything useful exists. But if you assert its existence then the theorems work as before". Wasn't the idea of foundations on set theory exactly to have one framework which just proves that everything you want to do can be done, except division by zero? :-) – Asaf Karagila Dec 18 at 23:35

2
... just a foundation for 'ordinary/everyday' maths. – David Roberts Dec 19 at 0:08

2
@Asaf: although I am not sure what question David is responding to in the OP (see also my comment under Andreas's answer), your comment sounds just a wee bit aggressive to me. Maybe the question needs to be closed down, before this gets too subjective and argumentative? – Todd Trimble Dec 19 at 0:13

4
My reading of Asaf's comment is different than Todd and Andrej. I think this is a case where the medium of communication interferes with the message. I think his (poorly formulated) point is valid. It's not clear to me that a general foundation should have the goal of doing just enough instead of the goal of doing it all. That said, there are other contexts where doing the minimum makes perfect sense, such as reverse mathematics. – François G. Dorais♦ Dec 19 at 1:54

3
Well, I do feel we're getting sidetracked. For the sake of making progress, how about we consider ETCS augmented by a suitable axiom scheme of replacement (a categorical form of this has been discussed by McLarty -- the reference is in Tom's paper, IIRC), and try addressing OP's questions with that in mind? – Todd Trimble Dec 19 at 2:57
show 4 more comments

I like the fact that you asked this question, but I'm a little worried that it will be seen as "subjective and argumentative".

For the second question, I think a lot of set theorists (trained since childhood in ZFC) have gone on record saying they do find ETCS not easy to work with or not user-friendly, and I find this quite understandable. There is a critical hump of lemmas to get over in the beginning when working with ETCS, because unlike ZFC or some variation thereof, there is no ready-made comprehension scheme in ETCS (at least as it is ordinarily presented). Rather, a stock of instances of comprehension (where one builds up an "internal logic" by hand, as it were) have to proven before one is ready to fly. But after some point, with enough of these beginning lemmas under the belt, the development of mathematics, say of the core undergraduate curriculum involving basic results of real analysis, algebra, topology, etc., proceeds pretty much the same way as what one is used to. So in that sense, I'd say "it does not matter" for the needs of working mathematicians.

In developing his new set theory SEAR (Sets, Elements, And Relations), Mike Shulman recognized this cumbersome aspect of ETCS, quoting an analogy I made once about ETCS on the now-moribund "Todd and Vishal's blog":

[Trimble] "with ZFC it’s more as if you can just hop in the car and go; with ETCS you build the car engine from smaller parts with your bare hands, but in the process you become an expert mechanic, and are not so rigidly attached to a particular make and model."

[Shulman] Using this metaphor, SEAR can be thought of as an ETCS-car which comes preassembled with a nice slick control panel. Or, using an alternate metaphor, ZFC is like Windows, ETCS is like UNIX, and SEAR is like OS X (or maybe Ubuntu). With SEAR you get a nice familiar interface with which it is easy to do standard things, there is less cruft than you get with ZFC, and behind the scenes you have all the power of ETCS (and more). (Of course, if you like Microsoft products, then this metaphor probably does not appeal to you.)

So SEAR aims to combine the advantages of ETCS (as a truly "structural" set theory, where the aspects of sets we truly care about are isomorphism-invariant, and carry less "cruft") with the advantages of ZFC (where comprehension principles, etc. are built right in; see his axiom 1). SEAR will probably look more home-y and familiar to those used to traditional naive set theory; there is none of this intimidating "well-pointed topos with NNO and choice" business to wade through at the outset.

-

2
@Todd Trimble: This answer is closest to the intention of the question, particularly with phrases like "gone on record saying they do find ETCS not easy to work with or not user-friendly". – Stxmqs Dec 19 at 6:54

Much of set theory research (for example, a paper I'm currently working on, concerning certain ultrafilters over the natural numbers) would work just fine in ETCS. But much of set theory research uses the axiom of replacement in ways that cannot be imitated in ETCS. Tom Leinster's paper gives the example of the existence of the union of $\mathbb N$, its power set $\mathcal P(\mathbb N)$, the power set of that, and so on, iterated for countably many steps. To put it another way, ETCS cannot prove that there is a cardinal number $\kappa$ with infinitely many infinite cardinals below it. Such $\kappa$'s and far larger ones are certainly involved in a great deal of research-level set theory, so a foundation having the strength of ZFC (or even more) is needed there.

-

1
My impression is that the OP was aware of the need for an extra replacement axiom in addition to ETCS to get equiconsistency with full ZFC; his questions seem to lie elsewhere. – Todd Trimble Dec 19 at 0:06
@Andreas Blass: Ok, so set-theory goes well beyond ZFC these days. The question then is take ETCS as your base and add whatever large cardinals that you need, then do you now care that you have started with ETCS instead of ZFC? – Stxmqs Dec 19 at 6:48
Another question arises: can even stronger theories be rephrased using ideas that would be comfortable for category-theorists but without the category terminology - category-free categorical-set theories and would set-theorists care for such things? – Stxmqs Dec 19 at 7:01

2
As Tom Leinster points out in his paper, one can reconstruct the ZFC universe in ETCS once one adds enough axioms (like a version of replacement). After that reconstruction is carried out, there would be no noticeable difference between working in ZFC and working in the interpretation of ZFC in ETCS. You could take what people ordinarily say on the basis of ZFC, including things about the ZFC membership relation and the cumulative hierarchy of sets, and understand them as referring to those notions as defined within ETCS. – Andreas Blass Dec 19 at 12:38
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 46, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9525278210639954, "perplexity_flag": "middle"}