Definition
Gödel numbering is a scheme that assigns each symbol of a formal system a number, then encodes a string of symbols as a single number via a uniquely decodable function — typically a product of prime powers. If the symbols of TNT are mapped to small numbers (0 → 1, S → 2, = → 3, …) then the string S0=0 becomes the number 2^2 × 3^1 × 5^3 × 7^1 = 2,500,500. From the number you can uniquely recover the original symbol sequence.
The same trick extends to whole proofs: a proof is a list of formulas with rule justifications, encodable as a list of numbers, encodable as a single number. The result is that every statement about formal systems can be translated into a statement about numbers, which arithmetic can express.
Why it matters
How it works
Step 1: enumerate the symbols of the system and assign each a unique positive integer.
Step 2: encode a string s₁ s₂ ... sₖ as 2^{n₁} × 3^{n₂} × 5^{n₃} × ... × pₖ^{nₖ} where pᵢ is the i-th prime and nᵢ is the code of sᵢ. By the fundamental theorem of arithmetic, the prime factorization is unique, so decoding is unambiguous.
Step 3: encode a proof (a list of formulas) by applying the same trick to the list of Gödel numbers of the formulas.
Step 4: define an arithmetic predicate Proof-Pair(m, n) that says "m is the Gödel number of a proof of the formula with Gödel number n." The predicate is constructed by spelling out the conditions on m (every line is an axiom or follows by an inference rule, the last line decodes to the formula with number n). Each condition is a primitive recursive arithmetic check.
Step 5: build the Gödel sentence by self-application. The famous one decodes to "there is no m such that m is a proof of the formula with this very number" — and the number it talks about is its own.