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's work also foundational.

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	Member	Set membership
Ω	U+03A9	Quine atom	Ω = {Ω}
∼	U+223C	Bisimilar	Bisimulation equivalence
AFA	—	Anti-foundation	Unique decoration
→	U+2192	Edge	Graph edge
d	—	Decoration	Graph labeling

Metatheory. ZFA (ZFC minus foundation plus AFA) is equiconsistent with ZFC. Every set has a canonical graph (its unfolding). Bisimulation quotient gives unique normal form. Final coalgebra semantics: non-well-founded sets are final coalgebras. Set theory becomes a category of coalgebras.

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. Counterintuitive: x ∈ x violates naive expectations. Different anti-foundation axioms exist (Boffa, Scott). Most mathematics doesn't need non-well-founded sets. Tool support limited compared to ZFC. Intuitions from well-founded sets mislead. Cardinality and other properties require care.