Vtyjkyuk

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 $Aneqvarnothing$, a mapping $varphi:Ato P(A
)setminus varnothing$, and $barain A$. Then there exists a sequence

$$(a_n)_nin mathbbN$$

such that $a_0=bara$ and $a_n+1in varphi(a_n)$ for all $nin mathbbN$

Axiom of Choice:

Given a collection $A$ of nonempty sets, there exists a function

$$c: A to bigcup_A_i in AA_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 $mathcalR$ on $A$ such that for all $ain A$, there exists $bin A$ such that $amathcalRb$. There exists a sequence

$$(a_n)_nin mathbbN$$

such that $a_nmathcalRa_n+1$ for all $n in mathbbN$.

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 $Xin P(A)setminus varnothing$.

Let $barvarphi=varphi'circ varphi:Ato Aimpliesbarvarphi(a)=varphi'(varphi(a))in varphi(bara)$ for all $ain A$

To sum up, we have $barvarphi:Ato A$ and $barain A$. Applying Recursion Theorem, we get a sequence $$(a_n)_nin mathbbN$$ such that $a_0=bara$ and $a_n+1=barvarphi(a_n)invarphi(a_n)$ for all $nin mathbbN$.

So this $(a_n)_nin mathbbN$ 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) = bara$ 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.

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