Gödel number (Gödel numbering)

Typical constructions

There is no single canonical Gödel numbering; many encodings satisfy the basic requirements. A common and historically important method encodes finite sequences of symbols as unique integers by using prime factorization: assign each basic symbol a distinct positive integer code and map a finite sequence s1,...,sn to the product 2^{c(s1)}·3^{c(s2)}·5^{c(s3)}·... . Because prime factorization is unique, each sequence corresponds to exactly one natural number and decodes uniquely. Other methods use positional numeral systems, pairing functions, or effective bijections between strings and numbers.

• Symbol-to-code assignment: give each primitive symbol a distinct small code.
• Sequence encoding: combine symbol codes into one number using primes or base representations.
• Decoding: use unique factorization or computable algorithms to recover the original sequence.

History and origin

The notion of assigning numbers to formulas was made prominent by Kurt Gödel in his proof of the incompleteness theorem, where he used such encodings to construct a formula that, informally, asserts its own unprovability. For context see materials on Kurt Gödel and the original metamathematical arguments. Gödel's idea followed earlier attempts to formalize syntax and paved the way for modern recursion theory and the formal study of computation.

Uses and importance

Gödel numbering is central to several areas:

• Incompleteness and self-reference: coding allows a system to express statements about its own sentences and proofs.
• Computability theory: numberings make precise the concept of effective enumerations of syntactic objects and functions; one studies numberings of the set of computable functions and effective operations on indices.
• Proof theory and automated reasoning: syntactic objects are manipulated as numbers in algorithms and meta-theorems.

Properties and formal requirements

Useful Gödel numberings are typically computable and injective; often the mapping and its inverse (decoding) are required to be primitive recursive or at least recursive so that syntactic manipulations correspond to arithmetic operations. Different acceptable numberings are equivalent in the sense that there is a computable bijection translating one encoding into another. Results such as Rogers' equivalence theorem describe conditions under which numberings of function classes are essentially the same in computability-theoretic terms.

Variants, examples, and distinctions

Variants of Gödel numbering include simple symbol-to-digit codings, more compact encodings used in implementations, and abstract indexings of partial computable functions. The term "Gödel number" is sometimes used loosely to mean any effective code of syntactic objects; more precise texts distinguish between a particular Gödel numbering and the general technique of arithmetization. For background on formal languages and symbols consult resources on formal language, the role of the symbol in mathematical notation, and the nature of the mathematical notation being encoded. For technical treatments of functions and encodings see discussions of function theory and the use of natural numbers as carriers of syntax (natural number encodings).

For further reading, introductory logic texts cover Gödel numbering and arithmetization in chapters on incompleteness; advanced texts connect these encodings to enumeration operators, indices, and the study of effective numberings. Useful pointers can be found in standard overviews and online bibliographies (natural number encodings and formal number theory references).

Additional detailed accounts compare Gödel numberings with other coding strategies in computability theory and explore formal results about which classes of numberings preserve properties of interest.