View source for Well-founded relation

''well-founded partial order''

A ([[Partial order|partial order]]) relation on a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976401.png" /> is called well-founded, or recursive, if every non-empty subset of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976402.png" /> has a least element with respect to this relation. Thus, a total order on a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976403.png" /> (cf. [[Totally ordered set|Totally ordered set]]) that is well-founded makes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976404.png" /> a [[Well-ordered set|well-ordered set]].

A relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976405.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976406.png" /> is well-founded if and only if for any set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976407.png" /> and function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976408.png" /> there is a unique function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w0976409.png" /> such that the following diagram commutes (cf. [[#References|[a1]]]):

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w09764010.png" /></td> </tr></table>

Here, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w09764011.png" /> is the set of all subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w09764012.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w09764013.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w09764014.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/w/w097/w097640/w09764015.png" />. 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>