# Condition for Well-Foundedness/Reverse Implication

## Theorem

Let $\left({S, \preceq}\right)$ be an ordered set.

Suppose that there is no infinite sequence $\left \langle {a_n}\right \rangle$ of elements of $S$ such that $\forall n \in \N: a_{n+1} \prec a_n$.

Then $\left({S, \preceq}\right)$ is well-founded.

## Proof 1

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$

## Proof 2

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

Let $T \subseteq S$ have no minimal element.

Let $a_0 \in T$.

We have that $a_0$ is not minimal in $T$.

So:

$\exists a_1 \in T: a_1 \prec a_0$

Similarly, $a_1$ is not minimal in $T$.

So:

$\exists a_2 \in T: a_2 \prec a_1$

Let $a_{k + 1}$ be an arbitrary element for which $a_{k + 1} \prec a_k$.

In order to allow this to be possible in the infinite case, it is necessary to invoke the Axiom of Dependent Choice as follows:

Let $a_k \in T$.

Then as $a_k$ is not minimal in $T$:

$\exists a_{k + 1} \in T: a_{k + 1} \prec a_k$

Hence by definition $\prec$ is a right-total relation.

So, by the Axiom of Dependent Choice, it follows that:

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

Thus we have been able to construct an infinite sequence $\sequence {a_n}$ in $T$ such that:

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

It follows by the Rule of Transposition that 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$

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

$\Box$

## Axiom of Dependent Choice

This theorem depends on the Axiom of Dependent Choice.

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.