In formal number theory a Gödel numbering is a function which assigns to each symbol and formula of some formal language a unique natural number called a Gödel number (GN). The concept was first used by Kurt Gödel for the proof of his incompleteness theorem.

A Gödel numbering can be interpreted as an encoding where a number is assigned to each symbol of a mathematical notation, and a stream of natural numbers can then represent some form or function. A numbering of the set of computable functions can then be represented by a stream of Gödel numbers (also called effective numbers). Rogers' equivalence theorem states criteria for which those numberings of the set of computable functions are Gödel numberings.

Given a countable set S, a Gödel numbering is an injective function

${\displaystyle f:S\to \mathbb {N} }$

with both f and ${\displaystyle f^{-1}}$ (the inverse of f) being computable functions.

One of the simplest Gödel numbering schemes is used every day: The correspondence between integers and their representations as strings of symbols. For example, the sequence 2 3 is understood, by a particular set of rules, to correspond to the number twenty-three. Similarly, strings of symbols from some alphabet of N symbols can be encoded by identifying each symbol with a number from 0 to N and reading the string as the base N+1 representation of an integer.

• Gödel, Kurt, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatsheft für Math. und Physik 38, 1931, pages 173–198.

• Gödel, Escher, Bach: an Eternal Golden Braid, by Douglas Hofstadter. This book defines and uses an alternative Gödel numbering.
• Gödel's Proof by Ernest Nagel and James R. Newman. This book provides a good introduction and summary of the proof, with a large section dedicated to Gödel's numbering.