Kurt Gödel developed the concept for the proof of his incompleteness theorems.
These sequences of natural numbers can again be represented by single natural numbers, facilitating their manipulation in formal theories of arithmetic.
In simple terms, Gödel devised a method by which every formula or statement that can be formulated in the system gets a unique number, in such a way that formulas and Gödel numbers can be mechanically converted back and forth.
A simple example is the way in which English is stored as a sequence of numbers in computers using ASCII.
Since ASCII codes are in the range 0 to 127, it is sufficient to pad them to 3 decimal digits and then to concatenate them: Gödel used a system based on prime factorization.
He first assigned a unique natural number to each basic symbol in the formal language of arithmetic with which he was dealing.
To encode an entire formula, which is a sequence of symbols, Gödel used the following system.
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: According to the fundamental theorem of arithmetic, any number (and, in particular, a number obtained in this way) can be uniquely factored into prime factors, so it is possible to 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 proof's key observation (Gödel 1931).
There are more sophisticated (and more concise) ways to construct a Gödel numbering for sequences.
For example, supposing there are K basic symbols, an alternative Gödel numbering could be constructed by invertibly mapping this set of symbols (through, say, an invertible function h) to the set of digits of a bijective base-K numeral system.
would then be mapped to the number In other words, by placing the set of K basic symbols in some fixed order, such that the
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.
In computability theory, the term "Gödel numbering" is used in settings more general than the one described above.
In simple cases when one uses a hereditarily finite set to encode formulas this is essentially equivalent to the use of Gödel numbers, but somewhat easier to define because the tree structure of formulas can be modeled by the tree structure of sets.
Gödel sets can also be used to encode formulas in infinitary languages.