Gödel numbering

Gödel numbering assigns natural numbers to symbols, formulas, proofs, or finite sequences so that syntactic objects can be studied using arithmetic.

Prime factorization: The decomposition of a positive integer into a unique product of prime powers. Gödel’s original scheme stores a sequence by using successive primes as exponents.
Formal language: A set of finite strings formed from a specified alphabet according to explicit rules. Gödel numbering starts with the symbols and strings of a formal language.
Kurt Gödel: An Austrian-born logician and mathematician whose incompleteness theorems transformed mathematical logic. His 1931 proof made systematic use of numerical codes for expressions and proofs.
Proof predicate: An arithmetic relation that holds of codes representing a proof and the formula it proves. Coding lets a theory express arithmetically whether a particular sequence is a valid proof.
Gödel's original numbering: Gödel’s encoding that assigns prime-powered products to finite sequences of symbol numbers. It is a specific implementation of the broader idea named by this page.
Gödel's β-function: A number-theoretic function used to encode and recover finite sequences from pairs of natural numbers. It provides an alternative arithmetic method for representing finite sequences.
First-order logic: A formal system for expressing relations among objects using quantifiers, variables, and predicates. Its formulas and proof rules are among the main objects encoded in mathematical logic.
On Formally Undecidable Propositions: Gödel’s 1931 paper proving that sufficiently expressive, consistent formal systems contain undecidable statements. The paper’s proof uses arithmetized syntax to construct its central self-referential statement.
Gödel sentence: A sentence constructed in a formal theory to assert, in an appropriate coded sense, that it is not provable there. Its construction relies on representing formulas and provability through numbers.
Gödel numbering of Turing machines: An assignment of natural-number descriptions to Turing machines or their finite instruction tables. Machine codings illustrate how the method applies beyond formulas and proofs.

Linked from 24 pages