Proof of Proposition/Theorem V in Gödel's 1931 paper? Proposition V in Gödel's famous 1931 paper is stated as follows:
For every recursive relation $ R(x_{1},...,x_{n})$ there is an n-ary "predicate" $r$ (with "free variables" $u_1,...,u_n$) such that, for all n-tuples of numbers $(x_1,...,x_n)$, we have:
$$R(x_1,...,x_n)\Longrightarrow Bew[Sb(r~_{Z(x_1)}^{u_1}\cdot\cdot\cdot~_{Z(x_n)}^{u_n})] $$
$$\overline{R}(x_1,...x_n)\Longrightarrow Bew[Neg~Sb(r~_{Z(x_1)}^{u_1}\cdot\cdot\cdot~_{Z(x_n)}^{u_n})]$$
Gödel "indicate(s) the outline of the proof" and basically says, in his inductive step, that the construction of $r$ can be formally imitated from the construction of the recursive function defining relation $R$.
I have been trying to demonstrate the above proposition with more rigor, but to no avail. I have, however, consulted "On Undecidable Propositions of Formal Mathematical Systems," the lecture notes taken by Kleene and Rosser from Gödel's 1934 lecture, which have been much more illuminating; but still omits the details in the inductive step from recursive definition, stating "the proof ... is too long to give here."
So can anyone give me helpful hint for the proof of the above proposition, or even better, a source where I can find such a demonstration? Thanks!

I'm not completely familiar with Gödel's notation, but I think this is equivalent to theorem 60 in Chapter 2 of The Logic of Provability by George Boolos, which has fairly detailed proofs of this sort of thing (all in chapter 2).
