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

enter image description here


(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?

  • 2
    $\begingroup$ 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.) $\endgroup$ – user642796 Dec 4 '12 at 11:23
  • $\begingroup$ @ArthurFischer Yes, this is exercise 44 on page 147. That would make sense and solve my problem. Are you sure? $\endgroup$ – Rudy the Reindeer Dec 4 '12 at 11:32
  • $\begingroup$ Matt, it appears two lines before the exercise. :-) $\endgroup$ – Asaf Karagila Dec 4 '12 at 11:32

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.