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.

This relation has well-foundedness without Axiom of foundation or axiom of choice. If a nonempty set $S$ had no minimal member, put $b=\bigcap S$. For each $y\in S$, choose existentially an $x\in S$ with $xRy$. Since $b\subseteq x\cap y$, every subset of $b$ belongs to $y$. Thus $\mathcal{P}(b)\subseteq b$. But $d=\{u\in b:u\notin u\}$ is then an element of $b$, contradicting $d\in d⟺d\notin d$.

This well-founded relation is well-founded without the axiom of choice or Axiom of foundation. If a nonempty set $A$ lacked a minimal member, put $b=\bigcap A$. For each $y\in A$, some $x\in A$ has $\mathcal{P}(x)\subseteq y$, and $b\subseteq x$ gives $\mathcal{P}(b)\subseteq y$. Hence $\mathcal{P}(b)\subseteq b$. The Cantor diagonal argument applied to $d=\{u\in b:u\notin u\}$ contradicts this inclusion.

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.

A map $f:a\to \mathcal{P}(a)$ is recursive if every map $g:\mathcal{P}(b)\to b$ admits a unique $h:a\to b$ with $h(y)=g(\{h(x):x\in f(y)\})$. This holds exactly when the predecessor relation $x\in f(y)$ is a well-founded relation. For the forward construction, take the union of all consistent partial solutions on downward-closed domains; well-founded induction proves compatibility, and a minimal missing point allows extension. Conversely, a nonempty subset with no minimal point has an upward reachability closure $T$ satisfying $y\in T$ exactly when some predecessor is in $T$. With $b=\{0,1\}$ and $g(S)=1$ exactly when $1\in S$, both the zero map and the indicator of $T$ solve the recursion, contradicting uniqueness.

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\}$.

The rank of a terminal node is zero; the rank of any node is the supremum of the successor ranks of its immediate extensions. The rank of the empty node gives one convention for tree height. Every countable well-founded tree has countable rank. Changing between empty-root rank and successive leaf-deletion order changes harmless endpoint conventions.

This hierarchy measures the complexity of successive finite selections. Start with ${\mathcal{M}}_0=\{\varnothing \}$. At a successor stage, retain the previous family and allow one smaller integer to be prepended. At a countable limit $\lambda$, choose positive ordinals ${\lambda }_j\uparrow \lambda$ and admit sets in ${\mathcal{M}}_{{\lambda }_j}$ whose minimum is at least $j$. Each family is hereditary and spreading, has no infinite branch, and its extension-tree rank on every infinite subset is at least $\alpha$. These properties make the hierarchy useful for transfinite constructions of unconditional basic sequences.

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.