How does Axiom of Dependent Choice imply this weaker variant?

Here is the excerpt from the textbook A Course in Mathematical Analysis by Prof D. J. H. Garling. So I have the Theorem 1:

Given a set $A\neq\varnothing$, a mapping $\varphi:A\to P(A )\setminus \{\varnothing\}$, and $\bar{a}\in A$. Then there exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{0}=\bar{a}$ and $a_{n+1}\in \varphi(a_{n})$ for all $n\in \mathbb{N}$

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

The author states that The axiom of dependent choice states that this [Theorem 1] is always possible. But I can only infer Theorem 1 from Axiom of Choice, not from Axiom of Dependent Choice. Below is how I did it.

Using Axiom of Choice for the collection $P(A)\setminus \{\varnothing\}$ of nonempty sets, then there exists a choice function $$\varphi':P(A)\setminus \{\varnothing\} \to A$$ such that $\varphi'(X)\in X$ for all $X\in P(A)\setminus \{\varnothing\}$.

Let $\bar{\varphi}=\varphi'\circ \varphi:A\to A\implies\bar{\varphi}(a)=\varphi'(\varphi(a))\in \varphi(\bar{a})$ for all $a\in A$

To sum up, we have $\bar{\varphi}:A\to A$ and $\bar{a}\in A$. Applying Recursion Theorem, we get a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{0}=\bar{a}$ and $a_{n+1}=\bar{\varphi}(a_{n})\in\varphi(a_{n})$ for all $n\in \mathbb{N}$. So this $(a_{n})_{n\in \mathbb{N}}$ is the required sequence.

I would like you to check my above proof and check whether it is possible for Axiom of Dependent Choice to imply Theorem 1.

Many thanks for your help!

Here is how I would think about the problem:

Let $T$ be the set of all finite functions $$s \colon n \to A$$ such that $n \in \mathbb N$, $s(0) = \bar{a}$ and, for all $i +1 < n$, $$s(i+1) \in \phi(s(i)).$$ Let $R \subseteq T \times T$ be given by $$R = \{(s,t) \in T^2 \mid t \text{ is a proper end-extension of } s \} = \{ (s,t) \in T^2 \mid s \subsetneq t \}$$

$R$ satisfies the requirement of DC (since $\phi(a) \neq \emptyset$ for all $a \in A$). Hence there is an infinite sequence (branch) $(s_n \mid n \in \mathbb N)$ through $T$ such that for all $m < n \in \mathbb N \colon s_m \subsetneq s_n$. Let $s := \bigcup_{n \in \mathbb N} s_n$. For each $k \in \mathbb N$ let $a_k := s(k)$. Then $(a_k \mid n \in \mathbb N)$ is as desired.

• The above also suggest how you can reformulate DC into an equivalent statement that is a generalization of Kőnig's lemma. I find that reformulation much easier to work with in practice. (Mind you: There is a good chance this is only true because I've been inflicted with the 'just build a search tree' virus of inner model theory.) – Stefan Mesken Feb 23 '18 at 13:55
• To some extent, the tree variant is the clearer version of DC. The reason is that it's easy to translate it into pretty much every other variant. – Asaf Karagila Feb 23 '18 at 14:50
• @leanhdung No, it's $s \colon n \to A$ -- they are functions with finite domain. (But you should note that, in my notation, $n = \{0,1, \ldots, n-1 \}$ -- that's standard among set theorists but maybe not among other mathematicians.) – Stefan Mesken Feb 24 '18 at 8:10
• @leanhdung At that point I'm not making any choices -- I simply collect all of those sequences into a set (a priori it could be that there just aren't that many such sequences). Then, in a second step, I use DC to show that not only are there infinitely many such sequences -- there is even an infinite 'chain' (a branch) of them. This may not be true in the absence of DC. (Side note: I usually don't take a stance on the 'philosophical truth' of axioms but I must say -- to me DC seems 'true', it's almost mind bending to me to imagine a situation in which it could possibly fail.) – Stefan Mesken Feb 24 '18 at 10:23
• Now I got that point, but i'm still not sure how $R$ satisfies the requirement of DC i.e for all $s\in T$, there exists $s'\in T$ such that $s\subsetneq s'$. Please check my reasoning: 1. Assume $s: n\to A$ such that $s\in T$, let $s': n+1\to A$ such that $s'(x)=s(x)$ for all $x\leqslant n-1$ and $s'(n)\in \phi(s(n-1))\implies s'\in T$ and $s'\subsetneq s$. – MadnessFor MATH Feb 26 '18 at 3:48

Let $\mathcal R =\{ (a,b) \in A \times A \mid a,b \in A \text{ and } b \in \phi(a) \}$, then $\mathcal R$ satisfies DC's requirement. Hence there is an infinite sequence (branch) $(a_n \mid n \in \mathbb N)$ through $A$ such that $a_{n+1} \in \phi(a_n)$ for all $n \in \mathbb N$.