2
$\begingroup$

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

enter image description here

and

(RCW): enter image description here

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?

  • 0
    Matt, it appears two lines before the exercise. :-)2012-12-04

1 Answers 1

1

As Arthur pointed out in the comments you need to prove the equivalence between DC and the statement in Theorem 4.24 (p. 58).

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.