Well-founded relation

well-founded partial order

A (partial order) relation on a set $A$ is called well-founded, or recursive, if every non-empty subset of $A$ has a least element with respect to this relation. Thus, a total order on a set $A$ (cf. Totally ordered set) that is well-founded makes $A$ a well-ordered set.

A relation $R\subset A\times A$ on $A$ is well-founded if and only if for any set $B$ and function $g:\mathcal{P}(B)\rightarrow B$ there is a unique function $f$ such that the following diagram commutes (cf. [a1]):

\[ \begin{matrix} A & \xrightarrow{f} & B\\ r\downarrow & & \uparrow g\\ \mathcal{P}(A) & \xrightarrow[\mathcal{P}(f)]{} & \mathcal{P}(B) \end{matrix} \]

Here, $\mathcal{P}(A)$ is the set of all subsets of $A$, $\mathcal{P}(f)(A')=\{f(a'):\, a'\in A'\}$ for $A'\in\mathcal{P}(A)$ and $r(a)=\{a':\, (a, a')\in R\}$. In this form well-foundedness is defined in any elementary topos.

References

[a1]	G. Osius, "Categorical set theory: a characterization of the category of sets" J. Pure Appl. Algebra , 4 (1974) pp. 79–119
[a2]	P. Odifreddi, "Classical recursion theory" , North-Holland (1989) pp. Chapt. II; esp. pp. 199ff
[a3]	R.I. Goldblatt, "Topoi: the categorical analysis of logic" , North-Holland (1984) pp. 318ff