Axiom of Foundation

Definition

The axiom of foundation (also called the axiom of regularity) states that every non-empty set has a member disjoint from itself: $\forall S:\mathbf{Set}.S\ne \varnothing \to \exists x\in S.x\cap S=\varnothing .$

The element $x$ is called an $\in$-minimal element of $S$: no element of $x$ is also in $S$.

Equivalent Formulations

The following are equivalent over the other axioms of ZF:

• Well-foundedness of $\in$: there is no infinite descending $\in$-chain $\cdots \in x_2\in x_1\in x_0.$
• $\in$-induction: to prove a property $P$ holds for all sets, it suffices to show that if $P(y)$ holds for all $y\in x$, then $P(x)$ holds: $(\forall x.(\forall y\in x.P(y))\to P(x))\to \forall x.P(x).$
• No set is an element of itself: $\forall x.x\notin x$ (a consequence of the chain-free formulation).

Consequences

• No set contains itself: $x\notin x$ for all $x$.
• No two-element cycle: there are no sets $x,y$ with $x\in y$ and $y\in x$.
• More generally, no finite $\in$-cycle exists.
• The membership relation $\in$ restricted to any set is well-founded, enabling $\in$-induction and $\in$-recursion.

The Cumulative Hierarchy

Foundation is equivalent to the assertion that every set appears in the von Neumann cumulative hierarchy $V={\bigcup }_{\alpha }{V}_{\alpha }$, defined by transfinite recursion on the ordinals: $V_0=\varnothing ,V_{\alpha +1}=\mathcal{P}(V_{\alpha }),V_{\lambda }={\bigcup }_{\alpha <\lambda }{V}_{\alpha }\text{ (for limit }\lambda \text{)}.$

The rank of a set $x$ is the least ordinal $\alpha$ such that $x\in V_{\alpha +1}$. Foundation ensures that every set has a rank.

The cumulative hierarchy stratifies all sets into levels: sets at level $\alpha$ are built from sets at earlier levels, reflecting the intuition that sets are “constructed from below.”

Role in ZF

Foundation is the only axiom of ZF that restricts which sets exist, rather than asserting that new sets can be formed. The other axioms are essentially generative. Foundation rules out pathological sets such as $x=\{x\}$ or infinite descending chains.

Foundation is not needed for most of ordinary mathematics. Many results in analysis, algebra, and topology can be developed in ZF without foundation. However, it is essential for the theory of ordinals and cardinals to behave cleanly, and for the cumulative hierarchy to provide a canonical universe of sets.

Relationship to Well-Foundedness

The axiom of foundation asserts precisely that the global membership relation $\in$ is well-founded on the universe of all sets. This is analogous to the well-ordering of the ordinals by $\in$, and it is what makes $\in$-induction and $\in$-recursion available as proof and definition principles across all of set theory.

In type theory, a similar role is played by the structural discipline of inductive types, which ensure that all data is built by a finite sequence of constructors, ruling out self-referential or non-well-founded structures by design.

Non-Well-Founded Set Theory

Set theories that drop the axiom of foundation and instead allow sets such as $x=\{x\}$ are called non-well-founded or hyperuniversal set theories. Aczel’s anti-foundation axiom (AFA) is a well-studied alternative, replacing foundation with the assertion that every “graph equation” has a unique solution. Non-well-founded sets are used to model bisimulation and coinductive structures.

Related Concepts

• Well-founded Relation
• Ordinal
• Set Theory
• Transitive Set
• Power Set
• Inductive Type
• Bisimulation