In mathematics, a binary relation R is called well-founded (or wellfounded or foundational) on a set or, more generally, a class X if every non-empty subset (or subclass) 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. More formally, a relation is well-founded if:
( ∀ S ⊆ X ) [ S ≠ ∅ ⟹ ( ∃ m ∈ S ) ( ∀ s ∈ S ) ¬ ( s R m ) ] . {\displaystyle (\forall S\subseteq X)\;[S\neq \varnothing \implies (\exists m\in S)(\forall s\in S)\lnot (s\mathrel {R} m)].}
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 when it contains no infinite descending chains, meaning 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 (X, R) is a well-founded relation, P(x) is some property of elements of X, and we want to show that
P(x) holds for all elements x of X, it suffices to show that:
If x is an element of X and P(y) is true for all y such that y R x, then P(x) must also be true. That is,
( ∀ x ∈ X ) [ ( ∀ y ∈ X ) [ y R x ⟹ P ( y ) ] ⟹ P ( x ) ] implies ( ∀ x ∈ X ) P ( x ) . {\displaystyle (\forall x\in X)\;[(\forall y\in X)\;[y\mathrel {R} x\implies P(y)]\implies P(x)]\quad {\text{implies}}\quad (\forall x\in X)\,P(x).}
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 (X, R) be a set-like well-founded relation and F a function that assigns an object F(x, g) to each pair of an element x ∈ X and a function g on the set {y: y R x} of predecessors of x. Then there is a unique function G such that for every x ∈ X,
G ( x ) = F ( x , G | { y : y R x } ) . {\displaystyle G(x)=F\left(x,G\vert _{\left\{y:\,y\mathrel {R} x\right\}}\right).}
That is, if we want to construct a function G on X, we may define G(x) using the values of G(y) for y R x. 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. Then induction on S is the usual mathematical induction, and recursion on S gives primitive recursion. If we consider the order relation (N, <), we obtain complete induction, and course-of-values recursion. The statement that (N, <) 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 that are not totally ordered include:
The positive integers {1, 2, 3, ...}, with the order defined by a < b if and only if a divides b and a ≠ b. The set of all finite strings over a fixed alphabet, with the order defined by s < t if and only if s is a proper substring of t. The set N × N of pairs of natural numbers, ordered by (n1, n2) < (m1, m2) if and only if n1 < m1 and n2 < m2. Every class whose elements are sets, with the relation ∈ ("is an element of"). This is the axiom of regularity. The nodes of any finite directed acyclic graph, with the relation R defined such that a R b if and only if there is an edge from a to b. Examples of relations that are not well-founded include:
… excerpt ends here. Continue reading the full article.
