Gödel number

Poll without page-refresh

Article on other languages:

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.

1 Gödel's encoding
2 Lack of uniqueness
3 Application to formal arithmetic
4 Generalizations
5 See also
6 References
7 Further reading

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 $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:

$\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 (for any given number n of symbols to be encoded).

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 $s_1 s_2 s_3 \dots s_n$ would be mapped to the number

$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.

$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). \$

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:

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.
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.

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.

Gödel number

Contents

Gödel's encoding

Lack of uniqueness

Application to formal arithmetic

Generalizations

See also

References

Further reading