Aczel's ZFC/AFA

The set of axioms for classical set theory created by Zermelo-Fraenkel is called ZF. ZFC is the set theory of Zermelo-Fraenkel with the axiom of choice:

Axiom 5.41  

$$\begin{split}\forall x (\emptyset \notin x \land \forall uv (... ...arrow \ z \cap u \mbox{ has exactly one element})) \end{split}$$

The axiom that is on question in this section is the axiom of foundation. This axiom states, that every set has an $\in$-minimal element:

Axiom 5.42  

$$\exists x (x \not= \emptyset \rightarrow \exists y (y\in x \land x \cap y = \emptyset))$$

The foundation axiom assures that sets cannot contain themselves as elements and that the class of all sets is not a set. It makes sure, that the universe of sets is hierarchical structured and can be created by iterated power-set construction. This is the axiom in question.

A set is well-founded, if it does not have an infinite descending membership sequence, otherwise non-well-founded. This notion is quite old, and well-founded as well as non-well-founded sets have been studied for decades. The notion has been introduced 1917 by Dmitry Mirimanov. Although there have been a number of attempts to replace the foundation axiom of ZFC, there has not been a major breakthrough in applications for non-well-founded sets until the revolutionary work of Peter Aczel in 1988aczset. Before Aczel, there have been a few anti-foundation axioms, due to M. Forti and F. Honsell, P. Finsler, or Dana Scott. The axiom AFA by Forti and Honsell has been adopted by Aczel.

Figure 5.7: The set $a=\{b\}$

Figure 5.8: The set $a=\{\{b,\{c,d\}\},e\}$

Peter Aczel used a graph representation of sets, where an arrow between the nodes $a$ and $b$ denotes the membership relation $a \in b$. A set in graph representation is called well-founded, if it does not have any cycles or infinite descending branches. Figure 5.7 shows the simple well-founded set $a=\{b\}$. The more complex set $a=\{\{b,\{c,d\}\},e\}$ is show in figure 5.8.

Figure 5.9: The set $x=\{x\}$

Figure 5.10: The set $x=\{x\}$ as different graphs

The anti-foundation axiom AFA states, that every set, well-founded or not, pictures a unique set. Removing the foundation axiom from ZFC and adding AFA instead leads to the hyperset theory ZFC/AFA. Now, the so-called Quine atom $x=\{x\}$ can be pictured by a graph, as can be seen in figure 5.9. However, the same unique set can be pictured by many different graphs, as can be seen in figure 5.10.

Aczel stated, that there has to be a fundamental structural difference between graphs to model different sets. He introduced the notion of a bisimulation between two graphs.

Definition 5.34 (Bisimulation of two graphs)   A bisimulation between two graphs $G_1$ with point $p_1$ and $G_2$ with point $p_2$ is a relation $R\subseteq G_1 \times G_2$ satisfying

1. $R(p_1,p_2)$
2. if $R(n,m)$ then
   • for every edge $n\longrightarrow n'$ of $G_1$ there exists an edge $m \longrightarrow m'$ of $G_2$ such that $R(n',m')$.
   • for every edge $m \longrightarrow m'$ of $G_2$ there exists an edge $n\longrightarrow n'$ of $G_1$ such that $R(n',m')$.

Two graphs are called bisimilar, if a bisimulation exists between them.

If two graphs are bisimilar, they picture the same set. Therefore, a set is completely determined by a graph that pictures it. This solves some problems with equality of sets, and shows some interesting properties of extensionality. In classical set theory two sets are equal if and only if they have the same elements. But let $a=\{0,a\}$ and $b=\{0,b\}$. Then $a=b$ if and only if $a=b$. In the theory ZFC/AFA, $a$ and $b$ are indeed equal, because their corresponding graphs are bisimilar.