# Dependent Choice for Finite Sets

## Theorem

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

For each $a \in S$, let $C_a = \left\{{ b \in S: a \mathrel{\mathcal R} b }\right\}$

Suppose that:

For all $a \in S$, $C_a$ is a non-empty finite set.

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}$

## Remark

This theorem follows trivially from Dependent Choice (Fixed First Element), a form of the Axiom of Dependent Choice.

The proof below shows that it follows from the weaker Axiom of Countable Choice for Finite Sets.

## Proof

Define $\langle D_n \rangle$ recursively:

Let $D_0 = \left\{{s}\right\}$.

For each $n \in \N$ let $D_{n+1} = \mathcal R \left({D_n}\right)$.

Now, for each $n \in \N$ let $E_n$ be the set of all enumerations of $D_n$.

Then $E_n$ is non-empty and finite for each $n$.

By the Axiom of Countable Choice for Finite Sets, there is a sequence $\langle e_n \rangle$ such that for each $n$, $e_n \in E_n$.

Now recursively define $\left\langle{x_n}\right\rangle$:

Define $x_0$ as $s$.
Define $x_{n+1}$ as the first element in the enumeration $e_n$ which is in $\mathcal R(x_n)$.

Then $\langle x_n \rangle$ is the required sequence.

$\blacksquare$

## Axiom:Axiom of Countable Choice for Finite Sets

This theorem depends on Axiom:Axiom of Countable Choice for Finite Sets.

Although not as strong as the Axiom of Choice, Axiom:Axiom of Countable Choice for Finite Sets is similarly independent of the Zermelo-Fraenkel axioms.

As such, mathematicians are generally convinced of its truth and believe that it should be generally accepted.