# Lema diagonal

En lógica matemática, el lema diagonal (también conocido como lema de diagonalización, lema de autorreferencia o teorema del punto fijo) establece la existencia de sentencias autorreferenciadas en ciertas teorías formales de los números naturales, específicamente aquellas teorías que son lo suficientemente fuertes como para representar todas las funciones computables. Las oraciones cuya existencia está asegurada por el lema diagonal pueden, a su vez, usarse para probar resultados limitativos fundamentales como los teoremas de incompletitud de Gödel y el teorema de indefinibilidad de Tarski.

## Antecedentes

Sea $\mathbb {N}$ el conjunto de los números naturales. Una teoría de primer orden $T$ en el lenguaje de la aritmética representa la función computable $f:\mathbb {N} \rightarrow \mathbb {N}$ si existe una fórmula expresable como un "grafo" ${\mathcal {G}}_{f}(x,y)$ en el lenguaje de $T$ tal que para cada $n\in \mathbb {N}$
    $\vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {G}}_{f}(^{\circ }n,\,y)]$
Aquí, $^{\circ }n$ es el numeral correspondiente al número natural $n$, que se define como el $n$º sucesor del presunto primer numeral $0$ en $T$.
El lema diagonal también requiere una forma sistemática de asignar a cada fórmula ${\mathcal {A}}$ un número natural $\#({\mathcal {A}})$ (también escrito como $\#_{\mathcal {A}}$) llamado su número de Gödel. Entonces, las fórmulas se pueden representar dentro de $T$ mediante los números correspondientes a sus números de Gödel. Por ejemplo, ${\mathcal {A}}$ está representada por $^{\circ }\#_{\mathcal {A}}$
El lema diagonal se aplica a teorías capaces de representar todas las funciones primitivas recursivas. Tales teorías incluyen la aritmética de Peano de primer orden y la más débil aritmética de Robinson, e incluso una teoría mucho más débil conocida como R. Una declaración común del lema (como se indica a continuación) supone más firmemente que la teoría puede representar todas las funciones computables, pero todas las teorías mencionadas también tienen esta capacidad.

## Enunciado del lema

* Sea $T$ una teoría de primer orden en el lenguaje de la aritmética capaz de representar todas las funciones computables, y sea ${\mathcal {F}}(y)$ una fórmula en $T$ con una variable libre. Entonces, existe una sentencia ${\mathcal {C}}$ tal que
* $\vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})$
Intuitivamente, ${\mathcal {C}}$ es una oración autorreferenciada: ${\mathcal {C}}$ afirma que ${\mathcal {C}}$ tiene la propiedad ${\mathcal {F}}$. La oración ${\mathcal {C}}$ también puede verse como un punto fijo de la operación que asigna, a la clase de equivalencia de una oración determinada ${\mathcal {A}}$, la clase de equivalencia de la oración ${\mathcal {F}}(^{\circ }\#_{\mathcal {A}})$ (la clase de equivalencia de una oración es el conjunto de todas las oraciones a las que es demostrablemente equivalente en la teoría $T$). La oración ${\mathcal {C}}$ construida en la demostración no es literalmente la misma que $F(^{\circ }\#_{\mathcal {C}})$, pero es demostrablemente equivalente a ella en la teoría $T$.

## Demostración

Sea $f:\mathbb {N} \to \mathbb {N}$ la función definida por:
    $f(\#_{\mathcal {A}})=\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})]$
para cada fórmula ${\mathcal {A}}(x)$ con una sola variable libre $x$ en la teoría $T$, y $f(n)=0$ en caso contrario. Aquí, $\#_{\mathcal {A}}=\#({\mathcal {A}}(x))$ denota el número de Gödel de la fórmula ${\mathcal {A}}(x)$. La función $f$ es computable (lo que en última instancia es una suposición sobre el esquema de numeración de Gödel), por lo que existe una fórmula ${\mathcal {G}}_{f}(x,\,y)$ que representa $f$ en $T$. Nominalmente
    $\vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y=^{\circ }f(\#_{\mathcal {A}})]\}$
lo que equivale a decir que
    $\vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y=^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\}$
Ahora, dada una fórmula arbitraria ${\mathcal {F}}(y)$ con una variable libre $y$, se define la fórmula ${\mathcal {B}}(z)$ como:
    ${\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]$
Entonces, para todas las fórmulas ${\mathcal {A}}(x)$ con una variable libre:
    $\vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow (\forall y)\{[y=^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\Rightarrow {\mathcal {F}}(y)\}$
lo que equivale a decir que
    $\vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow {\mathcal {F}}(^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})])$
Ahora, se sustituye ${\mathcal {A}}$ por ${\mathcal {B}}$ y se define la oración ${\mathcal {C}}$ como:
    ${\mathcal {C}}:={\mathcal {B}}(^{\circ }\#_{\mathcal {B}})$
Entonces la línea anterior se puede reescribir como
    $\vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})$
que es el resultado buscado.
(El mismo argumento en términos diferentes se presenta en [Raatikainen (2015a)].)

## Historia

El lema se llama "diagonal" porque tiene cierto parecido con el argumento de la diagonal de Cantor. Los términos "lema diagonal" o "punto fijo" no aparecen en el artículo de 1931 de Kurt Gödel ni en el artículo de 1936 publicado por Alfred Tarski.
Rudolf Carnap (1934) fue el primero en demostrar el lema autorreferencial general, que dice que para cualquier fórmula F en una teoría T que satisfaga ciertas condiciones, existe una fórmula ψ tal que ψ ↔ F(°#(ψ)) es demostrable en T. El trabajo de Carnap fue redactado en un lenguaje alternativo, ya que el concepto de función computable aún no se había desarrollado en 1934. Mendelson (1997, p. 204) cree que Carnap fue el primero en afirmar que algo así como el lema diagonal estaba implícito en el razonamiento de Gödel, quien conocía el trabajo de Carnap en 1937.
El lema diagonal está estrechamente relacionado con el teorema de recursión de Kleene en la teoría de la computabilidad, y sus respectivas demostraciones son similares.