Non-well-founded Set Theory

Origin. Aczel formalized anti-foundation axiom (AFA, 1988). Allows sets to contain themselves and circular membership. Motivated by computer science (co-induction, bisimulation). Generalizes ZFC by replacing foundation axiom. Forti and Honsell had stated an equivalent axiom earlier (1983).

Models. Sets with circular membership. ZFC: foundation axiom forbids x ∈ x. Non-well-founded: allows Ω = {Ω} and more complex cycles. Models streams, processes, circular data structures. Bisimulation replaces extensionality: sets equal if bisimilar.

Formalism.

Anti-Foundation Axiom (AFA): Every graph has a unique decoration.

A decoration of a graph G = (N, →) assigns a set to each node such that: d(n) = {d(m) : n → m}

AFA: For every graph G, there exists a unique decoration.

Examples:

Ω = {Ω}: graph with one node pointing to itself
Stream s = (head, s): graph n → n (for tail) and n → leaf (for head)
Mutual: A = {B}, B = {A}: two nodes, each pointing to other

Bisimulation: R is a bisimulation on sets if: xRy implies for all a ∈ x, exists b ∈ y with aRb, and vice versa.

Two sets are equal iff bisimilar (strong extensionality).

Solution lemma: Systems of equations have unique solutions. X = {a, X, Y} Y = {X} Has unique solution under AFA.

Co-induction: Prove properties by showing bisimulation exists. Dual to induction on well-founded sets.

Symbols.

Symbol	Unicode	Name	Meaning
∈	U+2208	Element of	Set membership, no longer well-founded
Ω	U+03A9	Omega / Quine atom	The unique set with Ω = {Ω}
∼	U+223C	Tilde operator / Bisimilarity	Bisimulation equivalence, which AFA makes identity
→	U+2192	Arrow / Graph edge	n → m: m is a child of n in the decorated graph
G	—	Graph	A system of nodes and edges to be decorated
N	—	Nodes	The node set of a graph
d	—	Decoration	The assignment d(n) = {d(m) : n → m}
R	—	Bisimulation	A relation matching children in both directions
AFA	—	Anti-foundation axiom	Every graph has exactly one decoration
ZFA	—	ZFC − Foundation + AFA	The resulting set theory

Metatheory. ZFA — ZFC with Foundation deleted and AFA put in its place — is equiconsistent with ZFC, and the proof is constructive in both directions: the well-founded sets of any model of ZFA form an inner model of ZFC, while Aczel (1988), following Forti and Honsell (1983), built a model of ZFA inside ZFC from the accessible pointed graphs quotiented by bisimulation. So nothing is risked and nothing is gained in consistency strength. AFA has three equivalent faces. As unique decoration it says every graph names exactly one set; as strong extensionality it says bisimilar sets are identical, strengthening the ordinary extensionality axiom; and category-theoretically it says the universe of sets is the final coalgebra of the powerclass functor, which is why coinduction and the solution lemma come with it — a system of set equations has a unique solution because finality gives a unique map into the carrier. AFA is not the only such axiom. Aczel catalogues four mutually incompatible ones — his AFA, Scott's SAFA, Finsler's FAFA and Boffa's BAFA — all consistent relative to ZFC and differing over how finely non-well-founded sets are individuated, BAFA being the most permissive.

Applies to. Process algebra semantics (bisimulation). Co-inductive data types (streams, infinite trees). Circular definitions in CS. Semantics of programming languages. Non-terminating computation modeling. Self-reference and fixed points.

Limitations. Dropping Foundation removes ∈-induction and ∈-recursion on the universe. There is no rank function, the cumulative hierarchy no longer exhausts V, and any definition or proof that recurses on membership has to be confined to the well-founded part — which is where almost all of ordinary set theory is then carried out, so the extension does no mathematical work outside the circular fragment it was built for. ZFA gains nothing in strength: it is equiconsistent with ZFC, so it cannot prove Con(ZFC) or Con(ZFA), and CH, AC and the rest remain exactly as independent as before. The axiom is a choice, not a discovery — AFA, SAFA, FAFA and BAFA are pairwise incompatible and nothing in the mathematics selects one. AFA's identification of bisimilar sets is a real loss of resolution: a set records no more than its bisimulation class, so exactly one Quine atom exists, and any process semantics finer than bisimulation — trace equivalence, testing equivalence, weak bisimulation — cannot be represented by distinct AFA sets.