# Condition for Well-Foundedness

## Theorem

Let $\struct {S, \preceq}$ be an ordered set.

Then $\struct {S, \preceq}$ is well-founded if and only if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:

- $\forall n \in \N: a_{n + 1} \prec a_n$

That is, if and only if there is no infinite sequence $\sequence {a_n}$ such that $a_0 \succ a_1 \succ a_2 \succ \cdots$.

## Proof

### Reverse Implication

Suppose $\struct {S, \preceq}$ is not well-founded.

So by definition there exists a non-empty subset $T$ of $S$ which has no minimal element.

Let $a \in T$.

Since $a$ is not minimal in $T$, we can find $b \in T: b \prec a$.

Since this holds for all $a \in T$, $\prec \restriction_{T \times T}$, the restriction of $\prec$ to $T \times T$, is a right-total endorelation on $T$.

So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence $\sequence {a_n}$ in $T$ such that $\forall n \in \N: a_{n + 1} \prec a_n$.

$\Box$

### Forward Implication

Suppose there exists an infinite sequence $\sequence {a_n}$ in $S$ such that:

- $\forall n \in \N: a_{n + 1} \prec a_n$

We let $T = \set {a_0, a_1, a_2, \ldots}$.

Clearly $T$ has no minimal element.

Thus by definition $S$ is not well-founded.

$\blacksquare$

## Axiom of Dependent Choice

This theorem depends on the Axiom of Dependent Choice, by way of Condition for Well-Foundedness/Reverse Implication.

Although not as strong as the Axiom of Choice, the Axiom of Dependent Choice is similarly independent of the Zermelo-Fraenkel axioms.

The consensus in conventional mathematics is that it is true and that it should be accepted.

## Sources

- 1993: Keith Devlin:
*The Joy of Sets: Fundamentals of Contemporary Set Theory*(2nd ed.) ... (previous) ... (next): $\S 1$: Naive Set Theory: $\S 1.5$: Relations: Lemma $1.5.1$ - 1997: Donald E. Knuth:
*The Art of Computer Programming: Volume 1: Fundamental Algorithms*(3rd ed.) ... (previous) ... (next): $\S 1.2.1$: Mathematical Induction: Exercise $15 \ \text{(f)}$