Lema diagonal

En lógica matemática , el lema diagonal (también conocido como lema de diagonalización , lema de autorreferencia ^[1] o teorema del punto fijo ) establece la existencia de enunciados autorreferenciales 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— . Los enunciados cuya existencia está asegurada por el lema diagonal pueden entonces, a su vez, usarse para probar resultados limitativos fundamentales como los teoremas de incompletitud de Gödel y el teorema de indefinibilidad de Tarski . ^[2]

Sea el conjunto de los números naturales . Una teoría de primer orden en el lenguaje de la aritmética representa ^[3] la función computable si existe una fórmula "gráfica" en el lenguaje de — es decir, una fórmula tal que para cada${\displaystyle \mathbb {N}}$ ${\estilo de visualización T}$${\displaystyle f:\mathbb {N}\rightarrow\mathbb {N}}$ ${\displaystyle {\mathcal {G}}_{f}(x,y)}$${\estilo de visualización T}$${\displaystyle n\in \mathbb {N}}$

${\displaystyle \vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {G}}_{f}(^{\circ }n ,\,y)]}$.

Aquí está el numeral correspondiente al número natural , que se define como el sucesor del presunto primer numeral en . ${\displaystyle {}^{\circ }n}$${\estilo de visualización n}$${\estilo de visualización n}$${\estilo de visualización 0}$${\estilo de visualización T}$

El lema diagonal también requiere una forma sistemática de asignar a cada fórmula un número natural (también escrito como ) llamado su número de Gödel . Las fórmulas pueden entonces representarse dentro de los numerales correspondientes a sus números de Gödel. Por ejemplo, se representa por${\displaystyle {\mathcal {A}}}$${\displaystyle \#({\mathcal {A}})}$${\displaystyle \#_{\mathcal {A}}}$${\estilo de visualización T}$${\displaystyle {\mathcal {A}}}$${\displaystyle ^{\circ }\#_{\mathcal {A}}}$

El lema diagonal se aplica a teorías capaces de representar todas las funciones recursivas primitivas . Entre estas teorías se encuentran la aritmética de Peano de primer orden y la aritmética de Robinson , más débil , e incluso una teoría mucho más débil conocida como R. Un enunciado común del lema (como se muestra a continuación) supone con mayor fuerza que la teoría puede representar todas las funciones computables , pero todas las teorías mencionadas también tienen esa capacidad.

Intuitivamente, es una oración autorreferencial : dice que tiene la propiedad . La oración también puede verse como un punto fijo de la operación que asigna, a la clase de equivalencia de una oración dada , la clase de equivalencia de la oración (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 ). La oración construida en la prueba no es literalmente la misma que , pero es demostrablemente equivalente a ella en la teoría . ${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {F}}}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {A}})}$${\estilo de visualización T}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$${\estilo de visualización T}$

Sea la función definida por: ${\displaystyle f:\mathbb {N} \a \mathbb {N} }$

${\displaystyle f(\#_{\mathcal {A}})=\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})]}$

para cada fórmula con una sola variable libre en teoría , y en caso contrario. Aquí denota el número de Gödel de la fórmula . La función es computable (lo que en última instancia es una suposición sobre el esquema de numeración de Gödel), por lo que hay una fórmula que representa en . Es decir ${\displaystyle {\mathcal {A}}(x)}$${\estilo de visualización x}$${\estilo de visualización T}$${\displaystyle f(n)=0}$${\displaystyle \#_{\mathcal {A}}=\#({\mathcal {A}}(x))}$${\displaystyle {\mathcal {A}}(x)}$${\estilo de visualización f}$${\displaystyle {\mathcal {G}}_{f}(x,\,y)}$${\estilo de visualización f}$${\estilo de visualización T}$

${\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y) \Leftrightarrow [y={}^{\circ }f(\#_{\mathcal {A}})]\}}$

Es decir

${\displaystyle \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 con una variable libre , defina la fórmula como: ${\displaystyle {\mathcal {F}}(y)}$${\displaystyle y}$${\displaystyle {\mathcal {B}}(z)}$

${\displaystyle {\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]}$

Luego, para todas las fórmulas con una variable libre: ${\displaystyle {\mathcal {A}}(x)}$

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow (\forall y)\{[y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\Rightarrow {\mathcal {F}}(y)\}}$

Es decir

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow {\mathcal {F}}(^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})])}$

Ahora sustituya por , y defina la oración como: ${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {B}}}$${\displaystyle {\mathcal {C}}}$

${\displaystyle {\mathcal {C}}:={\mathcal {B}}(^{\circ }\#_{\mathcal {B}})}$

Luego la línea anterior se puede reescribir como

${\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$

Cuál es el resultado deseado.

(El mismo argumento en términos diferentes se da en [Raatikainen (2015a)].)

El lema se llama "diagonal" porque tiene cierta similitud con el argumento diagonal de Cantor . ^[5] Los términos "lema diagonal" o "punto fijo" no aparecen en el artículo de Kurt Gödel de 1931 ni en el artículo de Alfred Tarski de 1936 .

Rudolf Carnap (1934) fue el primero en demostrar el lema general autorreferencial ^[6], que dice que para cualquier fórmula F en una teoría T que satisface 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 funciones computables 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. Gödel estaba al tanto del trabajo de Carnap en 1937. ^[7]

El lema diagonal está estrechamente relacionado con el teorema de recursión de Kleene en la teoría de computabilidad , y sus respectivas pruebas son similares.

• Autorreferencia indirecta
• Lista de teoremas de punto fijo
• Aritmética recursiva primitiva
• Autorreferencia
• Paradojas autorreferenciales

• George Boolos y Richard Jeffrey , 1989. Computabilidad y lógica , 3.ª ed. Cambridge University Press. ISBN 0-521-38026-X ISBN 0-521-38923-2   
• Rudolf Carnap , 1934. Logische Syntax der Sprache . (Traducción al español: 2003. The Logical Syntax of Language . Open Court Publishing.)
• Haim Gaifman , 2006. 'Nombramiento y diagonalización: de Cantor a Gödel y Kleene'. Logic Journal of the IGPL, 14: 709–728.
• Hinman, Peter, 2005. Fundamentos de lógica matemática . AK Peters. ISBN 1-56881-262-0 
• Mendelson, Elliott , 1997. Introducción a la lógica matemática , 4ª ed. Chapman & Hall.
• Panu Raatikainen, 2015a. El lema de la diagonalización. En Enciclopedia de Filosofía de Stanford , ed. Zalta. Suplemento de Raatikainen (2015b).
• Panu Raatikainen, 2015b. Teoremas de incompletitud de Gödel. En Stanford Encyclopedia of Philosophy , ed. Zalta.
• Raymond Smullyan , 1991. Teoremas de incompletitud de Gödel . Oxford Univ. Press.
• Raymond Smullyan, 1994. Diagonalización y autorreferencia . Oxford Univ. Press.
• Alfred Tarski (1936). "Der Wahrheitsbegriff in den formalisierten Sprachen" (PDF) . Estudios Filosóficos . 1 : 261–405. Archivado desde el original (PDF) el 9 de enero de 2014 . Consultado el 26 de junio de 2013 .
  • Alfred Tarski , tr. J. H. Woodger, 1983. "El concepto de verdad en lenguajes formalizados". Traducción al inglés del artículo de Tarski de 1936. En A. Tarski, ed. J. Corcoran, 1983, Logic, Semantics, Metamathematics , Hackett.