All definitions tacitly require the homogeneous relation
A term's definition may require additional properties that are not listed in this table.
In mathematics, a binary relation R is called well-founded (or wellfounded or foundational[1]) on a set or, more generally, a class X if every non-empty subset S ⊆ X has a minimal element with respect to R; that is, there exists an m ∈ S such that, for every s ∈ S, one does not have s R m. In other words, a relation is well-founded if:
Equivalently, assuming the axiom of dependent choice, a relation is well-founded when it contains no infinite descending chains, which can be proved when there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.[2][3] In order theory, a partial order is called well-founded if the corresponding strict order is a well-founded relation.
In this case R is also said to satisfy the ascending chain condition.
In the context of rewriting systems, a Noetherian relation is also called terminating.
An important reason that well-founded relations are interesting is because a version of transfinite induction can be used on them: if (X, R) is a well-founded relation, P(x) is some property of elements of X, and we want to show that it suffices to show that: That is,
On par with induction, well-founded relations also support construction of objects by transfinite recursion.
As an example, consider the well-founded relation (N, S), where N is the set of all natural numbers, and S is the graph of the successor function x ↦ x+1.
If we consider the order relation (N, <), we obtain complete induction, and course-of-values recursion.
There are other interesting special cases of well-founded induction.
When the well-founded relation is the usual ordering on the class of all ordinal numbers, the technique is called transfinite induction.
When the well-founded relation is set membership on the universal class, the technique is known as ∈-induction.
Well-founded relations that are not totally ordered include: Examples of relations that are not well-founded include: If (X, <) is a well-founded relation and x is an element of X, then the descending chains starting at x are all finite, but this does not mean that their lengths are necessarily bounded.
Then X is a well-founded set, but there are descending chains starting at ω of arbitrary great (finite) length; the chain ω, n − 1, n − 2, ..., 2, 1 has length n for any n. The Mostowski collapse lemma implies that set membership is a universal among the extensional well-founded relations: for any set-like well-founded relation R on a class X that is extensional, there exists a class C such that (X, R) is isomorphic to (C, ∈).
For example, in the natural numbers with their usual order ≤, we have 1 ≥ 1 ≥ 1 ≥ .... To avoid these trivial descending sequences, when working with a partial order ≤, it is common to apply the definition of well foundedness (perhaps implicitly) to the alternate relation < defined such that a < b if and only if a ≤ b and a ≠ b.
More generally, when working with a preorder ≤, it is common to use the relation < defined such that a < b if and only if a ≤ b and b ≰ a.