nLab
well-founded relation

A (binary) relation $\prec$ on a set $S$ is called well-founded if it is valid to do induction on $\prec$ over $S$.

Definition

Given a subset $A$ of $S$, suppose that $A$ has the property that, given any element $x$ of $S$, if

$$\forall (t:S),t\prec x\Rightarrow t\in A,$$\forall (t: S),\; t \prec x \Rightarrow t \in A ,

then $x\in A$. Such an $A$ may be called a $\prec$-inductive subset of $S$. The relation $\prec$ is well-founded if the only $\prec$-inductive subset of $S$ is $S$ itself.

Note that this is precisely what is necessary to validate induction over $\prec$: if we can show that a statement is true of $x\in S$ whenever it is true of everything $\prec$-below $x$, then it must be true of everything in $S$. In the presence of excluded middle it is equivalent to other commonly stated definitions; see “alternative formulations” below.

Examples

Let $S$ be a finite set. Then any relation on $S$ is well-founded.

Let $S$ be the set of natural numbers, and let $x\prec y$ if $y$ is the successor of $x$: $y=x+1$. That this relation is well-founded is the usual principle of mathematical induction.

Again let $S$ be the set of natural numbers, but now let $x\prec y$ if $x<y$ in the usual order. That this relation is well-founded is the principle of strong induction.

More generally, let $S$ be a set of ordinal numbers (or even the proper class of all ordinal numbers), and let $x\prec y$ if $x<y$ in the usual order. That this relation is well-founded is the principle of transfinite induction.

Let $S$ be the set of positive integers, and let $x\prec y$ mean that $x$ divides $y$: $x\mid y$, or $y/x$ is an integer. This relation is also well-founded, so one can prove properties of integers by induction on their divisors.

Alternative formulations

While the definition above follows how a well-founded relation is generally used (namely, to prove properties of elements of $S$ by induction), it is complicated. Two alternative formulations are given by the following lemmas:

1. The relation $\prec$ is well-founded if and only if there exists no infinite descending sequence $\cdots \prec x_2\prec x_1\prec x_0$.

2. The relation $\prec$ is well-founded if and only if every inhabited subset $A$ of $S$ has a member $x\in A$ such no $t\in A$ satisfies $t\prec x$. (Such an $x$ is called a $\prec$-minimal element of $A$.)

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 $A$), 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 $S$). When necessary, we call a relation with the property of Lemma (2) classically well-founded.

Simulations

Given two sets $S$ and $T$, each equipped with a well-founded relation $\prec$, a function $f:S\to T$ is a simulation of $S$ in $T$ if

• $f(x)\prec f(y)$ whenever $x\prec y$ and
• given $t\prec f(x)$, there exists $y\prec x$ with $t=f(y)$.

Then sets so equipped form a category with simulations as morphisms. See extensional relation for more uses of simulations.

Remarks

Every well-founded relation is irreflexive; that is, $x\nprec x$. Sometimes one wants a reflexive version $⪯$ of a well-founded relation; let $x⪯y$ if and only $x\prec y$ or $x=y$. Then the requirement that $x$ be a minimal element of a subset $A$ states that $t⪯x$ only if $t=x$. But infinite descent or direct proof by induction still require $\prec$ 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 $\in$ 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.