# Dependent Choice (Fixed First Element)

## Theorem

Let $\mathcal R$ be a binary relation on a non-empty set $S$.

Suppose that:

- $\forall a \in S: \exists b \in S: a \mathrel{\mathcal R} b$

that is, that $\mathcal R$ is a left-total relation (specifically a *serial relation*).

Let $s \in S$.

Then there exists a sequence $\left\langle{x_n}\right\rangle_{n \in \N}$ in $S$ such that:

- $x_0 = s$
- $\forall n \in \N: x_n \mathrel{\mathcal R} x_{n+1}$

## Proof

Let $S' = \left\{{y \in S: s \mathrel{\mathcal R^+} y}\right\}$, where $\mathcal R^+$ is the transitive closure of $\mathcal R$.

Let $\mathcal R'$ be the restriction of $\mathcal R$ to $S'$.

For each $x \in S'$, there is a $y \in S$ such that $x \mathrel{\mathcal R} y$. But then $s \mathrel{\mathcal R^+} y$, so $y \in S'$, so $x \mathrel{\mathcal R'} y$.

Thus $\mathcal R'$ is a left-total relation on $S'$.

$S'$ is non-empty: since $\mathcal R$ is left-total, there is a $t \in S$ such that $s \mathrel{\mathcal R} t$, so $s \mathrel{\mathcal R^+} t$, so $t \in S'$.

By the Axiom of Dependent Choice, there is a infinite sequence $\left\langle{ y_n}\right\rangle_{n \in \N}$ in $S'$ such that for each $n \in \N$, $y_n \mathrel{\mathcal R'} y_{n+1}$.

Then by the definition of restriction, $y_n \mathrel{\mathcal R} y_{n+1}$ for each $n \in \N$.

By the definition of $S'$, $s \mathrel{\mathcal R^+} y_0$.

By the definition of transitive closure, there are elements $x_0, \dots, x_m$ such that $s = x_0 \mathrel{\mathcal R} x_1 \mathrel{\mathcal R} \cdots \mathrel{\mathcal R} x_m \mathrel{\mathcal R} x_m = y_0$.

Then for $n > m$, define $x_n$ as $y_{n-m}$.

This sequence then meets the requirements.

$\blacksquare$

## 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.