# Proof that recursive construction is equivalent to dependent choice

I am trying to prove the following: In Zf, dependent choice (DC) and recursive construction (RCW) are equivalent where

and

(RCW):

Can you tell me if my proof in one direction is correct and help me with the other? Thank you.

(RCW) $\rightarrow$ (DC): Assume RCW and let $R$ be a binary relation on $X$ such that $\forall x \exists y : \langle x, y \rangle \in R$. Pick $x_0 \in X$ and define $G^\ast$ as $\langle f,0 \rangle \mapsto \{x_0\}$ and $\langle f,n \rangle \mapsto \{ x \mid \langle f(k), f(k+1) \rangle \in R \text{ for } 0 \le k \le n-2 \land \langle f(n-1), x\rangle \in R \}$. Then $f(n) \in G^\ast (F\mid I(n), n)$ is the desired sequence.

(DC) $\rightarrow$ (RCW): Assume DC and let $X,Z,W$ and $G^\ast$ be as in RCW. Now we want to define a binary relation $R$ on $X$ such that for every $x$ there is a $y$ such that $\langle x,y\rangle \in R$ and such that the set of the $x_n$ we obtain defines a function $F$ as in $R^\ast$ somehow.

The problem is, I don't see how we can turn our countable sequence into something defining a function defined on a possibly uncountable set. How to prove this direction?

-
As this is certainly from Just-Weese, are you doing Exercise 44 on p.147? If so, I believe it is only talking about Principle of (Un-Generalized) Recursive Constructions from p.58. (And your troubles are quite warranted.) –  Arthur Fischer Dec 4 '12 at 11:23
@ArthurFischer Yes, this is exercise 44 on page 147. That would make sense and solve my problem. Are you sure? –  Rudy the Reindeer Dec 4 '12 at 11:32
Matt, it appears two lines before the exercise. :-) –  Asaf Karagila Dec 4 '12 at 11:32

The idea behind the proof of DC looks fine. Show that there is a $G^\ast$ which satisfies the assumptions of PRC, which is more or less what you did (although you defined it for the wrong principle so some minor adjustment is required, think about $G^\ast(\langle x_0,\ldots x_n\rangle)$ where $x_i$'s form an $R$-chain as the set of all possible continuations, then $F$ gives you the chain).
In the other direction, simply show that if you are given $G^\ast\colon^{<\omega}X\to\mathcal P(X)\setminus\{\varnothing\}$, define $R$ on the domain of $G^\ast$ to be $x R y$ if and only if $y$ is $x$ extended by one element which lies in $G^\ast(x)$. Then $F$ gives you a "coherent" sequence which satisfies the wanted requirements.