Arithmetization

Arithmetization is the technique, central to Gödel's incompleteness proof, of assigning natural numbers (Gödel numbers) to syntactic objects — symbols, formulas, and proofs — so that arithmetic can make statements about its own syntax. A formula is encoded as a number, a proof as a sequence of numbers, and meta-level statements about provability become first-order arithmetic statements. This enables the construction of a formula that is true if and only if it is not provable — the self-referential core of the incompleteness argument. Arithmetization is a specific instance of a more general technique: representation of one domain inside another. Turing's encoding of Turing machines as integers (allowing a universal Turing machine to simulate any other) uses the same technique, and the halting problem proof uses it in an exactly analogous way. The deep connection between Gödel's incompleteness results and Turing's undecidability results — both being the same phenomenon viewed through different formalisms — is made explicit by the Curry-Howard correspondence and by proof theory, which shows that both results arise from the same diagonal argument applied to different formal systems.