Well-founded relation


In mathematics, a binary relation R is called well-founded on a class X if every non-empty subset SX has a minimal element with respect to R, that is, an element m not related by sRm for any sS. In other words, a relation is well founded if
Some authors include an extra condition that R is set-like, i.e., that the elements less than any given element form a set.
Equivalently, assuming the axiom of dependent choice, a relation is well-founded if it contains no countable infinite descending chains: that is, there is no infinite sequence x0, x1, x2,... of elements of X such that xn+1 R xn for every natural number n.
In order theory, a partial order is called well-founded if the corresponding strict order is a well-founded relation. If the order is a total order then it is called a well-order.
In set theory, a set x is called a well-founded set if the set membership relation is well-founded on the transitive closure of x. The axiom of regularity, which is one of the axioms of Zermelo–Fraenkel set theory, asserts that all sets are well-founded.
A relation R is converse well-founded, upwards well-founded or Noetherian on X, if the converse relation R−1 is well-founded on X. 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.

Induction and recursion

An important reason that well-founded relations are interesting is because a version of transfinite induction can be used on them: if is a well-founded relation, P is some property of elements of X, and we want to show that
it suffices to show that:
That is,
Well-founded induction is sometimes called Noetherian induction, after Emmy Noether.
On par with induction, well-founded relations also support construction of objects by transfinite recursion. Let be a set-like well-founded relation and F a function that assigns an object F to each pair of an element xX and a function g on the initial segment of X. Then there is a unique function G such that for every xX,
That is, if we want to construct a function G on X, we may define G using the values of G for y R x.
As an example, consider the well-founded relation, where N is the set of all natural numbers, and S is the graph of the successor function xx+1. Then induction on S is the usual mathematical induction, and recursion on S gives primitive recursion. If we consider the order relation, we obtain complete induction, and course-of-values recursion. The statement that is well-founded is also known as the well-ordering principle.
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 set is a set of recursively-defined data structures, the technique is called structural induction. When the well-founded relation is set membership on the universal class, the technique is known as ∈-induction. See those articles for more details.

Examples

Well-founded relations which are not totally ordered include:
Examples of relations that are not well-founded include:
If 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. Consider the following example:
Let X be the union of the positive integers and a new element ω, which is bigger than any integer. Then X is a well-founded set, but
there are descending chains starting at ω of arbitrary great 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 which is extensional, there exists a class C such that is isomorphic to.

Reflexivity

A relation R is said to be reflexive if aRa holds for every a in the domain of the relation. Every reflexive relation on a nonempty domain has infinite descending chains, because any constant sequence is a descending chain. For example, in the natural numbers with their usual order ≤, we have To avoid these trivial descending sequences, when working with a partial order ≤, it is common to apply the definition of well foundedness to the alternate relation < defined such that a < b if and only if ab and ab. More generally, when working with a preorder ≤, it is common to use the relation < defined such that a < b if and only if ab and ba. In the context of the natural numbers, this means that the relation <, which is well-founded, is used instead of the relation ≤, which is not. In some texts, the definition of a well-founded relation is changed from the definition above to include these conventions.