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!
 A: Remember that what Gödel called "recursive" is what we now call primitive recursive; the term "recursive" is now used to mean computable instead. Also the "predicate" $r$ is now called a formula. 
The general idea at hand here is called "representability of functions". We are proving is that every primitive recursive function is representable in a particular way in our fixed, sufficiently strong theory of arithmetic.  This sort of thing is covered in great detail in chapters 12 and 13 of Peter Smith's book An Introduction to Gödel's Theorems which at the moment is probably the best rigorous reference in print at the undergraduate level. 
One method of proof is by induction on the definition of the primitive recursive function $R$. Here is a sketch of how to define the formula $r$:


*

*For the successor function $R(x) = x+1$ let $r(x,y)$ be $y = x+1$

*For the projection function $R(x_1,\ldots, x_n) = x_i$ let $r(x_1, \ldots, x_n, y)$ be $y = x_i$

*For the zero function $R(x) = 0$ let $r(x,y)$ be $y = 0$

*If $R$ is a composition $f(g_1(x_1, \ldots, x_n), \ldots, g_k(x_1, \ldots, x_n))$, let $r_f$ and $r_{g_i}$, $i \leq k$, be obtained by induction. Then let $r(x_1,\ldots,x_n, y)$ be $$(\exists y_1, \ldots, y_k)[ r_f(y_1, \ldots, y_k, y) \land r_{g_1}(x_1,\ldots,x_n,y_1) \land \cdots \land r_{g_k}(x_1,\ldots,x_n,y_k)]$$

*If $R$ is defined by primitive recursion as
$$R(0, x_1, \ldots, x_n) = f(x_1, \ldots, x_n)$$
$$R(k+1, x_1, \ldots , x_n) = g(k, x_1, \ldots, x_n, R(k, x_1, \ldots, x_n))$$
then let $r_f$ and $r_g$ be obtained by induction and let
$$
r(z, x_1, \ldots, x_n, y) = (\exists \sigma)[|\sigma| = z+1 \land r_f(x_1,\ldots,x_n,\sigma(0)) \land (\forall i < z)[r_g(i, x_1, \ldots, x_n, \sigma(i+1)) \land y = \sigma(z)]$$
The quantification over a finite sequence $\sigma$ can be turned into quantification over natural numbers using the technique of Gödel's β function.
You can then prove by induction that for each primitive recursive $R$, for each $x_1,\ldots, x_n$ there is a unique $y$ such that $r(\overline{x_1}, \ldots, \overline{x_n},\overline{y})$ is provable. 
A: 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).
