Gödel number

For numberings of the set of computable functions, see Numbering (computability theory).

In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number called its Gödel number. The concept was first used by Kurt Gödel for the proof of his incompleteness theorem.

A Gödel numbering can be interpreted as an encoding in which a number is assigned to each symbol of a mathematical notation, after which a sequence of natural numbers can then represent a sequence of strings. These sequences of natural numbers can again be represented by single natural numbers, facilitating their manipulation in formal theories of arithmetic.

In the time since Gödel's paper was published in 1931, the term Gödel numbering has come to be used for a variety of more general assignments of mathematical objects to natural numbers.

Gödel's encoding

Gödel used a system of Gödel numbering based on prime factorization. He first assigned a unique natural number to each basic symbol in the formal language of arithmetic he was dealing with.

In order to encode an entire formula, which is a sequence of symbols, Gödel used the following system. Given a sequence Failed to parse (Missing texvc executable; please see math/README to configure.): x_1 x_2 x_3 ... x_n

of positive integers, the Gödel encoding of the sequence is the product of the first n primes raised to their corresponding values in the sequence:

Failed to parse (Missing texvc executable; please see math/README to configure.): \mathrm{enc}(x_1 x_2 x_3 ... x_n) = 2^{x_1}\cdot 3^{x_2}\cdot 5^{x_3}\cdot ...\cdot {p_n}^{x_n}.

According to the fundamental theorem of arithmetic, any number obtained this way can be uniquely factored into prime factors, so it is possible to effectively recover the original sequence from its Gödel number.

Gödel specifically used this scheme at two levels: first, to encode sequences of symbols representing formulas, and second, to encode sequences of formulas representing proofs. This allowed him to show a correspondence between statements about natural numbers and statements about the provability of theorems about natural numbers, the key observation of the proof.

There are more sophisticated (but more “concise”) ways to construct a Gödel numbering for sequences.

Lack of uniqueness

A Gödel numbering is not unique, in that for any proof using Gödel numbers, there are many ways in which these numbers could be defined.

Suppose there are K basic symbols. An alternative Gödel numbering could be constructed by mapping each of the basic symbols (through, say, a mapping h) to a digit of a bijective base-K numeral system, so a formula consisting of a string of n symbols Failed to parse (Missing texvc executable; please see math/README to configure.): s_1 s_2 s_3 \dots s_n

would be mapped to the number

Failed to parse (Missing texvc executable; please see math/README to configure.): h(s_1) \times K^{(n-1)} + h(s_2) \times K^{(n-2)} + \cdots + h(s_{n-1}) \times K^1 + h(s_n) \times K^0.

Application to formal arithmetic

Once a Gödel numbering for a formal theory is established, each inference rule of the theory can be expressed as a function on the 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.

Failed to parse (Missing texvc executable; please see math/README to configure.): A, B \vdash_r C, \

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

Failed to parse (Missing texvc executable; please see math/README to configure.): g_r(f(A),f(B)) = f(C). \

This is true for the numbering Gödel used, and for any other numbering where the encoded formula can be arithmetically recovered from its Gödel number.

Thus, in a formal theory such as Peano arithmetic in which one can make statements about numbers and their arithmetical relationships to each other, one can use a Gödel numbering to indirectly make statements about the theory itself. This technique allowed Gödel to prove results about the consistency and completeness properties of formal systems.

Generalizations

In computability theory, the term "Gödel numbering" is used in settings more general than the one described above. It can refer to:

1. Any assignment of the elements of a formal language to natural numbers in such a way that the numbers can be manipulated by an algorithm to simulate manipulation of elements of the formal language.
2. More generally, an assignment of elements from a countable mathematical object, such as a countable group, to natural numbers to allow algorithmic manipulation of the mathematical object.

Also, the term Gödel numbering is sometimes used when the assigned "numbers" are actually strings, which is necessary when considering models of computation such as Turing machines that manipulate strings rather than numbers.

See also

• Church numeral
• Description number
• Gödel's incompleteness theorems

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.

Further reading

• Gödel, Escher, Bach: an Eternal Golden Braid, by Douglas Hofstadter. This book defines and uses an alternative Gödel numbering.
• Gödel's Proof by Ernest Nagel and James R. Newman. This book provides a good introduction and summary of the proof, with a large section dedicated to Gödel's numbering.ca:Nombre de Gödel

de:Gödelnummer es:Numeración de Gödel it:Numero di Gödel ja:ゲーデル数 simple:Gödel number sl:Gödlovo število zh-yue:Gödel號數