Equivalence of Definitions of Well-Founded Relation
Theorem
Let $\struct {S, \RR}$ be a Relational Structure.
The following definitions of the concept of Well-Founded Relation are equivalent:
Definition 1
$\RR$ is a well-founded relation on $S$ if and only if:
- $\forall T \subseteq S: T \ne \O: \exists z \in T: \forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
where $\O$ is the empty set.
Definition 2
$\RR$ is a well-founded relation on $S$ if and only if:
- for every non-empty subset $T$ of $S$, $T$ has a minimal element.
Proof
By definition of minimal element:
- $\forall y \in T: y \preceq x \implies x = y$
$(1)$ implies $(2)$
Let $\RR$ be a well-founded relation by definition $1$.
Then by definition:
- $\forall T \subseteq S: T \ne \O: \exists z \in T: \forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
So, let $T \subseteq S: T \ne \O$.
That is, $T$ is a non-empty subset of $S$.
It is asserted that there exists $z \in T \setminus \set z$ such that:
- $\forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
This does not exclude the case that $\tuple {z, z} \in \RR$.
So if there exists $y \in T$ such that $\tuple {y, z} \in \RR$, then it must be the case that $y = z$
That is:
- $\forall y \in T: \tuple {y, z} \in \RR \implies y = z$
That is, $z$ is a minimal element of $T$ under $\RR$.
So we have shown that:
- for every non-empty subset $T$ of $S$, there exists an element $z$ in $T$ such that $z$ is a minimal element of $T$.
Thus $\RR$ is a well-founded relation by definition $2$.
$\Box$
$(2)$ implies $(1)$
Let $\RR$ be a well-founded relation by definition $2$.
Then by definition:
- for every non-empty subset $T$ of $S$, $T$ has a minimal element.
That is, for every non-empty subset $T$ of $S$, there exists an element $z$ in $T$ such that:
- $\forall y \in T: \tuple {y, z} \in \RR \implies y = z$
Hence:
- $\forall y \in T \setminus \set z: \tuple {y, z} \in \RR \implies y = z$
But:
- $\not \exists y \in T \setminus \set z: y = z$
and so it follows that:
- $\forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
That is:
- $\forall T \subseteq S: T \ne \O: \exists z \in T: \forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
Thus $\RR$ is a well-founded relation by definition $1$.
$\blacksquare$