well-founded relation



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


Let SS be a set, and let \prec be a binary relation on SS. A subset AA of SS is \prec-inductive if

(x:S),((t:S),txtA)xA. \forall (x\colon S),\; (\forall (t\colon S),\; t \prec x \;\Rightarrow\; t \in A) \;\Rightarrow\; x \in A.

The relation \prec is well-founded if the only \prec-inductive subset of SS is SS itself.

Note that this is precisely what is necessary to validate induction over \prec: if we can show that a statement is true of an element xx of SS whenever it is true of everything that precedes (\prec) xx, then it must be true of everything in SS. In the presence of excluded middle it is equivalent to other commonly stated definitions; see Formulations in classical logic below.

Formulations in classical logic

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

  1. The relation \prec has no infinite descent (usually attributed to Pierre de Fermat) if there exists no sequence x 2x 1x 0\cdots \prec x_2 \prec x_1 \prec x_0 in SS. (Such a sequence is called an infinite descending sequence.)

  2. The relation \prec is classically well-founded if every inhabited subset AA of SS has a member xAx \in A such that no tAt \in A satisfies txt \prec x. (Such an xx is called a minimal element of AA.)

In classical mathematics, both of these conditions are equivalent to being well-founded. In constructive mathematics, we may prove that a well-founded relation has no infinite descent (see Proposition 2), but not the converse, and that a classically well-founded relation is well-founded (see Proposition 3), but not the converse.

The classical notion of well-foundedness enforces classical logic onto us, in the following sense.


If (X,)(X, \prec) is an inhabited well-founded relation in a classical sense, then the unrestricted law of excluded middle holds.

For a topos-theoretic proof see here.


Suppose there are xx and yy such that yxy\prec x, and let QQ be an arbitrary proposition. Consider then a set PXP \subset X defined as P={x}{aaxQ}P = \{ x \} \cup \{ a \mid a \prec x \;\wedge\; Q\}. Clearly, the set PP is inhabited, thus by classical well-foundedness it has a minimal element x 0x_0. By intuitionistic reasoning, either x 0x_0 is in {x}\{ x \}, i.e. x 0=xx_0 = x, or x 0{aaxQ}x_0 \in \{ a \mid a \prec x \;\wedge\; Q\}, i.e. x 0xQx_0 \prec x \;\wedge\; Q. In the latter case we immediately see that QQ holds. So, suppose that x 0=xx_0 = x is the minimal element of PP; we will show that ¬Q\neg Q holds. For suppose that QQ holds; then yPy \in P and yx=x 0y \prec x = x_0, violating the condition that x 0x_0 is a minimal element of PP.

Since QQ was an arbitrary proposition, we can deduce Q.(Q¬Q)\forall Q. (Q \vee \neg Q).


We note that classical well-foundedness is really too strong for constructive (i.e., intuitionistic) mathematics, due to Proposition 1. On the other hand, the infinite descent condition is too weak to be of much use in constructive mathematics. It is the inductive notion of well-foundedness that is just right.

Note however that in predicative mathematics, the definition of well-founded may be impossible to even state, and so either of these alternative definitions would be preferable, provided classical logic is used.

Even in constructive predicative mathematics, (1) is strong enough to establish the Burali-Forti paradox (when applied to linear orders). In material set theory, (2) is traditionally used to state the axiom of foundation, although the impredicative definition could also be used as an axiom scheme (and must be in constructive versions). In any case, either (1) or (2) is usually preferred by classical mathematicians as simpler.

To round out the discussion we prove the following two results, both valid in intuitionistic mathematics:


If (X,)(X, \prec) is a well-founded relation and AXA \subseteq X has no minimal element, then AA is empty.

This result makes it trivial to infer (under classical logic) that classical well-foundedness is a consequence of well-foundedness. It also shows that well-foundedness rules out infinite descent (intuitionistically), since an infinite descent sequence has no minimal element.


Let U={uX:uA(x:X),xuxA}U = \{u \in X: u \notin A\; \wedge \; (\forall x: X),\; x \prec u \Rightarrow x \notin A\}. Clearly UA=U \cap A = \emptyset. We show UU is inductive, so that under well-foundedness U=XU = X and A=XA=UA=A = X \cap A = U \cap A = \emptyset, as desired.

So, suppose zz is an element such that yUy \in U whenever yzy \prec z. We must show zUz \in U. Claim: zAz \notin A. For if zAz \in A, then zz would be a minimal element of AA (as yzyUyAy \prec z \Rightarrow y \in U \Rightarrow y \notin A). But this negates the assumption that AA has no minimal element.

Thus zAz \notin A, and yzyUyAy \prec z \Rightarrow y \in U \Rightarrow y \notin A, so that zUz \in U. This completes the proof.


In intuitionistic set theory, classical well-foundedness implies (inductive) well-foundedness.


