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 oraciones autorreferenciales en ciertas teorías formales de los números naturales, específicamente aquellas teorías que son lo suficientemente fuertes 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 . [2]
Fondo
Dejar ser el conjunto de números naturales . Una teoría T representa la función computable si existe un predicado "gráfico" en el lenguaje de T de tal manera que para cada, T prueba
- . [3]
Aquí es el numeral correspondiente al número natural , que se define como el término cerrado 1+ ··· +1 ( unos), y es el numeral correspondiente a .
El lema diagonal también requiere que haya una forma sistemática de asignar a cada fórmula θ un número natural # ( θ ) llamado su número de Gödel . Las fórmulas se pueden representar dentro de la teoría mediante los números correspondientes a sus números de Gödel. Por ejemplo, θ está representado por ° # ( θ )
El lema diagonal se aplica a las teorías capaces de representar todas las funciones recursivas primitivas . Tales teorías incluyen la aritmética de Peano y la aritmética más débil de Robinson . Un enunciado común del lema (como se indica a continuación) hace la suposición más fuerte de que la teoría puede representar todas las funciones computables .
Declaración del lema
Sea T una teoría de primer orden en el lenguaje de la aritmética y capaz de representar todas las funciones computables . Sea F una fórmula en el lenguaje con una variable libre, entonces:
Lema - Hay una oración tal que es demostrable en T . [4]
Intuitivamente, es una oración autorreferencial que dice quetiene la propiedad F . La frasetambién se puede ver como un punto fijo de la operación que asigna a cada fórmula la frase . La frase construido en la prueba no es literalmente lo mismo que , Pero es demostrable equivalente a que en la teoría T .
Prueba
Sea f : N → N la función definida por:
- f (# ( θ )) = # ( θ (° # ( θ )))
para cada fórmula T θ en una variable libre, y f ( n ) = 0 en caso contrario. La función f es computable, así que hay una Γ fórmula f representa f en T . Por lo tanto, para cada fórmula θ , T demuestra
- (∀ y ) [Γ f (° # ( θ ), y ) ↔ y = ° f (# ( θ ))],
que es decir
- (∀ y ) [Γ f (° # ( θ ), y ) ↔ y = ° # ( θ (° # ( θ )))].
Ahora defina la fórmula β ( z ) como:
- β ( z ) = (∀ y ) [Γ f ( z , y ) → F ( y )].
Entonces T prueba
- β (° # ( θ )) ↔ (∀ y ) [ y = ° # ( θ (° # ( θ ))) → F ( y )],
que es decir
- β (° # ( θ )) ↔ F (° # ( θ (° # ( θ )))).
Ahora tome θ = β y ψ = β (° # ( β )), y la oración anterior se reescribe a ψ ↔ F (° # ( ψ )), que es el resultado deseado.
(El mismo argumento en diferentes términos se da en [Raatikainen (2015a)].)
Historia
El lema se llama "diagonal" porque guarda cierta semejanza con el argumento diagonal de Cantor . [5] Los términos "lemma diagonal" o "punto fijo" no aparecen en Kurt Gödel 's 1931 artículo o en Alfred Tarski ' s 1936 artículo .
Rudolf Carnap (1934) fue el primero en probar el lema general autorreferencial , [6] 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 funciones computables aún no se desarrolló en 1934. Mendelson (1997, p. 204) cree que Carnap fue el primero en afirmar que algo 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 recursividad de Kleene en la teoría de la computabilidad y sus respectivas demostraciones son similares.
Ver también
Notas
- ^ Hájek, Petr ; Pudlák, Pavel (1998) [primera impresión en 1993]. Metamatemáticas de la aritmética de primer orden . Perspectivas en lógica matemática (1ª ed.). Saltador. ISBN 3-540-63648-X. ISSN 0172-6641 .
En los textos modernos, estos resultados se prueban utilizando el conocido lema de diagonalización (o autorreferencia), que ya está implícito en la demostración de Gödel.
- ^ Ver Boolos y Jeffrey (2002, sec. 15) y Mendelson (1997, Prop. 3.37 y Cor. 3.44).
- ^ Para obtener detalles sobre la representabilidad, consulte Hinman 2005, p. 316
- ^ Smullyan (1991, 1994) son referencias especializadas estándar. El lema es la Prop. 3.34 de Mendelson (1997) y se trata en muchos textos sobre lógica matemática básica, como Boolos y Jeffrey (1989, sec. 15) y Hinman (2005).
- ^ Ver, por ejemplo, Gaifman (2006).
- ^ Kurt Gödel , Obras completas, Volumen I: Publicaciones 1929-1936 , Oxford University Press, 1986, p. 339.
- ^ Ver Obras completas de Gödel , vol. 1 , Oxford University Press, 1986, pág. 363, nota 23.
Referencias
- George Boolos y Richard Jeffrey , 1989. Computability and Logic , 3ª ed. Prensa de la Universidad de Cambridge. ISBN 0-521-38026-XISBN 0-521-38923-2
- Rudolf Carnap , 1934. Logische Syntax der Sprache . (Traducción al inglés: 2003. The Logical Syntax of Language . Open Court Publishing.)
- Haim Gaifman , 2006. ' Naming and Diagonalization: From Cantor to Gödel to 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 y Hall.
- Panu Raatikainen, 2015a. El lema de la diagonalización . En Stanford Encyclopedia of Philosophy , 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 . Universidad de Oxford. Prensa.
- Raymond Smullyan, 1994. Diagonalización y autorreferencia . Universidad de Oxford. Prensa.
- Alfred Tarski (1936). "Der Wahrheitsbegriff in den formalisierten Sprachen" (PDF) . Studia Philosophica . 1 : 261–405. Archivado desde el original (PDF) el 9 de enero de 2014 . Consultado el 26 de junio de 2013 .
- Alfred Tarski , tr. JH 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, Lógica, Semántica, Metamatemática , Hackett.