gdel number

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

Definition

Given a countable set S, a Gdel numbering is a function

f:S \to \mathbb{N}

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

Example

Step 1

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

Step 2

Arithmetical statements are assigned unique Gdel 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
{2, 3, 5, 7, 11, ...} 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).

Step 3

Finally, sequences of arithmetical statements are assigned further Gdel numbers, such that the sequence
Statement 1 (GN1)
Statement 2 (GN2)
Statement 3 (GN3)
gets the Gdel number 2^GN1*3^GN2*5^GN3, which we will call GN4. The proof of Gdel'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. R(v,x) would then mean "x proves v". In the case where x and v are Gdel numbers GN5 and GN4 we would say
R(GN5,GN4).

An informal account of the proof

The core of Gdel'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 Gdel 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 ... s_n

would be mapped to the number

h(s_1) \times 22^{(n-1)} + h(s_2) \times 22^{(n-2)} + ... + h(s_{n-1}) \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. See also: Church number.

Gdel Number