nLab axiom of foundation

The axiom of foundation

The axiom of foundation

In material set theory, the axiom of foundation, also called the axiom of regularity, states that the membership relation \in on the proper class of all pure sets is well-founded. In structural set theory, accordingly, one uses well-founded relations in building structural models of well-founded pure sets.


Given a proper class AA of pure sets, suppose that AA has the property that, given any pure set xx,

t,txtA, \forall t,\; t \in x \Rightarrow t \in A ,

then xAx \in A. Such an AA may be called a membership-inductive class. Then the axiom of foundation states that the only membership-inductive class of pure sets is the class of all pure sets. In this form, the axiom of foundation is also called \in-induction.

Although the statement here refers to proper classes, it can also be formulated as an axiom schema that makes no mention of classes.

Alternative formulations

While the statement above follows how the axiom of foundation is generally used —to prove properties of pure sets by transfinite induction—, it is complicated. Two alternative formulations are given by the following lemmas:


The axiom of foundation holds if and only if there exists no infinite descending sequence x 2x 1x 0\cdots \in x_2 \in x_1 \in x_0.


First, suppose the axiom of foundation holds, and suppose there were such a sequence. Let AA be the class of all sets which are not equal to x ix_i for any ii. Then for any xx, if xx were equal to some x ix_i, then some txt\in x would also be equal to some x jx_j, namely x i+1x_{i+1}; hence if all txt\in x are in AA, so is xx. Thus, by the axiom of foundation, all sets are in AA, a contradiction.

Second, suppose there are no such sequences, and let AA be as in the statement of foundation. Suppose that AA does not contain all sets. Then there exists an x 0Ax_0\notin A. By hypothesis on AA, there must exist an x 1x 0x_1\in x_0 such that x 1Ax_1 \notin A. And hence an x 2x 1x_2\in x_1 such that x 2Ax_2 \notin A, and so on, producing an infinite descending \in-sequence in contradiction to our hypothesis; hence AA must contain all sets.

This is essentially a version of Fermat's method of infinite descent modified to apply to transfinite induction instead of only to ordinary induction. It arguably provides the most direct intuitive picture of what the axiom means. Note that as a special case, it implies that no set can contain itself, since then xxx\cdots \in x\in x\in x would be an infinite chain.


The axiom of foundation holds if and only if every inhabited pure set xx has a member yxy \in x such that no txt \in x satisfies tyt \in y. (Such a yy is called a membership-minimal element of xx.)


First, suppose the axiom of foundation holds, let xx be a pure set without a membership-minimal element, and let A={y|yx}A = \{ y | y\notin x \}. If zz is a set such that all tzt\in z are in AA, then we cannot have zxz\in x, since then we would have some tzt\in z with txt\in x and hence tAt\notin A; hence zAz\in A. So AA satisfies the assumptions of the foundation axiom, and hence xx is empty.

Second, suppose that every inhabited pure set has a membership-minimal element, and let AA be as in the statement of foundation. Since every pure set is contained in a transitive set, it suffices to show that Ax=xA \cap x = x for any transitive xx. Let y={zxzA}y = \{ z\in x \mid z \notin A \}. If yy is inhabited, then it contains a membership-minimal element zz, i.e. we have zxz\in x, zAz\notin A, and for every tzt\in z we have tzt\notin z—but txt\in x since xx is transitive, hence tAt\in A. Thus this zz contradicts the assumption on AA, so yy must be empty, as desired.

This version is favoured by classical set theorists as a statement of the axiom, since it uses neither higher-order reasoning (as our first definition does) or infinity (as infinite descent does).

However, neither of these is acceptable in constructive mathematics, since both lemmas require at least the principle of excluded middle to prove at least one direction. In particular, the nonexistence of infinite descending sequences is too weak to allow proofs by transfinite induction (except for special forms of AA), while the requirement that every inhabited pure set have a minimal element is unnecessarily strong and itself implies excluded middle.

