# 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!

-
As a general principle, you should only look at Gödel's original paper if you are interested in the history of the theorem. There are now much clearer expositions of the proof that eliminate extraneous hypotheses, use modern terminology, and bring out the underlying principles more clearly. – Carl Mummert Apr 10 '13 at 17:54

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.

-
Two minor remarks. For projections you should take the formula $x_1=x_1\wedge\ldots\wedge x_n=x_n\wedge y=x_i$, similarly for the zero function the proper formula is $x=x\wedge y=0$. – Mad Hatter Apr 11 '13 at 13:59
@R.G.: since those are logically equivalent to the ones I have (and thus, certainly provably equivalent), it won't make a difference. e.g. for the zero function all that $r$ has to assert is that the output is zero, it does not need to assert anything about the input. There is no requirement that all the variables $x_i$ have to actually appear in the formula; if they do not, substituting into them is a vacuous operation, but everything still works as it should. – Carl Mummert Apr 11 '13 at 14:22
Yes, you are right. I take back my comment. – Mad Hatter Apr 11 '13 at 22:16

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

-