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:
of 
, there exists
an edge 
of 
such that 
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))