10
$\begingroup$

In categorical set theory, we observe that certain topoi satisfy (suitable versions of) certain axioms from set theory. For example, Lawvere's $\mathsf{ETCS}$ asserts that $\mathbf{Set}$ is a well-pointed topos with a natural numbers object, satisfying the (internal) axiom of choice. $\mathsf{ETCS}$ is known to be equivalent to $\mathsf{BZC}$, a fragment of $\mathsf{ZFC}$ which doesn't include regularity.

My question is: what does it take for a topos to satisfy (a suitably phrased version of) the axiom of regularity? Or perhaps some statement which is equivalent (in the presence of the other $\mathsf{ZFC}$ axioms), as I understand regularity is not intuitionistically acceptable.

$\endgroup$
1
  • $\begingroup$ I think it will take some work to whip up an appropriate phrasing of the axiom of regularity; "$\in$ is well-founded" isn't really categorical. One which I can think of - due to Hamkins as far as I know - is "If every well-founded set can be well-ordered, then every set can be well-ordered." But that's is extremely clunky to work with. (Incidentally, there are various questions here and at MSE about regularity in categorical foundations which may be of interest. $\endgroup$ Commented Nov 3, 2020 at 8:02

1 Answer 1

22
$\begingroup$

The relationship between toposes and set theories was studied comprehensively in

Steve Awodey, Carsten Butz, Alex Simpson, Thomas Streicher: Relating first-order set theories, toposes and categories of classes. Annals of Pure and Applied Logic, Volume 165, Issue 2, February 2014, Pages 428-502

Regularity is discussed under the name "well-foundedness". You can find a lot of details in the paper, I am just going to quickly review the setup.

We work in an elementary topos $\mathcal{E}$.

The first step is to cook up a notion of $\in$-membership. Define a membership graph to be a triple $G = (|G|, A_G, r_G)$ where $|G|$ an $A_G$ are objects and $r_G : |G| \to A_G + P|G|$ a morphism. We think of $|G|$ as a set of vertices with each vertex $x \in |G|$ being either an atom $a$ (in case $r(x) = \mathrm{inl}(a)$ for $a : A_G$) or a branching vertex with adjacency set $d \subseteq |G|$ (in case $r(x) = \mathrm{inr}(d)$ for $d : P|G|$). We may define a bisimilarity relation $\sim_{G,H}$ between two membership graphs expressing the fact that, up to reordering and repetition, $G$ and $H$ represent the same $\in$-membership structure. In other words, $\sim_{G,H}$ expresses extensional equality of sets represented by $G$ and $H$. In particular, $\sim_{G,G}$ is an equivalence relation which quotients the membership graph to give a membership relation that is extensional.

Next, we define a new topos $\mathcal{E}_\mathrm{nwf}$ whose objects are triples $(D, m, G)$ where $G$ is a membership graph in $\mathcal{E}$, $D$ an object of $\mathcal{E}$, and $m : D \to |G|$ a mono in $\mathcal{E}$. A suitable notion of morphism is devised that takes into account the bisimilarity relations $\sim_{G,H}$. We then have:

Theorem 11.7: $\mathcal{E}_\mathrm{nwf}$ is equivalent to $\mathcal{E}$.

We may understand the theorem as saying that we enriched the topos $\mathcal{E}$ with membership relations to get $\mathcal{E}_\mathrm{nwf}$, which changed the topos only up to equivalence (so not in any essential way from the point of view of topos theory).

So far we allow both atoms and non-well-founded membership relation. The next step is to define what it means for a membership graph $G = (|G|, A_G, r_G)$ to be well-founded. Here there are no surprises, as we can use the internal language of the topos to state when $X : P|G|$ satisfies the property "$X$ contains all the atoms $A_G$ and is hereditarily closed under the membership relation $r_G$" (see the formula after Corollary 11.2).

We define a third topos $\mathcal{E}_\mathrm{wf}$ as the full subcategory of $\mathcal{E}_\mathrm{nwf}$ of those objects whose membership graphs are well-founded.

Proposition 11.3: The equivalence between $\mathcal{E}$ and $\mathcal{E}_\mathrm{nwf}$ cuts down to an equivalence between $\mathcal{E}$ and $\mathcal{E}_\mathrm{wf}$.

The moral of the story is that, firstly, we may define a notion of extensional membership relation on objects in a topos, and secondly, that restricting to the well-founded part of the topos does not change the topos in a way that is relevant to topos theory.

In a sense the answer to the question "when does a topos satisfy the axiom of regularity" is "it does not matter". This is further discussed in the paper in Section 11.4, where the authors conclude with

... it follows that any topos can be construed both as a model of BIZFA− and as a model of BINWFA−.

Here BIZFA- is their formulation of ZF-like set theory with foundation (regularity) and BIZWFA- a formulation of ZF-like set theory with anti-foundation.

Disclaimer: please do not take the above summary as a satisfactory description. The paper contains many more details and explanations, and it should be consulted for thorough understanding of the topic.

$\endgroup$
2
  • $\begingroup$ Note that as BIZFA- and BIZWFA- have atoms, this doesn't contradict Hamkin's answer which Noah linked above. It follows that the category $\mathcal E_{\operatorname{wf}}$ is not always equivalent to its subcategory on the objects with atom-free transitive closure. $\endgroup$
    – Jem
    Commented Nov 4, 2020 at 14:47
  • $\begingroup$ Good point. So what happens if we additionally restrict to well-founded atom-less membership graphs? $\endgroup$ Commented Nov 11, 2020 at 14:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .