Question about the incompleteness proof (Theorem V)

Question

Question in short: Where do I find a complete proof of Theorem V from Gödels incompleteness proof? If it does not exists, can someone provide it?

---

Question in detail:

I am trying to understand Gödels incompleteness proof, by reading the following translation here. I was able to follow the proof until the bottom of page 13, where he states Theorem V.

I tried to proof Theorem V for a constant primitive recursive function $\phi(\nu) = c$, then one only has to show that $$ y = \phi(\nu) \Rightarrow \quad \vdash \varphi(\overline{y},\overline{\nu}) $$ $$ y \neq \phi(\nu) \Rightarrow \quad \vdash \neg \varphi(\overline{y},\overline{\nu}) $$ where for $n \in \mathbb{N}$ we define $$\overline{n}= \underbrace{f\cdots f}_{\text{n times}} 0,$$ and $$\varphi(y_1,x_1) := (y_1 = \overline{c}), $$ where '=' is a metasymbol for $$ x_i = y_i :\Leftrightarrow \forall z_{i+1} (z_{i+1}(x_i) \rightarrow z_{i+1}(y_i) $$

I can proof within PA that it holds $$ \vdash \sigma_i = \sigma_i$$ for any variable of typ $i \in \mathbb{N}$. To be more precise, from axiom II it follows $p \Rightarrow p$. Therefore, it holds $$ \begin{align}\vdash & z_{i+1}(\sigma_i) \Rightarrow z_{i+1}(\sigma_i) \\ \vdash& \forall z_{i+1}( z_{i+1}(\sigma_i) \Rightarrow z_{i+1}(\sigma_i)) \end{align}$$ Now, if $y =\phi(\nu) =c$, then $\overline{y}$ and $\overline{c}$ denote the same sign of type one. Therefore, one can prove that $$ \vdash \overline{y} = \overline{c}.$$

However, I already struggle to prove that if $y \neq c$ that then $$\vdash \neg( \overline{y} = \overline{c}).$$

How do I prove that? Does anyone know a source where the complete detailed proof of Theorem V is given?

Also, if I understood it correctly, then the prove for $$ y \neq \phi(\nu) \Rightarrow \quad \vdash \neg \varphi(\overline{y},\overline{\nu}) $$ can only be shown with metamathematic and it does not derive from some formal PA system, right?

Answer 1

For a modern exposition, see Elliott Mendelson, Introduction to mathematical logic (4ed - 1997), Ch.3.2 NUMBER-THEORETIC FUNCTIONS AND RELATIONS :

We say that a number-theoretic relation $R$ of $n$ arguments is expressible in $K$ if and only if there is a wf $\varphi(x_1,\ldots, x_n)$ of $K$ with the free variables $x_1,\ldots, x_n$, such that, for any natural numbers $k_1,\ldots, k_n$, the following hold:

1. If $R(k_1,\ldots, k_n)$ is true, then $\vdash_K \varphi(\overline {k_1},\ldots, \overline {k_n})$.

2. If $R(k_1,\ldots, k_n)$ is false, then $\vdash_K \lnot \varphi(\overline {k_1},\ldots, \overline {k_n})$.

After this definition there is a long list of number-theoretic relations (and functions) which are showed to be representable.

For example, the number-theoretic relation of identity is expressed in $S$ by the wf $x = x$.

In fact, if $k_1 = k_2$, then $\overline {k_1}$ is the same term as $\overline {k_2}$ and so, by Proposition 3.2(a) $\vdash_S \overline {k_1} = \overline {k_2}$.

Moreover, if $k_1 \ne k_2$ then, by Proposition 3.6(a), $\vdash_S \lnot \overline {k_1} = \overline {k_2}$.

Likewise, the relation 'less than' is expressed in $S$ by the wf $x_1 < x_2$. Recall that $x_1 < x_2$ is $(\exists x_3)(x_3 \ne 0 \land x_3 + x_1 = x_2)$. If $k_1 < k_2$, then there is some non-zero number $n$ such that $k_2 = n + k_1$.

All these results are achieved proving that the system $S$ (usual Robinson arithmetic) has "enough expressive capabilities".

See e.g. Mendelson, PROPOSITION 3.6(a) :

Let $m,n$ be any natural numbers.

(i) If $m \ne n$, then $\vdash_S \lnot \overline {m} = \overline {n}$.

(ii) $\vdash_S \overline {m+n} = \overline {m} + \overline {n}$ and $\vdash_S \overline {m \cdot n} = \overline {m} \cdot \overline {n}$.

These results are metamathematical : they show that for every $m,n$ there is a formal derivation in $S$ of the corresponding formula. But their proof is constructive : it shows a formal derivation is $S$ of the required formula.