Teorema de completitud de Gödel - Gödel's completeness theorem

La fórmula ( ∀ x . R ( x , x )) → (∀ x ∃ y . R ( x , y )) se cumple en todas las estructuras (solo las 8 más simples se muestran a la izquierda). Por el resultado de integridad de Gödel, por lo tanto, debe tener una prueba de deducción natural (que se muestra a la derecha).

El teorema de completitud de Gödel es un teorema fundamental en lógica matemática que establece una correspondencia entre la verdad semántica y la demostrabilidad sintáctica en la 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 lenguaje) y cualquier modelo de T es un modelo de φ, entonces hay una prueba (de primer orden) de φ usar los enunciados de T como axiomas. A veces uno dice esto como "todo lo verdadero es demostrable".

Establece un vínculo estrecho entre la teoría de modelos que se ocupa de lo que es cierto 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 fue simplificado en 1947, cuando Leon Henkin observó en su Ph.D. tesis de que la parte difícil de la demostración puede presentarse como el Teorema de la existencia del modelo (publicado en 1949). La demostración de Henkin fue simplificada por Gisbert Hasenjaeger en 1953.

Preliminares

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 . Esta es una secuencia (o, en algunos casos, un árbol finito ) de fórmulas con una conclusión especialmente designada . La definición de una deducción es tal que es finita y que es posible verificar algorítmicamente (por una computadora , por ejemplo, oa mano) que una determinada secuencia (o árbol) de fórmulas es de hecho una deducción.

Una fórmula de primer orden se considera lógicamente válida si es verdadera en todas las estructuras para el 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 probar, 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 a la completitud es la solidez , el hecho de que solo las fórmulas lógicamente válidas pueden demostrarse en el sistema deductivo.

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 solo si es lógicamente válida), por lo que equivale a cualquier otro sistema deductivo con la misma calidad (cualquier prueba en un sistema se puede convertir en el otro).

Declaración

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.

Formulación original de Gödel

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 a la completitud es la solidez , el hecho de que sólo las fórmulas lógicamente válidas pueden demostrarse en el sistema deductivo. Junto con la solidez (cuya verificación es fácil), este teorema implica que una fórmula es lógicamente válida si y solo si es la conclusión de una deducción formal.

Forma más general

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 , si s es demostrable a partir de T en nuestro sistema deductivo. Decimos que s es una consecuencia semántica de T , denotado , si s tiene en cada modelo de camiseta . El teorema de completitud dice entonces que para cualquier teoría de primer orden T con un lenguaje bien ordenado y cualquier oración s en el lenguaje de T , ${\ Displaystyle T \ vdash s}$${\ Displaystyle T \ modelos s}$

si , entonces .${\ Displaystyle T \ modelos s}$${\ Displaystyle T \ vdash s}$

Dado que la recíproca (solidez) también es válida, se deduce que si y sólo si , y por lo tanto esa consecuencia sintáctica y semántica son equivalentes para la lógica de primer orden. ${\ Displaystyle T \ modelos s}$ ${\ Displaystyle T \ vdash s}$

Este teorema más general se usa implícitamente, por ejemplo, cuando se demuestra que una oración puede demostrarse a partir de los axiomas de la teoría de grupos al considerar un grupo arbitrario y mostrar 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.

Teorema de existencia del modelo

El teorema de completitud también se puede entender en términos de consistencia , como consecuencia del teorema de existencia del modelo de Henkin . Se dice que una teoría T es sintácticamente coherente si no hay sentencia s tal que ambos s y su negación ¬ s son demostrables de T en nuestro sistema deductivo. El teorema de existencia del modelo dice que para cualquier teoría T de primer orden con un lenguaje bien ordenado,

si es sintácticamente consistente, entonces tiene un modelo.${\ Displaystyle T}$${\ Displaystyle T}$

Otra versión, con conexiones al teorema de Löwenheim-Skolem , dice:

Toda teoría de primer orden contable y sintácticamente coherente tiene un modelo finito o contable.

Dado el teorema de Henkin, el teorema de completitud se puede demostrar de la siguiente manera: Si , entonces no tiene modelos. Por lo contrario del teorema de Henkin, entonces es sintácticamente inconsistente. Por tanto, se puede demostrar una contradicción ( ) en el sistema deductivo. Por lo tanto , a continuación, por las propiedades del sistema deductivo, . ${\ Displaystyle T \ modelos s}$${\ Displaystyle T \ cup \ lnot s}$${\ Displaystyle T \ cup \ lnot s}$${\ Displaystyle \ bot}$${\ Displaystyle T \ cup \ lnot s}$${\ Displaystyle (T \ cup \ lnot s) \ vdash \ bot}$${\ Displaystyle T \ vdash s}$

Como teorema de la aritmética

El teorema de la existencia del modelo y su demostración se pueden formalizar en el marco de la aritmética de Peano . Precisamente, podemos definir sistemáticamente un modelo de cualquier teoría T de primer orden efectiva consistente en la 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 suponer, 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 es, en general , Δ ₂ ).

Consecuencias

Una consecuencia importante del teorema de completitud es que es posible enumerar recursivamente las consecuencias semánticas de cualquier teoría de primer orden eficaz , enumerando todas las posibles deducciones formales de los axiomas de la teoría, y usar 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 del concepto de "demostrabilidad", y por tanto de "teorema", 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.

Relación con los teoremas de incompletitud

Los teoremas de incompletitud de Gödel muestran que existen limitaciones inherentes a lo que puede demostrarse dentro de cualquier teoría matemática de primer orden dada. La "incompletitud" en su nombre se refiere a otro significado de completo (ver teoría del modelo - Usando 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 ( ) . ${\ Displaystyle T}$${\ Displaystyle S}$${\ Displaystyle T}$${\ Displaystyle T \ vdash S}$${\ Displaystyle T \ vdash \ neg S}$

El primer teorema de incompletitud establece que todo lo que sea consistente , efectivo y contenga aritmética de Robinson (" Q ") debe estar incompleto 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 mostrando que se puede elegir de modo que exprese la consistencia de sí mismo. ${\ Displaystyle T}$${\ Displaystyle S_ {T}}$${\ Displaystyle T}$${\ Displaystyle S_ {T}}$${\ Displaystyle T}$

Dado que no se puede refutar en , el teorema de completitud implica la existencia de un modelo de en el cual es falso. De hecho, es una oración Π ₁ , es decir, establece que alguna propiedad finitista es verdadera para todos los números naturales; así que 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 se refutaría dentro ; pero el teorema de incompletitud mostró que esto era imposible, por lo que el contraejemplo no debe ser un número estándar y, por lo tanto, cualquier modelo en el que sea ​​falso debe incluir números no estándar . ${\ Displaystyle S_ {T}}$${\ Displaystyle T}$${\ Displaystyle T}$${\ Displaystyle S_ {T}}$${\ Displaystyle S_ {T}}$${\ Displaystyle S_ {T}}$${\ Displaystyle T}$${\ Displaystyle T}$${\ Displaystyle S_ {T}}$

De hecho, el modelo de cualquier teoría que contenga Q obtenido por la construcción sistemática del teorema de existencia del modelo aritmético, es siempre no estándar con un predicado de probabilidad 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 un poco más fuerte que Q (por ejemplo, si incluye inducción para fórmulas existenciales limitadas), entonces el teorema de Tennenbaum muestra que no tiene modelos no estándar recursivos. ${\ Displaystyle T}$

Relación con el teorema de la compacidad

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 probarse de manera completamente efectiva , cada uno puede obtenerse efectivamente del otro.

El teorema de la 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 solo un número finito de axiomas de Γ puede mencionarse en una deducción formal de φ, y la solidez del sistema deductivo implica que φ es una consecuencia lógica de este conjunto finito. Esta prueba del teorema de la compacidad se debe originalmente a Gödel.

Por el contrario, para muchos sistemas deductivos, es posible probar el teorema de completitud como una consecuencia efectiva del teorema de compacidad.

La ineficacia del teorema de completitud se puede medir siguiendo las líneas de las matemáticas inversas . Cuando se consideran sobre 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 ₀ (una variante de segundo orden de la aritmética de Peano restringida a la inducción más de Σ ⁰ ₁ fórmulas). El lema de König débil se puede demostrar en ZF, el sistema de la teoría de conjuntos de Zermelo-Fraenkel sin axioma de elección, y por lo tanto, los teoremas de completitud y compacidad para lenguajes contables se pueden demostrar en ZF. Sin embargo, la situación es diferente cuando el lenguaje es de cardinalidad grande arbitraria 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 el lema del ultrafiltro. . En particular, ninguna teoría que extienda ZF puede probar los teoremas de completitud o compacidad sobre lenguajes arbitrarios (posiblemente incontables) sin probar también el lema del ultrafiltro en un conjunto de la misma cardinalidad.

Completitud en otras lógicas

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 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 tal sistema no 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 .

Pruebas

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 generalmente se demuestra con la prueba de Henkin , en lugar de con la prueba original de Gödel. La prueba de Henkin construye directamente un modelo de término para cualquier teoría consistente de primer orden. James Margetson (2004) desarrolló una demostración formal computarizada utilizando el demostrador del teorema de Isabelle . También se conocen otras pruebas.

Ver también

• Teoremas de incompletitud de Gödel
• Prueba original del teorema de completitud de Gödel

Otras lecturas

• Gödel, K (1929). "Über die Vollständigkeit des Logikkalküls" . Tesis doctoral. Universidad de Viena. Cite journal requiere |journal=( ayuda ) La primera prueba del teorema de completitud.
• Gödel, K (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls". Monatshefte für Mathematik (en alemán). 37 (1): 349–360. doi : 10.1007 / BF01696781 . JFM  56.0046.04 . S2CID  123343522 . El mismo material que la disertación, excepto con pruebas más breves, explicaciones más sucintas y omitiendo la introducción extensa.

enlaces externos

• Enciclopedia de Filosofía de Stanford : " Kurt Gödel " —por Juliette Kennedy .
• Biografía de MacTutor: Kurt Gödel.
• Detlovs, Vilnis y Podnieks, Karlis, " Introducción a la lógica matemática " .