View source for Well-founded relation

[[Category:TeX done]]

''well-founded partial order''

A ([[Partial order|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|Totally ordered set]]) that is well-founded makes $A$ a [[Well-ordered set|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. [[#References|[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|topos]].

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