El teorema de completitud de Gödel es un teorema fundamental en lógica matemática que establece una correspondencia entre verdad semántica y demostrabilidad sintáctica en lógica de primer orden .
El teorema de completitud se aplica a cualquier teoría de primer orden : si T es tal teoría, y φ es una oración (en el mismo idioma) y cada modelo de T es un modelo de φ, entonces hay una demostración (de primer orden). de φ usando los enunciados de T como axiomas. A veces se dice esto como "cualquier cosa verdadera en todos los modelos es demostrable". (Esto no contradice el teorema de incompletitud de Gödel , que trata sobre una fórmula φ u que no es demostrable en una determinada teoría T pero verdadera en el modelo "estándar" de los números naturales: φ u es falsa en alguna otra teoría "no estándar" modelos de T. [ 1] )
El teorema de completitud establece un estrecho vínculo entre la teoría de modelos , que se ocupa de lo que es verdadero en diferentes modelos, y la teoría de la prueba , que estudia lo que se puede probar formalmente en sistemas formales particulares .
Fue probado por primera vez por Kurt Gödel en 1929. Luego se simplificó cuando Leon Henkin observó en su doctorado. tesis de que la parte difícil de la demostración puede presentarse como el Teorema de existencia del modelo (publicado en 1949). [2] La prueba de Henkin fue simplificada por Gisbert Hasenjaeger en 1953. [3]
Existen numerosos sistemas deductivos para la lógica de primer orden, incluidos los sistemas de deducción natural y los sistemas de estilo Hilbert . Común a todos los sistemas deductivos es la noción de deducción formal . Se trata de una secuencia (o, en algunos casos, un árbol finito ) de fórmulas con una conclusión especialmente designada . La definición de deducción es tal que es finita y que es posible verificar algorítmicamente (mediante un ordenador , por ejemplo, o a mano) que una determinada secuencia (o árbol) de fórmulas es efectivamente una deducción.
Una fórmula de primer orden se considera lógicamente válida si es verdadera en todas las estructuras del lenguaje de la fórmula (es decir, para cualquier asignación de valores a las variables de la fórmula). Para enunciar formalmente y luego demostrar el teorema de completitud, es necesario definir también un sistema deductivo. Un sistema deductivo se llama completo si cada fórmula lógicamente válida es la conclusión de alguna deducción formal, y el teorema de completitud para un sistema deductivo particular es el teorema de que es completo en este sentido. Por tanto, en cierto sentido, existe un teorema de completitud diferente para cada sistema deductivo. Lo contrario de la integridad es la solidez , el hecho de que en el sistema deductivo sólo se pueden demostrar fórmulas lógicamente válidas.
Si algún sistema deductivo específico de lógica de primer orden es sólido y completo, entonces es "perfecto" (una fórmula es demostrable si y sólo si es lógicamente válida), por lo tanto equivalente a cualquier otro sistema deductivo con la misma cualidad (cualquier prueba en un sistema se puede convertir en el otro).
Primero fijamos un sistema deductivo de cálculo de predicados de primer orden, eligiendo cualquiera de los sistemas equivalentes conocidos. La prueba original de Gödel asumió el sistema de prueba de Hilbert-Ackermann.
El teorema de completitud dice que si una fórmula es lógicamente válida, entonces hay una deducción finita (una prueba formal) de la fórmula.
Por tanto, el sistema deductivo es "completo" en el sentido de que no se requieren reglas de inferencia adicionales para probar todas las fórmulas lógicamente válidas. Lo contrario de la integridad es la solidez , el hecho de que en el sistema deductivo sólo se pueden demostrar fórmulas lógicamente válidas. Junto con la solidez (cuya verificación es fácil), este teorema implica que una fórmula es lógicamente válida si y sólo si es la conclusión de una deducción formal.
El teorema se puede expresar de manera más general en términos de consecuencia lógica . Decimos que una oración s es una consecuencia sintáctica de una teoría T , denotada por , si s es demostrable a partir de T en nuestro sistema deductivo. Decimos que s es una consecuencia semántica de T , denotada , si s se cumple en todo modelo de T. El teorema de completitud dice entonces que para cualquier teoría de primer orden T con un lenguaje bien ordenable y cualquier oración s en el lenguaje de T ,
Dado que lo contrario (la solidez) también se cumple, se deduce que si y sólo si y, por tanto, esa consecuencia sintáctica y semántica son equivalentes para la lógica de primer orden.
Este teorema más general se usa implícitamente, por ejemplo, cuando se demuestra que una oración es demostrable a partir de los axiomas de la teoría de grupos considerando un grupo arbitrario y demostrando que ese grupo satisface la oración.
La formulación original de Gödel se deduce tomando el caso particular de una teoría sin ningún axioma.
El teorema de completitud también puede entenderse en términos de consistencia , como consecuencia del teorema de existencia del modelo de Henkin . Decimos que una teoría T es sintácticamente consistente si no existe una oración s tal que tanto s como sus negaciones ¬s sean demostrables a partir de T en nuestro sistema deductivo. El teorema de existencia del modelo dice que para cualquier teoría de primer orden T con un lenguaje bien ordenable,
Otra versión, con conexiones con el teorema de Löwenheim-Skolem , dice:
Dado el teorema de Henkin, el teorema de completitud se puede demostrar de la siguiente manera: Si , entonces no tiene modelos. Por contraposición al teorema de Henkin, entonces es sintácticamente inconsistente. Entonces una contradicción ( ) es demostrable en el sistema deductivo. Por tanto , y luego por las propiedades del sistema deductivo, .
El teorema de existencia del modelo y su demostración pueden formalizarse en el marco de la aritmética de Peano . Precisamente, podemos definir sistemáticamente un modelo de cualquier teoría de primer orden efectiva consistente T en aritmética de Peano interpretando cada símbolo de T mediante una fórmula aritmética cuyas variables libres son los argumentos del símbolo. (En muchos casos, necesitaremos asumir, como hipótesis de la construcción, que T es consistente, ya que la aritmética de Peano puede no probar ese hecho). Sin embargo, la definición expresada por esta fórmula no es recursiva (pero, en general, lo es). , Δ 2 ).
Una consecuencia importante del teorema de completitud es que es posible enumerar recursivamente las consecuencias semánticas de cualquier teoría efectiva de primer orden, enumerando todas las posibles deducciones formales de los axiomas de la teoría, y utilizar esto para producir una enumeración de sus conclusiones. .
Esto contrasta con el significado directo de la noción de consecuencia semántica, que cuantifica todas las estructuras en un lenguaje particular, que claramente no es una definición recursiva.
Además, hace que el concepto de "demostrabilidad", y por tanto de "teorema", sea un concepto claro que sólo depende del sistema de axiomas elegido de la teoría, y no de la elección de un sistema de prueba.
Los teoremas de incompletitud de Gödel muestran que existen limitaciones inherentes a lo que se puede probar dentro de cualquier teoría matemática de primer orden. La "incompletitud" en su nombre se refiere a otro significado de completo (ver teoría del modelo - Uso de los teoremas de compacidad y completitud ): una teoría es completa (o decidible) si cada oración en el lenguaje de es demostrable ( ) o refutable ( ) .
El primer teorema de incompletitud establece que cualquier oración que sea consistente , efectiva y contenga aritmética de Robinson (" Q ") debe ser incompleta en este sentido, al construir explícitamente una oración que no sea demostrable ni refutable en su interior . El segundo teorema de incompletitud amplía este resultado al mostrar que se puede elegir de modo que exprese la consistencia de sí mismo.
Como no se puede demostrar en , el teorema de completitud implica la existencia de un modelo de en el cual es falso. De hecho, es una oración Π 1 , es decir, establece que alguna propiedad finitista es verdadera para todos los números naturales; entonces, si es falso, entonces algún número natural es un contraejemplo. Si este contraejemplo existiera dentro de los números naturales estándar, su existencia sería refutada dentro ; pero el teorema de incompletitud demostró que esto es imposible, por lo que el contraejemplo no debe ser un número estándar y, por lo tanto, cualquier modelo de que sea falso debe incluir números no estándar .
De hecho, el modelo de cualquier teoría que contenga Q obtenido mediante la construcción sistemática del teorema de existencia del modelo aritmético siempre es no estándar, con un predicado de demostrabilidad no equivalente y una forma no equivalente de interpretar su propia construcción, de modo que esta construcción no es recursivo (ya que las definiciones recursivas no serían ambiguas).
Además, si es al menos ligeramente más fuerte que Q (por ejemplo, si incluye inducción para fórmulas existenciales acotadas), entonces el teorema de Tennenbaum muestra que no tiene modelos recursivos no estándar.
El teorema de completitud y el teorema de compacidad son dos piedras angulares de la lógica de primer orden. Si bien ninguno de estos teoremas puede demostrarse de manera completamente efectiva , cada uno puede obtenerse efectivamente del otro.
El teorema de compacidad dice que si una fórmula φ es una consecuencia lógica de un conjunto (posiblemente infinito) de fórmulas Γ, entonces es una consecuencia lógica de un subconjunto finito de Γ. Esta es una consecuencia inmediata del teorema de completitud, porque sólo un número finito de axiomas de Γ puede mencionarse en una deducción formal de φ, y la solidez del sistema deductivo implica entonces que φ es una consecuencia lógica de este conjunto finito. Esta demostración del teorema de la compacidad se debe originalmente a Gödel.
Por el contrario, para muchos sistemas deductivos, es posible demostrar el teorema de completitud como una consecuencia efectiva del teorema de compacidad.
La ineficacia del teorema de completitud se puede medir mediante la matemática inversa . Cuando se consideran en un lenguaje contable, los teoremas de completitud y compacidad son equivalentes entre sí y equivalentes a una forma débil de elección conocida como lema de Kőnig débil , con la equivalencia demostrable en RCA 0 (una variante de segundo orden de la aritmética de Peano restringida a la inducción). sobre Σ 0 1 fórmulas). El lema de Kőnig débil es demostrable en ZF, el sistema de teoría de conjuntos de Zermelo-Fraenkel sin axioma de elección y, por tanto, los teoremas de completitud y compacidad para lenguajes contables son demostrables en ZF. Sin embargo, la situación es diferente cuando el lenguaje tiene una cardinalidad arbitrariamente grande. Desde entonces, aunque los teoremas de completitud y compacidad siguen siendo demostrablemente equivalentes entre sí en ZF, también son demostrablemente equivalentes a una forma débil del axioma de elección conocido como lema del ultrafiltro. . En particular, ninguna teoría que extienda ZF puede probar los teoremas de completitud o compacidad en lenguajes arbitrarios (posiblemente incontables) sin probar también el lema del ultrafiltro en un conjunto de la misma cardinalidad.
El teorema de completitud es una propiedad central de la lógica de primer orden que no se aplica a todas las lógicas. La lógica de segundo orden , por ejemplo, no tiene un teorema de completitud para su semántica estándar (pero sí tiene la propiedad de completitud para la semántica de Henkin ), y el conjunto de fórmulas lógicamente válidas en la lógica de segundo orden no es recursivamente enumerable. Lo mismo ocurre con todas las lógicas de orden superior. Es posible producir sistemas deductivos sólidos para lógicas de orden superior, pero ningún sistema de este tipo puede ser completo.
El teorema de Lindström establece que la lógica de primer orden es la lógica más fuerte (sujeta a ciertas restricciones) que satisface tanto la compacidad como la integridad.
Se puede demostrar un teorema de completitud para la lógica modal o la lógica intuicionista con respecto a la semántica de Kripke .
La demostración original del teorema de Gödel procedió reduciendo el problema a un caso especial para fórmulas en una determinada forma sintáctica, y luego manejando esta forma con un argumento ad hoc .
En los textos de lógica moderna, el teorema de completitud de Gödel suele demostrarse con la prueba de Henkin , en lugar de con la prueba original de Gödel. La prueba de Henkin construye directamente un modelo temporal para cualquier teoría de primer orden consistente. James Margetson (2004) desarrolló una prueba formal computarizada utilizando el demostrador del teorema de Isabelle . [4] También se conocen otras pruebas.
