understanding gödel's 1931 paper - the undecidability theorem

Question

I am reading a translation of Gödel's original paper about in completeness theorem and there are a couple things i don't understand.

Here is the document i am using primarily : http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf

In the part "2.6 Undecidability theorem", it is said that (and i have an intuitive feeling) that :

r = subst(q, 19, number(p))

is supposed to mean "x does not prove p(p)" or rather, "p does not prove p(number(p))".

I "feel" the parallel with the so-called class-sign S or $R_q$ in the sketch of the proof in the introduction.

Here is where i get lost. We have :

r = subst(q, 19, number(p))

r = not(proofFor(x, sub(nb(p), 19, nb(nb(p)))))

But since nb(p) is a sequence of "succ" (encoded as '3') with a "0" in the end, there is not '19' to substitute so i end up with r intuitively meaning : "x is not a proof of nb(p)"

r = not(proofFor(x, nb(p))) since sub(nb(p), 19, nb(nb(p))) = nb(p)

and subst(p, 19, number(p)) = forall(17, r) meaning "nb(p) is not provable", where i guess we should have "p(nb(p)) is not provable".

What id i get wrong ?

Thank you.

---

EDIT1 :

Here is the detail of what i come up with that understanding :

q (17,19) = "not(proofFor(x, sub(y, 19, nb(y))))" with x standing for 17 and 19 standing for 19. I understand q is the number of some formula (so called "relation sign")

p (19) = forall(17, q)

p (19) = forall(x, not(proofFor(x, sub(y, 19, nb(y))))) where 'x' and 'y' denote respectively 17 and 19.

r (17) = sub(q, 19, nb(p))

r (17) = not(proofFor(x, sub(nb(p), 19, nb(nb(p)))))

r (17) = not(proofFor(x, nb(p)))

"x does not prove nb(p)" and :

forall(17, r) : "nb(p) is not provable"

Since : number(n) = succ_n(n, seq(1))

And "succ_n" is defined as follows :

succ n(0, x) = x succ n(n + 1, x) = seq(3) ◦ succ n(n, x)

nb(p) is the number of a sequence of '3' and a '1' in the end, there is no '19' to substitute.

---

EDIT 2 :

If r was defined as : r (17) = sub(q, 19, p)

r (17) = not(proofFor(x, sub(p, 19, nb(p))))

