# Is ETCS well-founded?

I can't find a statement about the axiom of regularity anywhere in treatments of ETCS. Perhaps this is due to the unfortunate clash of terminology with 'foundations'.

• This should be relevant. – Michael Greinecker Jan 8 at 18:09
• I suspect that ETCS is not well-founded in any reasonable sense. One particular way to phrase this might be the following: there are ill-founded models of ZFC - Foundation + $\neg$Foundation which "translate" in the appropriate sense to models of ETCS. – Noah Schweber Jan 8 at 18:16
• At the same time, it's not entirely clear to me what "foundation" would mean in the context of ETCS (where we're not basing everything on elementhood after all). In fact, I'd guess the following: if $M$ is a model of ETCS "generated" by a well-founded model $N$ of ZFC, there is a model of ZFC - Foundation + AFA which "generates" an isomorphic model. (Besides the obvious vagueness, I'm being a bit rude here in my mix of classical model-theoretic language and ETCS, but I think this is benign in this context.) – Noah Schweber Jan 8 at 18:19
• @NoahSchweber this is my gut feeling too. The more I look into this problem the more it becomes clear that ETCS is quite different of a beast from ZFC (at least model-wise). The question of well-foundedness then makes little sense, from a certain point of view. On the other hand, it is natural to ask how are the two theories related: in which sense ETCS sets are ZFC sets? – mattecapu Jan 8 at 18:26
• Does the pope poop in the woods? – Asaf Karagila Jan 8 at 18:51

As Noah suggests, the axiom of regularity doesn't make sense in the language of ETCS. What we can say is:

• To construct a model of ETCS+R from a model of ZFC, one doesn't need regularity.
• From a model of ETCS+R, one can construct a model of ZFC with regularity, and also separately models of ZFC with regularity replaced by various anti-foundation axioms.

The composite ETCS+R -> ZFC -> ETCS+R is the identity, as are the ill-founded versions. And the composite ZFC -> ETCS+R -> ZFC is also the identity, as are ill-founded versions whose anti-foundation axiom is sufficiently strong to characterize possible set-membership diagrams structurally.

Among other places, more details can be found in this paper of mine.

• What is R here? Replacement? – Noah Schweber Jan 8 at 20:05
• @NoahSchweber Yes, R denotes any of the equivalent replacement/collection axiom schemas that can be added to ETCS. – Mike Shulman Jan 9 at 21:28
• Is there a “canonical” way of interpreting ZFC in ETCS, about which one may ask whether one ends up with a well-founded model? – Monroe Eskew Jan 11 at 11:28
• @MonroeEskew Since "ZFC" by definition includes the regularity axiom, I would argue that the construction of a model with regularity is the canonical way of interpreting ZFC in ETCS. And there's similarly a canonical way of interpreting ZFC-regularity+AFA in ETCS. But no, there's no way of constructing such an interpretation without deciding in advance whether you want it to satisfy regularity or not, and it'll basically always be possible to do both -- ETCS doesn't "know" anything about regularity. – Mike Shulman Jan 11 at 20:23
• Another way to think about it is that ZFC and ZFC-regularity+AFA (AFA = anti-foundation axiom) are essentially equivalent -- one can construct a model of either one from the other -- and passing back and forth between them doesn't change the corresponding model of ETCS. – Mike Shulman Jan 11 at 20:24