# How does Axiom of Choice imply Axiom of Dependent Choice?

Axiom of Choice:

Given a collection $A$ of nonempty sets, there exists a function $$c: A \to \bigcup_{A_{i} \in A}A_{i}$$ such that $c(A_{i})\in A_{i}$ for all $A_{i} \in A$.

Axiom of Dependent Choice:

Given a nonempty set $A$ and a binary relation $\mathcal{R}$ on $A$ such that for all $a\in A$, there exists $b\in A$ such that $a\mathcal{R}b$. There exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{n}\mathcal{R}a_{n+1}$ for all $n \in \mathbb{N}$.

Here is my incomplete proof that Axiom of Choice implies Axiom of Dependent Choice:

For $a\in A$, let $R(a)=\{b\in A\mid a\mathcal{R}b\}\implies R(a)\neq\varnothing$ for all $a\in A$.

Using Axiom of Choice for the indexed family of sets $(R(a))_{a\in A}$, there exists a mapping

$$f:A\to A$$ such that $$\forall a\in A:f(a)\in R(a)$$

$\text{That is }\forall a\in A:a\mathcal{R}f(a)$. Let $B=\{(a,f(a))\mid a\in A\}$

I don't know how to proceed to prove the existence of the required sequence $(a_{n})_{n\in \mathbb{N}}$ from set $B$.

• Let $a_n=f^ n(a_0)$, of course. Feb 22, 2018 at 18:16

You're basically done already: pick some $a\in A$ and consider the sequence $$a, f(a),f(f(a)), f(f(f(a))), ...$$ The $f$ that choice provides us is exactly the "strategy" we use to build the desired sequence.

• I think your "strategy" looks like defining a sequence recursively. Is it true that your "strategy" implicitly appeals to Theorem of Recursion (wikiwand.com/en/Recursion#/The_recursion_theorem)? Feb 23, 2018 at 1:27
• @leanhdung No, actually! It follows just from the Separation axiom: we pick $a\in A$ and let $B$ be the set of $b\in A$ such that there is a finite chain of $f$-applications linking $a$ to $b$. This doesn't need the recursion theorem at all. (And incidentally, the recursion theorem doesn't need choice, so even if it was necessary that would be fine.) Feb 23, 2018 at 1:34
• The key point that lets us avoid the recursion theorem (that is, that makes this argument work in the axiom system Z, which is ZF minus Replacement and within which the recursion theorem is not provable) is that everything is taking place inside a fixed set $A$. Feb 23, 2018 at 1:35
• Yes, we only need Axiom of Separation to form such sets $R(a)=\{b\in A\mid a\mathcal{R}b\}$ for all $a\in A$, but what I meant is that you must use Recursion Theorem at the end to form $(a_{n})_{n\in \mathbb{N}}$ from mapping $f:A\to A$. Feb 23, 2018 at 7:58
• @leanhdung No, you don't - you can just use Separation. The application of Separation is a bit more complicated, as my comment says above. The recursion theorem is not needed here. Feb 23, 2018 at 11:39

Once you have $f$, use the assumption that $A$ is nonempty to choose $x \in A$. Now, you can define a sequence recursively by $a_0 = x$, $a_{n+1} = f(a_n)$. (So for example, $a_1 = f(x)$, $a_2 = f(f(x))$, $a_3 = f(f(f(x)))$, etc.)

• Since your answer mentions "define a sequence recursively", is it true that you implicitly appeal to Recursion Theorem (wikiwand.com/en/Recursion#/The_recursion_theorem)? at the end to form $(a_{n})_{n\in \mathbb{N}}$? Feb 23, 2018 at 8:02
• Yes, it uses the existence part of that theorem. Feb 23, 2018 at 17:32

I think you're almost there: now define $$a_0 := a, a_n := f^n(a)$$ for some $a \in A$.

• The way you acquire $(a_{n})_{n\in \mathbb{N}}$ makes me feel like you implicitly appeal to Recursion Theorem (wikiwand.com/en/Recursion#/The_recursion_theorem). Is my understanding true? Feb 23, 2018 at 8:13
• I don't think so. $f^n$ is a well-defined function for all $n \in \mathbb{N}$, so I am defining $a_n$ "explicitly". But I might be wrong, I am not an expert in set theory. Feb 23, 2018 at 8:42
• I am not sure, but isn't the theorem more focused on uniqueness than on existence? Here we don't need uniqueness, and existence is clear from the definition of $f^n$ (I think) Feb 23, 2018 at 8:48