Well-Founded Relation has no Relational Loops

Theorem

Let $\RR$ be a well-founded relation on $S$.

Let $x_1, x_2, \ldots, x_n \in S$.

Then:

$\neg \paren {\paren {x_1 \mathrel \RR x_2} \land \paren {x_3 \mathrel \RR x_4} \land \cdots \land \paren {x_n \mathrel \RR x_1} }$

That is, there are no relational loops within $S$.

Proof

Since $x_1, x_2, \ldots, x_n \in S$, there exists a non-empty subset $T$ of $S$ such that:

$T = \set {x_1, x_2, \ldots, x_n}$

By the definition of a well-founded relation:

$(1): \quad \exists z \in T: \forall y \in T \setminus z: \neg y \mathrel \RR z$

Aiming for a contradiction, suppose $\paren {x_1 \mathrel \RR x_2} \land \paren {x_2 \mathrel \RR x_3} \land \cdots \land \paren {x_n \mathrel \RR x_1}$.

We have that the elements of $T$ are $x_1, x_2, \ldots, x_n$.

Hence:

$\forall y \in T: \exists z \in T \setminus z: y \mathrel \RR z$

This then contradicts $(1)$.

Hence:

$\neg \paren {\paren {x_1 \mathrel \RR x_2} \land \paren {x_3 \mathrel \RR x_4} \land \cdots \land \paren {x_n \mathrel \RR x_1} }$

and so it follows that a well-founded relation has no relational loops.

$\blacksquare$

Sources

• 1996: Winfried Just and Martin Weese: Discovering Modern Set Theory. I: The Basics ... (previous) ... (next): Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $8$