More precisely, the necessary set-theoretic axioms for the above proofs are the following. (Is it known, in any case, that proofs using fewer axioms don’t exist?)

  • The “only if” direction of Lemma requires only the axiom of infinity (for “infinite sequence” to make sense).

  • The “if” direction of Lemma evidently requires the principle of excluded middle, the axiom of infinity, and the axiom of dependent choice. It also appears to require the axiom of collection (since dependent choice, as usually stated, only chooses elements from a sequence of nonempty sets, rather than nonempty classes), and a principle of induction strong enough to recursively construct functions into a proper class (which is usually proven using the axiom of separation) in order to put together these nonempty sets into a sequence we can apply dependent choice to.

  • The “only if” direction of Lemma requires only excluded middle.

  • The “if” direction of Lemma requires excluded middle, also that every set is contained in a transitive one (the axiom of transitive closure, which follows from replacement), as well as the axiom of separation in the form “the intersection of any class with a set is a set.”

Another version of the axiom of foundation which is intuitionistically acceptable, but makes no reference to proper classes is:


The axiom of foundation holds if and only if the relation \in on any transitive set is a well-founded relation.


Suppose the axiom of foundation holds, let xx be a transitive set, and let SxS\subseteq x be such that for any yxy\in x, if all tyt\in y are in SS, then ySy\in S. Let AA be the class of all sets yy such that if yxy\in x, then ySy\in S; then AA satisfies the conditions in the axiom of foundation, so it contains all sets, and hence S=xS=x.

Now suppose \in is well-founded on any transitive set and let AA satisfy the conditions in foundation. Since every set is contained in a transitive one, it suffices to show that Ax=xA\cap x = x for any transitive xx, but this follows directly from the assumption.

In this case:

  • The “only if” direction requires no notable axioms at all, while

  • The “if” direction requires transitive closure, as in Lemma , and also the axiom of separation.

Finally, another commonly cited version of foundation, equivalent to it at least over the other axioms of ZF, is:


The axiom of foundation holds if and only if every pure set is an element of V αV_\alpha for some ordinal α\alpha.

Here the V αV_\alpha are the cumulative hierarchy defined by transfinite recursion? as V α=P( β<αV β)V_\alpha = P(\bigcup_{\beta\lt \alpha} V_\beta).


Most of set theory works without the axiom of foundation, but not the deep study of well-founded pure sets. However, one might want to do material set theory without assuming that all sets are well-founded, then one would not assume this axiom.

Alternatively, one can adopt the axiom of anti-foundation, which says:

Since any relation has an extensional quotient, we may also phrase the axiom thus:

  • Given any binary relation \prec on any set SS, there exists a unique transitive set UU and surjection f:SUf : S \to U such that f(s 1)f(s 2)f(s_1) \in f(s_2) if and only if s 1s 2s_1 \in s_2, for s 1,s 2s_1, s_2 in SS. (That is, ff is almost an isomorphism between (S,)(S, \prec) and (U,)(U, \in), but needn’t be injective.)

Just as there are several versions of an extensional relation, there are several versions of this axiom. Note that the existence part of the statement is a set-formation axiom, while the uniqueness part is a strong version of the axiom of extensionality (which is equivalent to the usual one for well-founded sets).

If you include the hypothesis that \prec be well-founded, then the statement is a theorem (Mostowski's collapsing lemma), while the converse is the axiom of foundation.

If you adopt the axiom of anti-foundation (with the strongest notion of extensional relation) instead of foundation, then the universe of pure sets becomes the corecursively defined ill-founded sets instead of the recursively defined well-founded sets.

Structural meaning

Since the axiom of foundation is about pure sets, there seems little point to it in a structural set theory. However, it does have a structural consequence: every set SS is the underlying set of elements of a well-founded model for a pure set (in any of the ways described at pure set). If one assumes the axiom of choice, however, then this statement follows from the well-ordering theorem, since in that case SS is the underlying set of a model for a von Neumann ordinal number. But the axiom of foundation has no stronger structural consequence, since this statement already suffices to ensure that a model of structural set theory can be reconstructed from the material set theory consisting of its well-founded pure sets.

That this statement is the correct structural version of antifoundation may be justified by appeal to the material-structural adjunction.

See also

Last revised on November 20, 2022 at 00:09:54. See the history of this page for a list of all contributions to it.