La numeración de Gödel es una función que asigna a cada símbolo y fórmula de un lenguaje formal un número único, denominado Número de Gödel (GN). El concepto fue utilizado por primera vez por Kurt Gödel para la demostración del teorema de Incompletitud de Gödel.

La enumeración de un conjunto de funciones computables se denomina también enumeración de Gödel o enumeración efectiva. Una enumeración de Gödel se puede interpretar como un lenguaje de programación donde los números de Gödel están asignados a cada función computable igual que los programas de cálculos a los valores para la función en este lenguaje de programación.

Dado un conjunto enumerable S, una enumeración de Gödel es una función

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

donde f y la inversa de f son funciones computables.

Los números de Gödel se construyen con referencia a símbolos de cálculo proposicional y la aritmética formal. Cada símbolo se asigna primero a un número natural, por tanto:

.

Símbolos lógicos	Números 1:12
¬	1 ("no")
${\displaystyle \forall }$	2 ("para todos")
${\displaystyle \rightarrow }$	3 ("si, entonces")
${\displaystyle \vee }$	4 ("o")
${\displaystyle \wedge }$	5 ("y")
(	6
)	7
S	8 ("es el sucesor de")
0	9
=	10
.	11
+	12
Símbolos proposicionales	Números más grandes que 12 y divisibles por 3
P	12
Q	15
R	18
S	21
Variables individuales	Números más grandes que 12 con resto 1 cuando se dividen por 3
v	13
x	16
y	19
Símbolos de predicado	Números más grandes que 12 con resto 2 cuando se dividen por 3
E	14
F	17
G	20

Y así para todos los símbolos posibles. La sintaxis del cálculo proposicional asegura que no hay ambigüedad entre el símbolo "P" y el símbolo "+" aunque ambos estén asignados al número 12.

A cada enunciado aritmético se le asigna un número de Gödel único utilizando series de números primos. Se basa básicamente en el siguiente código: 1.er primo ^carácter × 2º primo ^carácter × 3.er primo ^carácter etc.
Por ejemplo el enunciado ${\displaystyle \forall }$x, P (x) se convierte en
2² × 3¹⁶ × 5¹² × 7⁶ × 11¹⁶ × 13⁷, porque {2, 3, 5, 7, 11,...} es la serie de primos, y 2, 16, 12, 6, 16, 7 son los códigos de los caracteres. Este es un número bastante grande, pero perfectamente determinado: 14259844433335185664666562849653536301757812500.

Es importante ver que, por el teorema fundamental de la aritmética, este número tan grande se puede descomponer en sus factores primos, y por tanto se puede convertir un número de Gödel en la secuencia de caracteres original.

Finalmente, a las secuencias de enunciados se les asigna un número de Gödel, de manera que la secuencia
Enunciado 1 (GN1)
Enunciado 2 (GN2)
Enunciado 3 (GN3)
(donde GN significa número de Gödel)

tiene el número de Gödel 2^GN1×3^GN2×5^GN3, que denominaremos GN4.

La demostración del teorema de incompletitud de Gödel se basa en la demostración de que, en aritmética formal, algunos conjuntos de enunciados prueban otros enunciados de forma lógica. Por ejemplo, se puede probar que la unión de GN1, GN2 y GN3 (es decir GN4) prueban GN5. Como esta es una relación demostrable entre dos números, se le asigna su propio símbolo, por ejemplo R. Entonces se puede escribir R (v, x) para expresar que x demuestra v. En el caso anterior donde x y v son los números de Gödel GN4 y GN5, se podría escribir R(GN5, GN4).

El argumento central de la demostración hecha por Gödel se basa en que puede escribirse

${\displaystyle \forall }$x, ¬R (v, x)

que quiere decir

ninguna sentencia de tipo v se puede probar.

El número de Gödel para esta sentencia sería

2² × 3¹⁶ × 5¹ × 7¹⁸ × 11⁶ × 13¹³ × 17¹⁶ × 19⁷

que se puede denominar GN6. Ahora, si se considera la sentencia

${\displaystyle \forall }$x, ¬R(GN6,x),

que de hecho está diciendo

ninguna sentencia que afirme 'ninguna sentencia de tipo v se puede probar' puede probarse.

Que equivale a

esta sentencia no se puede probar.

Si esta última sentencia se puede probar, entonces su sistema formal es inconsistente porque demuestra una sentencia que ella misma afirma que no se puede demostrar (contradicción). Si la sentencia no se puede probar dentro del sistema formal, entonces lo que afirma la sentencia es cierto, y por tanto la sentencia es consistente, pero como el sistema contiene una afirmación que es semánticamente cierta pero que no se puede probar (sintácticamente), entonces el sistema es incompleto.

• Codificación de Church

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