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?

  • 2
    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.)2012-12-04
  • 0
    @ArthurFischer Yes, this is exercise 44 on page 147. That would make sense and solve my problem. Are you sure?2012-12-04
  • 0
    Matt, it appears two lines before the exercise. :-)2012-12-04

1 Answers 1