Proof of Proposition/Theorem V in Gödel's 1931 paper?

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.


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).