It was Mirimanoff (1917) who first stated the fundamental difference
between * well-founded* and * non-well-founded* sets. He
called sets with no infinite descending membership sequence
well-founded and others non-well-founded. Non-well-founded sets have
been extensively studied through decades, but did not show up in
notable applications until Aczel. This is probably due to the fact
that the classical well-founded universe was a rather satisfying
domain for the practicing mathematician (``the mathematician in the
street'' (Barwise 1985)). Aczel's work on non-well-founded sets
evolved from his interest in modeling concurrent processes. He
adopted the graph representation for sets to use in his theory. A set
like can be unambiguously depicted as in
Figure 6 in this representation (Aczel 1988), where an arrow
from a node **x** to a node **y** denotes the membership relation between
**x** and **y** (i.e., ).

**Figure 6:** Representation of the set * a* in Aczel's conception

A set (pictured by a graph) is called well-founded if it has no
infinite paths or cycles, and non-well-founded otherwise. Aczel's
* Anti-Foundation Axiom*, AFA, states that every graph,
well-founded or not, pictures a unique set. Removing the Axiom of
Foundation (FA) from the ZFC and adding the AFA results in the *
Hyperset Theory*. (ZFC without FA is denoted as ZFC.) What is
advantageous with the new theory is that since graphs of arbitrary
form are allowed, including the ones containing proper cycles, one can
represent self-referring sets. For example, the graph in
Figure 7 is the picture of the unique set .

The picture of a set can be * unfolded* into a tree picture of
the same set. The tree whose nodes are the finite paths of the apg
(cf. Note 11) which start from the point of the apg, whose edges are
pairs of paths , and whose root is the path of length one is called the
* unfolding* of that apg. The unfolding of an apg always
pictures any set pictured by that apg. Unfolding the apg in
Figure 7 results in an infinite tree, analogous to
.

**Figure 7:** The picture of the circular set

According to Aczel's conception, for two sets to be different, there should be a genuine structural difference between them. (Therefore all the three graphs in Figure 8 depict the unique non-well-founded set .)

**Figure 8:** Other graphs depicting

Aczel develops his own extensionality concept by introducing the
notion of bisimulation. A * bisimulation* between two apg's,
with point and with point , is a relation satisfying the following conditions:

- if
**nRm**then- for every edge of , there exists an edge of such that
- for every edge of , there exists an edge of such that

Two apg's and are said to be * bisimilar*, if a
bisimulation exists between them; this means that they picture the
same sets. It can be concluded that a set is completely determined by
any graph which pictures it.

The uniqueness property of AFA leads to an intriguing concept of
extensionality for hypersets. The classical extensionality paradigm,
that sets are equal if and only if they have the same members, works
fine with well-founded sets. However, this is not of use in deciding
the equality of say, and because it just
asserts that **a=b** if and only if **a=b**, a triviality (Barwise &
Etchemendy 1987). However, in the universe of hypersets, **a** is
indeed equal to **b** since they are depicted by the same graph. To see
this, consider a graph **G** and a decoration **D** assigning **a** to a
node **x** of **G**, i.e., . Now consider the decoration
exactly the same as **D** except that . must also be a
decoration for **G**. But by the uniqueness property of AFA, , so
, and therefore **a=b**.

The AFA universe can be depicted as in Figure 9, extending around the well-founded universe, because it includes the non-well-founded sets which are not covered by the latter.

**Figure 9:** AFA universe extending around the well-founded universe (adapted from (Barwise & Etchemendy 1987))

Sat Jan 13 15:54:04 EET 1996