Template:Short description Template:Redirect Template:Stack

In mathematics, a binary relation Template:Mvar is called well-founded (or wellfounded or foundational<ref>See Definition 6.21 in Template:Cite book</ref>) on a set or, more generally, a class Template:Mvar if every non-empty subset Template:Math has a minimal element with respect to Template:Mvar; that is, there exists an Template:Math such that, for every Template:Math, one does not have Template:Math. In other words, a relation is well-founded if: <math display=block>(\forall S \subseteq X)\; [S \neq \varnothing \implies (\exists m \in S) (\forall s \in S) \lnot(s \mathrel{R} m)].</math> Some authors include an extra condition that Template:Mvar 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 Template:Math of elements of Template:Mvar such that Template:Math for every natural number Template:Mvar.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref><ref>Template:Cite book</ref>

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 Template:Mvar is called a well-founded set if the set membership relation is well-founded on the transitive closure of Template:Mvar. The axiom of regularity, which is one of the axioms of Zermelo–Fraenkel set theory, asserts that all sets are well-founded.

A relation Template:Mvar is converse well-founded, upwards well-founded or Noetherian on Template:Mvar, if the converse relation Template:Math is well-founded on Template:Mvar. In this case Template:Mvar is also said to satisfy the ascending chain condition. In the context of rewriting systems, a Noetherian relation is also called terminating.

Induction and recursionEdit

An important reason that well-founded relations are interesting is because a version of transfinite induction can be used on them: if (Template:Math) is a well-founded relation, Template:Math is some property of elements of Template:Mvar, and we want to show that

Template:Math holds for all elements Template:Mvar of Template:Mvar,

it suffices to show that:

If Template:Mvar is an element of Template:Mvar and Template:Math is true for all Template:Mvar such that Template:Math, then Template:Math must also be true.

That is, <math display=block>(\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).</math>

Well-founded induction is sometimes called Noetherian induction,<ref>Bourbaki, N. (1972) Elements of mathematics. Commutative algebra, Addison-Wesley.</ref> after Emmy Noether.

On par with induction, well-founded relations also support construction of objects by transfinite recursion. Let Template:Math be a set-like well-founded relation and Template:Mvar a function that assigns an object Template:Math to each pair of an element Template:Math and a function Template:Mvar on the initial segment Template:Math of Template:Mvar. Then there is a unique function Template:Mvar such that for every Template:Math, <math display=block>G(x) = F\left(x, G\vert_{\left\{y:\, y\mathrel{R}x\right\}}\right).</math>

That is, if we want to construct a function Template:Mvar on Template:Mvar, we may define Template:Math using the values of Template:Math for Template:Math.

As an example, consider the well-founded relation Template:Math, where Template:Math is the set of all natural numbers, and Template:Mvar is the graph of the successor function Template:Math. Then induction on Template:Mvar is the usual mathematical induction, and recursion on Template:Mvar gives primitive recursion. If we consider the order relation Template:Math, we obtain complete induction, and course-of-values recursion. The statement that Template:Math 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.

ExamplesEdit

Well-founded relations that are not totally ordered include:

Examples of relations that are not well-founded include:

  • The negative integers Template:Math, with the usual order, since any unbounded subset has no least element.
  • The set of strings over a finite alphabet with more than one element, under the usual (lexicographic) order, since the sequence Template:Nowrap is an infinite descending chain. This relation fails to be well-founded even though the entire set has a minimum element, namely the empty string.
  • The set of non-negative rational numbers (or reals) under the standard ordering, since, for example, the subset of positive rationals (or reals) lacks a minimum.

Other propertiesEdit

If Template:Math is a well-founded relation and Template:Mvar is an element of Template:Mvar, then the descending chains starting at Template:Mvar are all finite, but this does not mean that their lengths are necessarily bounded. Consider the following example: Let Template:Mvar be the union of the positive integers with a new element ω that is bigger than any integer. Then Template:Mvar is a well-founded set, but there are descending chains starting at ω of arbitrary great (finite) length; the chain Template:Math has length Template:Mvar for any Template:Mvar.

The Mostowski collapse lemma implies that set membership is a universal among the extensional well-founded relations: for any set-like well-founded relation Template:Mvar on a class Template:Mvar that is extensional, there exists a class Template:Mvar such that Template:Math is isomorphic to Template:Math.

ReflexivityEdit

A relation Template:Mvar is said to be reflexive if Template:Math holds for every Template:Mvar 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 Template:Nowrap. 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 Template:Math if and only if Template:Math and Template:Math. More generally, when working with a preorder ≤, it is common to use the relation < defined such that Template:Math if and only if Template:Math and Template:Math. 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.

ReferencesEdit

Template:Reflist

Template:Mathematical logic Template:Order theory