A (binary) relation on a set is called well-founded if it is valid to do induction on over .
Given a subset of , suppose that has the property that, given any element of , if
then . Such an may be called a -inductive subset of . The relation is well-founded if the only -inductive subset of is itself.
Note that this is precisely what is necessary to validate induction over : if we can show that a statement is true of whenever it is true of everything -below , then it must be true of everything in . In the presence of excluded middle it is equivalent to other commonly stated definitions; see “alternative formulations” below.
Let be a finite set. Then any relation on is well-founded.
Let be the set of natural numbers, and let if is the successor of : . That this relation is well-founded is the usual principle of mathematical induction.
Again let be the set of natural numbers, but now let if in the usual order. That this relation is well-founded is the principle of strong induction.
More generally, let be a set of ordinal numbers (or even the proper class of all ordinal numbers), and let if in the usual order. That this relation is well-founded is the principle of transfinite induction.
Let be the set of positive integers, and let mean that divides : , or is an integer. This relation is also well-founded, so one can prove properties of integers by induction on their divisors.
While the definition above follows how a well-founded relation is generally used (namely, to prove properties of elements of by induction), it is complicated. Two alternative formulations are given by the following lemmas:
The relation is well-founded if and only if there exists no infinite descending sequence .
The relation is well-founded if and only if every inhabited subset of has a member such no satisfies . (Such an is called a -minimal element of .)
Lemma (1) is essentially Fermat's method of infinite descent. Lemma (2) is traditionally used to state the axiom of foundation, since then it may be expressed as a single axiom (rather than a schema) that doesn't really on infinity (as infinite descent does). Either may be seen in the literature as simpler than our definition above.
However, neither of these is acceptable in constructive mathematics, since both lemmas require the principle of excluded middle to prove one direction. The nonexistence of infinite descending sequences is too weak to allow proofs by induction (except for special forms of ), although it is sufficient to establish the Burali-Forti paradox?. On the other hand, the requirement that every inhabited subset have a minimal element is too strong to ever be established (except for degenerate cases of ). When necessary, we call a relation with the property of Lemma (2) classically well-founded.
Given two sets and , each equipped with a well-founded relation , a function is a simulation of in if
Then sets so equipped form a category with simulations as morphisms. See extensional relation for more uses of simulations.
Every well-founded relation is irreflexive; that is, . Sometimes one wants a reflexive version of a well-founded relation; let if and only or . Then the requirement that be a minimal element of a subset states that only if . But infinite descent or direct proof by induction still require rather than .
A well order may be defined as a well-founded linear order, or alternatively as a transitive, extensional, well-founded relation.
The axiom of foundation in material set theory states precisely that the membership relation 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.