Costs and benefits of using non-well-founded set theories instead of ZFC, or ZFC instead of non-well-founded set theories?

Question

What are some advantages and disadvantages of using ZFC as opposed to non-well-founded set theories, and what are some advantages and disadvantages of using non-well-founded set theories as opposed to ZFC?

Answer 1

The main selling point of the axiom of foundation is that you can use Scott's Trick.

Let's say I define an equivalence relation $\textbf{R}$ on a class $\textbf{S}$.

The axiom of foundation allows us to produce a "quotient class" $\textbf{P} : \textbf{S} \to \textbf{S} / \textbf{R}$

What do I mean by that? Recall that given a set $S$ and an equivalence relation $R$, a quotient $P : S \to S / R$ is a set $S / R$ together with a surjective function $P : S \to S / R$ such that for all $a, b \in S$, $P(a) = P(b)$ iff $a R b$.

To construct a quotient, we typically define $P(x) = \{y \in S \mid yRx\}$ and then define $S / R$ to be the range of $P$.

This construction doesn't work when $\textbf{S}$ is a potentially proper class, since $\{y \in \textbf{S} \mid y \textbf{R} x\}$ may also be a proper class and thus can't be an output of $\textbf{P}$.

Instead, we define $\textbf{P}(x) = \{y \in \textbf{S} \mid y \textbf{R} x$ and of all the $y$ such that $y \textbf{R} x$, $y$ has minimal rank$\}$. Note that $\textbf{P}(x)$ is also always a set. This is because we can let $\alpha$ be the smallest rank of any $y \in \textbf{S}$ such that $y \textbf{R} x$. Then $\mathbf{P}(x) \subseteq \{y \mid y$ has rank $\alpha\}$, and the latter is a set.

We then define $\textbf{S} / \textbf{R}$ to be the range of $\textbf{P}$.

Note that the fact that every set has a rank is equivalent to the axiom of foundation. And this definition only makes sense if every set has a rank. So this definition only makes sense in the context of the axiom of foundation.

Let's also note that for all $y \in \mathbf{P}(x)$, $y \mathbf{R} x$.

This allows us to prove the axiom scheme of collection from the axiom scheme of replacement. In particular, let's say we know that for some class relation $\mathbf{C}$, $\forall x \in a \exists y (x \mathbf{C} y)$. Given a particular $x \in a$, define $\mathbf{R}_x$ to be the equivalence relation $y_1 \mathbf{R}_x y_2$ if and only if $[x \mathbf{C} y_1 \iff x \mathbf{C} y_2]$, and define $\mathbf{P}_x : \mathbf{V} \to \mathbf{V} / \mathbf{R}_x$ as a quotient map. Then for all $x \in a$, there exists a unique $z$ such that for some $y$, $x \mathbf{C} y$ and $z = \mathbf{P}_x(y)$. So we can form the set $S = \{\mathbf{P}_x(y) \mid x \in a$ and $x \mathbf{C} y\}$ using the axiom scheme of replacement.

Then for all $x \in a$, there is some $y \in \bigcup S$ such that $x \mathbf{C} y$.

Without the axiom of foundation, it's not possible to prove every instance of the axiom scheme of collection using the axiom scheme of replacement. See this answer for some details.

Of course, this is hardly the end of the world - we can just take collection as the axiom scheme instead of replacement. But it's still quite convenient.

In another sense, the axiom of foundation is totally useless. This is because in practice, all mathematics is about mathematical structure. This means that we only care about sets to the extent that they have structure on them which can be transferred via bijection.

But assuming the axiom of choice, every set can be well-ordered, and therefore every set can be placed into bijection with a von Neumann ordinal (which is a well-founded set).

Put another way, given a model of $ZFC^-$ (eg $ZFC$ without foundation), we can take its category of sets $Set_V$. We could also construct the class $WF$ of well-founded sets and then take the resulting category of sets $Set_{WF}$. The resulting categories of sets are equivalent (in that the forgetful functor $Set_{WF} \to Set_V$ is fully faithful and essentially surjective). Therefore, any "purely structural" theorems which can be proved using foundation can also be proved without it, since a "purely structural" theorem can be defined as one which depends only on the properties of the category of sets, and all theorems which depend only on the categorical properties of a category can be transferred across a fully faithful and essentially surjective functor.

In particular, most useful instances of the axiom of collection are provable without the axiom of foundation. And all instances of collection which are "structural" in natural can be proved without foundation.

To illustrate this, let $\phi(x, Y)$ be a property of $x$ and a topological space $Y$ which is invariant under homeomorphism in $Y$. Suppose we have shown that $\forall x \in a . \exists Y . \phi(x, Y)$.

