|
|
|
Revision difference : well-founded relation |
| Version 3 |
Version 2 |
| \PMlinkescapeword{class} |
A binary relation $R$ on a \PMlinkname{class}{Class} $X$ is \emph{well-founded} if and only if each nonempty subclass of $X$ contains an $R$-minimal element and, if $X$ is a proper class, then for each $x \in X$, $\lbrace y \mid yRx \rbrace$ is a set. The notion of a well-founded relation is a generalization of that of a well-ordering relation: proof by induction and definition by recursion may be carried out over well-founded relations. |
|
|
| A \PMlinkname{class}{Class} $R$ is a binary relation on a class~$X$ if and only if for each member $r$ of $R$, $r$ is $\langle x, y \rangle$ for a pair $x$, $y$ of members of $X$. If $R$ is a binary relation on the class~$X$ and $Y$ is a subclass of $X$, then $y$ is an $R$-minimal element of $Y$ if and only if $Y$ contains no member $z$ such that $zRy$. |
|
|
|
| A binary relation $R$ on a class $X$ is \emph{well-founded} if and only if |
|
|
|
| \begin{itemize} |
|
| \item each nonempty subclass of $X$ contains an $R$-minimal element and, |
|
| \item for each $x \in X$, $\lbrace y \mid yRx \rbrace$ is a set. |
|
| \end{itemize} |
|
|
|
| The notion of a well-founded relation is a generalization of that of a well-ordering relation: proof by induction and definition by recursion may be carried out over well-founded relations. |
|
|
|
|
|
