understanding gödel's 1931 paper - gödel numbers

Question

I am a little confused about gödel numbers and what numbers exactly we are manipulating.

are the numbers "real" natural numbers (than we obviously represent as) 1, 2, ... or are we always dealing with numbers in the "format" "succ( ... succ(0) ... )" ?

Like are we manipulating genuine natural numbers or their representation in the system at hand ?

I don't have a mathematical background, i'm just a curious guy so it may be a silly question, i feel like their is a difference between "real" numbers, whatever they may be, and their representation, and i'm getting confused about what is manipulated, using what system, etc.

I heard about models and stuff but i may be mixing up everything.

for example, for the 45-th primitive recursive function : "provable(x)", or " "Bew(x)", is x a real natural number of a number in the "format" "succ( ... succ(0) ... )" ?

"R(x) ≡ 2x" and "(n+1) N x" makes me believe we are using natural numbers "outside" of the system introduced by Gödel, but we could be working with numbers encoded in the system : "succ( ... (succ(0) ... )". i feel like for some reason we shouldn't work outside of the system.

Am i wrong ? Does that make any difference ?

Answer 1

(Collecting my comments into one answer.)

You're right to sweat the details on this: The entire proof is about the boundary between what can be said in a formal system, what can be proved in it, and the outside world (of abstract entities) which it attempts to characterize. So it's essential to maintain clarity about these things, and draw a sharp distinction between strings in the formal system and what they denote or evaluate to.

Within the formal system, the things that get substituted into a formula such as $Bew(w)$ are numerals, and not integers (actual numbers). They're representations of integers within the formal system, terms/expressions which denote integers. A Godel numbering is a particular way of assigning numbers to terms and formulas of a particular formal system, provided the system contains enough arithmetic to make that possible. The integer assigned to a formula is its Godel number. See the answer by @Mauro ALLEGRANZA for a little more detail, and in particular the link he provides re arithmetization of syntax, the key notion.

Finally, a note on terminology: "integers" rather than "real numbers". In math "the real numbers" denotes that set of numbers, $\mathbb{R}$, generally taken together with additional structure (addition, multiplication, and the usual "<" relation). The real numbers include the integers, all rationals such as $\frac 2 3, \frac {513} {153}, - \frac 5 7$ etc., as well as irrationals like $\pi$.

Answer 2

The basic intuition behind Gödel's proof is the arithmetization of syntax.

The language is made of symbols : $\lnot, \lor, \forall, 0, f, \ldots$.

The language is the first-order language of arithmetic. Thus, a term (e.g. $f(0)$) in the language is a "name" denoting a number (the number $1$) and a sentence (a closed formula, like : $\lnot (fx_1 = 0)$ ) express an arithmetical fact (the fact that $0$ has no predecessor).

The "trick" of encoding allows us to use arithmetical relations as a way to express relations between "syntactical" objects, like the provability predicate $Bew(x)$.

Gödel numbers are natural numbers : in your previous post we have seen how to "compute" them.

The provability predicate $Bew(n)$ holds iff $n$ is the code of a formula $\varphi$ that is provable in the formal system $\mathsf P$, i.e. with $n= \ulcorner \varphi \urcorner$ :

$Bew(\ulcorner \varphi \urcorner)$ iff $\mathsf P \vdash \varphi$.

Thus $Bew(x)$ is like any other predicate of natural numbers; like e.g. $Even(x)$, where $Even(n)$ holds iff $n$ is even.

By f-o language of arithmetic we can express the predicate $Even(x)$ as follows : $\exists k \ (n=f(f(0)) \times k)$.

In the same way, Gödel's proof shows how to "build" a formula (a very complicated one indeed) able to express "inside" the system $\mathsf P$ the arithmetical facts encoding the "syntactical" facts regarding $\mathsf P$ itself, like the fact that a specific formula is an axiom of the system or the fact that a certain sequence of formulae is a proof in the system.

This "double play" is cleraly sated by Gödel at the ouset of his paper :

The formulas of a formal system in outward appearance are finite sequences of primitive signs (variables, logical constants, and parentheses or punctuation dots), and it is easy to state with complete precision which sequences of primitive signs are meaningful formulas and which are not. Similarly, proofs, from a formal point of view, are nothing but finite sequences of formulas (with certain specifiable properties.) Of course, for metamathematical considerations it does not matter what objects are chosen as primitive signs, and we shall assign natural numbers to this use. Consequently, a formula win be a finite sequence of natural numbers, and a proof array a finite sequence of finite sequences of natural numbers. The metamathematical notions (propositions) thus become notions (propositions) about natural numbers or sequences of them; therefore they can (at least in part) be expressed by the symbols of the system itself. In particular, it can be shown that the notions "formula", "proof array", and "provable formula" can be defined in the system; that is, we can, for example, find a formula $F(v)$ with one free variable $v$ such that $F(v)$, interpreted according to the meaning of the terms of [the system], says: $v$ is a provable formula. We now construct an undecidable proposition of the system, that is, a proposition $A$ for which neither $A$ nor not-$A$ is provable. [...]

From the remark that $[R(q); q]$ says about itself that it is not provable it follows at once that $[R(q) ; q]$ is true, for $[R(q) ; q]$ is indeed unprovable (being undecidable). Thus, the proposition that is undecidable in the system still was decided by metamathematical considerations.

---

For a "classical" textbook with all the details of Gödel's proof (very much in the same "style" of Gödel's original paper), see :

• Elliott Mendelson, Introduction to mathematical logic (4th ed - 1997), page 190-on.

For a complete introduction to this topic, see :

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

For a divulgative books (without errors) see :

• Torkel Franzén, Gödel's theorem : An incomplete guide to its use and abuse (2005)

and :

• Francesco Berto, There's Something about Gödel : The Complete Guide to the Incompleteness Theorem (2009).