Gödel number

Encyclopedia : G : GD : GDE : Gödel number

In formal number theory a Gödel numbering is a function which assigns to each symbol and formula of some formal language a unique natural number called a Gödel number (GN). The concept was first used by Kurt Gödel for the proof of his incompleteness theorem.

A numbering of the set of computable functions is sometimes called Gödel numbering or effective numbering. A Gödel numbering can be interpreted as a programming language with the Gödel numbers assigned to each computable function as the programs which calculate the values for the function in that programming language. Rogers' equivalence theorem characterizes the numberings of the set of computable functions that are Gödel numberings.

Contents

1 Definition
2 Example

2.1 Step 1
2.2 Step 2
2.3 Step 3
2.4 An informal account of the proof

3 Discussion
4 See also
5 References
6 Further reading

Definition

Given a countable set S, a Gödel numbering is a function

[f:S \to \mathbb]

with both f and the inverse of f a computable function.

Example

Step 1

Gödel numbers are constructed with reference to symbols of the propositional calculus and formal arithmetic. Each symbol is first assigned a natural number, thus:

Logical symbols Numbers 1:12

¬ 1 ("not")

[\forall] 2 ("for all")

[\supset] 3 ("if,then")

[\vee] 4 ("or")

[\wedge] 5 ("and")

( 6

) 7

S 8 ("is the successor of")

0 9

= 10

. 11

+ 12
Propositional symbols Numbers greater than 10 but divisible by 3

P 12

Q 15

R 18

S 21

Individual variables numbers greater than 10 with remainder 1 when divided by 3

v 13

x 16

y 19

Predicate symbols numbers greater than 10 with remainder 2 when divided by 3

E 14

F 17

G 20

And so on and so forth (NB the syntax of the propositional calculus ensures that there is no ambiguity between "P" and "+", even though both are assigned the number 12).

Logical symbols	Numbers 1:12
¬	1 ("not")
[\forall]	2 ("for all")
[\supset]	3 ("if,then")
[\vee]	4 ("or")
[\wedge]	5 ("and")
(	6
)	7
S	8 ("is the successor of")
0	9
=	10
.	11
+	12
Propositional symbols	Numbers greater than 10 but divisible by 3
P	12
Q	15
R	18
S	21
Individual variables	numbers greater than 10 with remainder 1 when divided by 3
v	13
x	16
y	19
Predicate symbols	numbers greater than 10 with remainder 2 when divided by 3
E	14
F	17
G	20

Step 2

Arithmetical statements are assigned unique Gödel numbers referenced to the series of prime numbers. This is based on a simple code which essentially reads
prime 1 ^{character 1} × prime 2 ^{character 2} × prime 3 ^{character 3}
and so on. For example the statement
[\forall]x, P(x) becomes
2² × 3¹⁶ × 5¹² × 7⁶ × 11¹⁶ × 13⁷, because
is the prime series, and 2, 16, 12, 6, 16, 7 are the relevant character codes. This is a large but perfectly determinate number (namely 14259844433335185664666562849653536301757812500).

It is also important to note, by the fundamental theorem of arithmetic, this astronomical number can be decomposed into unique prime factors; thus it is possible to convert the Gödel number back to its sequence of characters.

Step 3

Finally, sequences of arithmetical statements are assigned further Gödel numbers, such that the sequence
Statement 1 (GN1)
Statement 2 (GN2)
Statement 3 (GN3)
(where GN denotes a Gödel number)
gets the Gödel number 2^GN1×3^GN2×5^GN3, which we will call GN4. The proof of Gödel's incompleteness theorem depends on the demonstration that, in formal arithmetic, some sets of statements logically entail or prove other statements. For example it might be shown that GN1, GN2, and GN3 together, i.e. GN4, prove GN5. Because this is a demonstrable relationship between numbers it is entitled to its own symbol, for example R. Then we could write R(v,x) to express "x proves v". In the case where x and v are Gödel numbers GN4 and GN5 we would say R(GN5,GN4).

An informal account of the proof

The core of Gödel's argument is that we can write the statement

[\forall]x, ¬R(v,x)

which means

no proposition of type v can be proved.

The Gödel number for this statement would be

2² × 3¹⁶ × 5¹ × 7¹⁸ × 11⁶ × 13¹³ × 17¹⁶ × 19⁷

but we will call it GN6. Now if we consider the statement

[\forall]x, ¬R(GN6,x),

we will realise that it says

no proposition that says 'no proposition of type v can be proved' can be proved.

This collapses into the statement

this proposition cannot be proved.

If the statement can actually be proved, then its formal system is inconsistent because it proves something which states that it itself cannot be proven (a contradiction). If the statement cannot be proved within its formal system, then what the statement asserts is actually true, so the statement is consistent, but since the formal system contains a statement which is semantically true but which cannot be proven (syntactically), then the system is incomplete. Therefore, assuming that the formal system is consistent, it has to be incomplete.

Discussion

The Gödel numbering is not unique. The general idea is to map formulas onto natural numbers. An alternative Gödel numbering could be to consider each of the symbols of Step 1 to be mapped (through, say, a mapping h) to a digit of a base-22 numeral system, so a formula consisting of a string of n symbols [ s_1 s_2 s_3 \dots s_n] would be mapped to the number

[ h(s_1) \times 22^ + h(s_2) \times 22^ + \cdots + h(s_) \times 22^1 + h(s_n) \times 22^0. ]

Also, Gödel numbering implies that each inference rule of the formal system can be expressed as a function of natural numbers. If f is the Gödel mapping and if formula C can be derived from formulas A and B through an inference rule r, i.e.

[ A, B \vdash_r C, \ ]

then there should be some arithmetical function g_r of natural numbers such that

[ g_r(f(A),f(B)) = f(C). \ ]

Then, since the formal system is a formal arithmetic, which can make statements about numbers and their arithmetical relationships to each other, it follows that the system can also, by means of Gödel coding, indirectly make statements about itself: that is, a proposition of the formal system can make assertions which, when viewed through the perspective of the Gödel mapping, translate into assertions about other propositions of the same formal system, or even about itself. Thus, by this means a formal arithmetic can make assertions about itself, becoming self-referential, almost like a second-order logic. This provided Gödel (and other logicians) with a means of exploring and discovering proofs about consistency and completeness properties of formal systems.

References

Gödel, Kurt, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatsheft für Math. und Physik 38, 1931, S.173-198.