Well-founded relation

A relation $r$ on $X$ is well-founded when every nonempty subset of $X$ contains an element with no $r$-predecessor in that subset.

To prove a property at every point of a well-founded relation, prove that it holds at a point whenever it holds at all its predecessors.

A recursive definition in which the value at a point depends on its predecessor values in a well-founded relation. For a class relation, set-likeness allows the local set recursions to combine into a class function.

An ordinal-valued function strictly increasing along a relation. For a well-founded set relation, or a set-like class relation, the canonical rank is $\rho (y)=\sup \{\rho (x)+1:xRy\}$.

A class relation for which each point has a set of predecessors. This allows the suprema in well-founded recursion to be ordinals rather than proper classes.