Then consider $x \in a$, and consider some $Y$ such that $\phi(x, Y)$. Put $Y$ into bijection with an ordinal $\alpha$, and equip $\alpha$ with the corresponding topology to get the space $Y'$. Then $\phi(x, Y')$ by homeomorphism invariance.

So in particular, we have $\forall x . \exists \alpha . \alpha$ is an ordinal and there is a topology $\tau$ on $\alpha$ such that $\phi(x, (\alpha, \tau))$. We can then take the smallest $\alpha$ such that $\phi(x, (\alpha, \tau))$ for some topology $\tau$ on $\alpha$. This allows us to prove the instance of collection involving $\phi$.

Edit: I don't know too much about non-well-founded set theories, but I will provide a summary of the implications of the axiom of anti-foundation.

The axiom of anti-foundation states:

For every $E \subseteq V^2$, there exists a unique surjective function $d$ with domain $V$ such that for all $v \in V$, $d(v) = \{d(u) \mid (u, v) \in E\}$. Such a function $d$ is known as the decorator of $(V, E)$.

ZFA is ZFC without foundation but with anti-foundation.

For an example of how this explicitly violates foundation, consider the graph $V = \{*\}$ with $E = \{(*, *)\}$. Any decorator must have $d(*) = \{d(*)\}$. So $d(*)$ is a non-well-founded set.

It turns out that using anti-foundation, we can actually do many of the same things as we could do with foundation. Namely, Scott's Trick still works.

How is that? We simply need a different definition of rank. Define $rank'(s) = |tc(s)|$, where $tc(s)$ is the transitive closure of $s$. Then $\{s \mid rank'(s) = \kappa\}$ is a set for all cardinals $\kappa$.

How do we know that $\{s \mid rank'(s) = \kappa\}$ is a set? We first show that $\{t \mid t$ is transitive and $|t| = \kappa\}$ is a set. If $t$ is transitive, then $(t, \in_t)$ is a graph, and the identity function is the decorator of the graph. Now if $|t| = \kappa$, then we can push the graph $(t, \in_t)$ across some bijection $t \to \kappa$ to get a graph $(\kappa, E)$ which is graph-isomorphic to $(t, \in)$. Thus, the range of the decorator of $(\kappa, E)$ will be the same as the range of the decorator of $(t, \in_T)$, which is of course $t$. So $\{t \mid t$ is transitive and $|t| = \kappa\}$ can be written as $\{U \mid E \subseteq \kappa^2, U = range(decorator(\kappa, E)), |U| = \kappa\}$.

Then $\{s \mid rank'(s) = \kappa\} \subseteq P(t \mid t$ is transitive and $|t| = \kappa\}$.

Thus, we can repeat Scott's trick using $rank'$ instead of $rank$.

In the case of the axiom of foundation, it's easy to phrase the principle as "all sets are well-founded". The class of well-founded sets provides a simple model for this statement, and, as noted, restricting mathematics to well-founded sets leaves us with an equivalent category of sets. This makes the class of well-founded sets the "canonical" model.

However, there is no corresponding principle for the axiom of anti-foundation, since if we start with a universe $V = WF$ where all sets are well-founded, we cannot get non-well-founded sets by restricting our attention to a subclass of $WF$.

We can still come up with a "canonical" model of anti-foundation by analysing very carefully the kinds of graphs which are of the form $(t, \in_t)$ for some transitive set $t$ using the notion of "bisimulation". The model is canonical in the sense that if we start with a model of ZFA, we will end with "the same" model of ZFA (up to isomorphism). And it is also very convenient in that the category of sets in the model is, once again, equivalent to the category of sets in the original model.

So anti-foundation, just like foundation, does not change the category of sets. Thus, no "purely structural" facts about mathematics require anti-foundation, just as no "purely structural" facts require foundation.

Anti-foundation does allow us to very conveniently construct coinductive sets. For instance, it's natural when studying computer science to want to discuss "streams", which are "infinite data structures". More specifically, a Stream(T) consists of a head of type T, together with a tail of type Stream(T).

With anti-foundation, we can explicitly construct the coinductive set $Stream(T) = T \times Stream(T)$ and actually make $Stream(T)$ contain all infinite sequences. With foundation, the equation $Stream(T) = T \times Stream(T)$ has only one solution: $Stream(T) = \emptyset$. So we would have to instead find a solution to $Stream(T) \simeq T \times Stream(T)$, and we'd have to deal with an isomorphism everywhere between $Stream(T)$ and $T \times Stream(T)$.