Let \prec be a classically well-founded relation on XX, and let UU be an inductive subset. We must show that every element xXx \in X belongs to UU. Since UU is inductive, it suffices to show that every uxu \prec x belongs to UU, i.e. we may assume given a uu such that uxu\prec x and show uUu\in U. But under this assumption we have that \prec is inhabited, so according to Remark 1, the law of excluded middle follows and we might as well then argue classically. The argument is well-known but we include it for completeness: under classical well-foundedness, if an inductive subset UU is not the entirety of XX, then the complement ¬U\neg U has a minimal element yy. In that case, vyv \prec y implies v¬¬U=Uv \in \neg\neg U = U, but then yUy \in U since UU is inductive, contradiction. Hence U=XU = X and in particular uUu \in U, which is what we wanted.

To bring us full circle: in classical set theory we may prove that if (X,)(X, \prec) has no infinite descent, then \prec is classically well-founded. For suppose an inhabited subset PXP \subseteq X (say with an element xPx \in P) failed to have a least element. Then we can find an infinite descent sequence x nPx_n \in P with x 0=xx_0 = x, by choosing at each stage x n+1Px_{n+1} \in P such that x n+1x nx_{n+1} \prec x_n. Technically this requires the use of dependent choice, but generally this is felt to be a mild choice principle (that is true even for intuitionistic mathematics).

Coalgebraic formulation

Many inductive or recursive notions may also be packaged in coalgebraic terms. For the concept of well-founded relation, first observe that a binary relation \prec on a set XX is the same as a coalgebra structure θ:XP(X)\theta\colon X \to P(X) for the covariant power-set endofunctor on SetSet, where yxy \prec x if and only if yθ(x)y \in \theta(x).

In this language, a subset i:UXi\colon U \hookrightarrow X is \prec-inductive, or θ\theta-inductive, if in the pullback

H j X θ PU Pi PX\array{ H & \stackrel{j}{\to} & X \\ \downarrow & & \downarrow^\mathrlap{\theta} \\ P U & \underset{P i}{\to} & P X }

the map jj factors through ii. (Note that jj is necessarily monic, since PP preserves monos.) Unpacking this a bit: for any xXx \in X, if θ(x)=V\theta(x) = V belongs to PUP U, that is if θ(x)U\theta(x) \subseteq U, then xUx \in U. This says the same thing as x:X( y:XyxyU)xU\forall_{x\colon X} (\forall_{y\colon X} y \prec x \Rightarrow y \in U) \Rightarrow x \in U.

Then, as usual, the PP-coalgebra (X,θ)(X, \theta) is well-founded if every θ\theta-inductive subset UXU \hookrightarrow X is all of XX.

Other relevant notions may also be packaged; for example, the PP-coalgebra XX is extensional if θ:XPX\theta\colon X \to P X is monic. See also well-founded coalgebra.


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

  1. f(x)f(y)f(x) \prec f(y) whenever xyx \prec y and

  2. given tf(x)t \prec f(x), there exists yxy \prec x with t=f(y)t = f(y).

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

In coalgebraic language, a simulation STS \to T is simply a PP-coalgebra homomorphism f:STf\colon S \to T. Condition (1), that ff is merely \prec-preserving, translates to the condition that ff is a colax morphism of coalgebras, in the sense that there is an inclusion

X θ X PX f Pf Y θ Y PY.\array{ X & \stackrel{\theta_X}{\to} & P X \\ ^\mathllap{f} \downarrow & \swArrow & \downarrow^\mathrlap{P f} \\ Y & \underset{\theta_Y}{\to} & P Y. }

If (X,)(X, \prec) is well-founded and (Y,)(Y, \prec) is (weakly) extensional, then there is at most one simulation f:XYf: X \to Y.


Every well-founded relation is irreflexive; that is, xxx \nprec x. Sometimes one wants a reflexive version \preceq of a well-founded relation; let xyx \preceq y if and only xyx \prec y or x=yx = y. Then the requirement that xx be a minimal element of a subset AA states that txt \preceq x only if t=xt = x. But infinite descent or direct proof by induction still require \prec rather than \preceq.

A well order may be defined as a well-founded linear order, or alternatively as a transitive, extensional, well-founded relation.

A well-quasi-order is a well-founded preorder (referring to the reflexive version of well-foundedness above) that in addition has no infinite antichains.

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.


Let SS be a finite set. Then any relation on SS whose transitive closure is irreflexive is well-founded.

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

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

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

Similarly, let SS be a set of pure sets (or even the proper class of all pure sets), and let xyx \prec y if xyx \in y. That this relation is well-founded is the axiom of foundation.

Let SS be the set of integers, and let xyx \prec y mean that xx properly divides yy: y/xy/x is an integer other than ±1\pm{1}. This relation is also well-founded, so one can prove properties of integers by induction on their proper divisors.

Revised on April 8, 2017 08:33:55 by Toby Bartels (