Gödelnumbering

Gödel numbering, also known as the arithmetization of syntax, is a method for encoding symbols, formulas, and sequences of a formal language as natural numbers. In the standard scheme, each basic symbol is assigned a unique natural number. A finite sequence of symbols s1, s2, ..., sn is encoded as a single number, often by using prime exponentiation: G = p1^{code(s1)} p2^{code(s2)} ... pn^{code(sn)}, where p_i is the i-th prime and code(s_i) is the number assigned to the i-th symbol. Variants of the encoding use pairing functions or other computable schemes. The mapping is computable and effectively invertible for finite strings.

This encoding allows syntactic notions such as “is a formula,” “is a proof of φ from axioms,” and “subformula” to be defined as arithmetical predicates on natural numbers. In particular, the set of well-formed formulas, proofs, and derivations can be described by primitive recursive or recursive relations within arithmetic. Consequently, a formal theory that is capable of expressing basic arithmetic can reason about its own syntax and proofs by talking about the Gödel numbers of objects.

The primary purpose of Gödel numbering is to enable self-reference and diagonalization within formal systems. By translating statements about syntax into statements about natural numbers, Gödel established that any sufficiently expressive, effectively axiomatized system cannot prove all true arithmetic statements, given consistency. This underpins Gödel’s incompleteness theorems.

Variants of the encoding exist, but all share the core idea: assign numbers to symbols and use arithmetic to represent strings, formulas, and proofs, thereby bridging logic and number theory.