forall(17, r) = sub(p, 19, p) forall(x, not(proofFor(not(proofFor(x, sub(p, 19, nb(p))))))

I could see how one would interpret it as p(nb(p)) (or p(p) ?) is not provable, but with the given definition i just don't see how

Answer 1

Revised edition

I'll use the translation in : Jean van Heijenoort, From Frege to Gödel : A Source Book in Mathematical Logic (1967), page 595-on.

---

[page 598] A formula of [the system] PM with exactly one free variable, that variable being of the type of the natural numbers (class of classes), will be called a class sign. [...] Let $\alpha$ be any class sign; by $[\alpha; n]$ we denote the formula that results from the class sign $\alpha$ when the free variable is replaced by the sign denoting the natural number $n$ [i.e. the numeral $S(S(\ldots S(0)))$].

[page 600] By $Subst \ a^v_b$ (where $a$ stands for a formula, $v$ for a variable, and $b$ for a sign of the same type as $v$ [a term]) we understand the formula that results from $a$ if in $a$ we replace $v$, wherever it is free, by $b$.

[page 603] The functions $x + y, x.y$, and $x^y$, as well as the relations $x < y$ and $x = y$, are recursive, as we can readily see. Starting from these notions, we now define a number of functions (relations) 1-45, each of which is defined in terms of preceding ones [...]

1. $x/y \equiv (\exists z)[z < x \land x = y.z]$, $x$ is divisible by $y$.

This function is $/ : \mathbb N \to \mathbb N$, while e.g. $+ : \mathbb N \times \mathbb N \to \mathbb N$.

I.e. they are functions with natural numbers as "inputs" and "output".

[page 604] 13. $Neg(x) \equiv R(5)*E(x)$, $Neg(x)$ is the NEGATION of $x$.

Now we are in the "arithmetized" world of the syntax, but the functions are still numerical ones; thus, we have to read $Neg : \mathbb N \to \mathbb N$ as the function that takes as input the code of a formula $\varphi$ and produces as output the code of the formula $\lnot \varphi$.

I'll stay with the "standard" use of writing $\ulcorner \varphi \urcorner$ for the code of the formula $\varphi$.

17. $Z(n) \equiv n N [R(1)]$, $Z(n)$ is the NUMERAL denoting the number $n$.

Again, a function that for each number $n$ calculates the code of the numeral $S(S(\ldots S(0)))$, due to the fact that $R(1)=2^1$ is the code of the sequence formed by the single symbol "$0$".

[page 605] $Su \ x^n_y$ results from $x$ when we substitute $y$ for the $n$th term of $x$.

[...] $Sb \ x^v_y$ is the notion $Subst \ a^v_y$ defined above.

$Subst$ is a syntactical operation performed on the formula $\varphi(y)$. The function $Sb$ is an arithmetical one, acting on number. Thus $Sb \ \ulcorner \varphi \urcorner ^v_y$ is the code of the formula $\varphi (v/y)$ obtained performing the $Subst$ operation.

[page 606 ] The fact that can be formulated vaguely by saying: every recursive relation is definable in the system $P$ (if the usual meaning is given to the formulas of this system), is expressed in precise language, without reference to any interpretation of the formulas of $P$, by the following theorem:

Theorem V. For every recursive relation $R(x_1, \ldots, x_n)$ there exists an $n$-place RELATION SIGN $r$ (with the FREE VARIABLES $u_1, u_2,\ldots, u_n)$ such that [...].

Thus, $R$ is a $n$-ary relation between numbers and $r$ is a formula of the formal system $P$.

[page 608] We now define the relation

$$Q(x,y) \equiv \lnot x B_k [Sb \ y^{19}_{Z(y)}].$$

$Q(x,y)$ is a binary numerical relation, defined in terms of previously inrtoduced functions and relations.

By Th.V, it is "expressible" in the system $P$ by a binary relation sign $q$, i.e. by a formula $q(x,y)$.

Let $\ulcorner q \urcorner$ be its code; it is the code number of a formula with two free variables, the two first var in the list of the alphabet, coded with $17$ and $19$ respectively.

Then, $\ulcorner p \urcorner = Gen(17,\ulcorner q \urcorner)$ is the code of the "universal closure" $\forall x q(x,y)$ of the formula $q(x,y)$ with respect to $x$, coded with $17$, due to the fact that the function $Gen(x,y)$ [page 604, n°14] calculates the code number of the GENERALIZATION of the formula coded by $y$ with respect to the VARIABLE coded by $x$.

Thus, the formula $p(y)$ has only one free variable.

Finally, we have $\ulcorner r \urcorner = Sb \ \ulcorner q \urcorner^{19}_{Z(\ulcorner p \urcorner)}$ where $r(x)$ is a new formula with one free variable obtained from $q(x,y)$ substituting the numeral $Z(\ulcorner p \urcorner)$ corresponding to the code for the formula $p(y)$ in place of the second free variable of $q(x,y)$.

This process is called diagonalization :

This is the idea of taking a wff $\varphi(y)$, and substituting (the numeral for) its own code number in place of the free variable. Think of a code number as a way of referring to a wff. Then the operation of ‘diagonalization’ allows us to form a wff that as it were indirectly refers to itself (refers to itself via the Gödel coding). We will use this trick [...] to form a Gödel sentence that encodes ‘I am unprovable in $\mathsf{PA}$’.

---

Following your translation, we have a formula $Q(x, y)$ that "means" : "$x$ does not prove the formula obtained from the formula with code $y$ by subst of the numeral $number(y)$ in place of the (only) free var".

Thus, $p = forall(17, q)$ means : "for all $x$, $x$ does not prove the formula obtained from the formula with code $y$ by subst of the numeral $number(y)$ in place of its only free variable", i.e. "the formula $\ldots$ is unprovable".

---

A very good book is :

• Peter Smith, An Introduction to Gödel's Theorems (2nd ed 2012).

See page 137 for some illuminating details :

[The expression] ‘$\ulcorner \varphi \urcorner$’ is shorthand for [the] standard numeral for the g.n. [Gödel number] of $\varphi$.

In other words, inside formal expressions ‘$\ulcorner \varphi \urcorner$’ stands in for the numeral for the number $\ulcorner \varphi \urcorner$.

A simple example to illustrate:

1. ‘$SS0$’ is an expression, the standard numeral for $2$.

2. On our numbering scheme $\ulcorner SS0 \urcorner$, the g.n. of ‘$SS0$’, is $2^{21}.3^{21}.5^{19}$.

3. So, by our further convention, we can also use the expression ‘$\ulcorner SS0 \urcorner$’ inside (a definitional extension of) [the language], as an abbreviation for the standard numeral for that g.n., i.e. as an abbreviation for ‘$SSS \ldots S0$’ with $2^{21}.3^{21}.5^{19}$ occurrences of ‘$S$’ !

---

See also, for useful details : Diagonalization Lemma.