Teorema de completitud de Gödel

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 lógica de primer orden .

El teorema de completitud se aplica a cualquier teoría de primer orden : si T es una teoría de este tipo, y φ es una proposición (en el mismo lenguaje), y todo modelo de T es un modelo de φ , entonces existe una demostración (de primer orden) de φ utilizando las proposiciones de T como axiomas . A veces se dice que "todo lo que es verdadero en todos los modelos es demostrable". (Esto no contradice el teorema de incompletitud de Gödel , que trata sobre una fórmula φ _u que es indemostrable en una teoría T determinada , pero verdadera en el modelo "estándar" de los números naturales: φ _u es falsa en otros modelos "no estándar" de T. ^{[ 1 ]} )

El teorema de completitud 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 demostración , que estudia lo que se puede demostrar formalmente en sistemas formales particulares .

Fue demostrado por primera vez por Kurt Gödel en 1929. Posteriormente, fue simplificado cuando Leon Henkin observó en su tesis doctoral que la parte difícil de la demostración puede presentarse como el Teorema de Existencia de Modelos (publicado en 1949). ^{[ 2 ]} La demostración de Henkin fue simplificada por Gisbert Hasenjaeger en 1953. ^{[ 3 ]}

Existen numerosos sistemas deductivos para la lógica de primer orden, incluyendo sistemas de deducción natural y sistemas de estilo Hilbert . Todos los sistemas deductivos comparten la noción de deducción formal . Esta consiste en una secuencia (o, en algunos casos, un árbol finito) de fórmulas con una conclusión específica . La definición de deducción implica que es finita y que es posible verificar algorítmicamente (por ejemplo, mediante una computadora o manualmente) que una secuencia (o árbol) de fórmulas dada constituye, en efecto, una deducción.

Una fórmula de primer orden se considera lógicamente válida si es verdadera en cualquier estructura 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 considera completo si toda 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 que demuestra su completitud en este sentido. Por lo tanto, en cierto modo, existe un teorema de completitud diferente para cada sistema deductivo. Un recíproco de la completitud es la solidez , el hecho de que solo las fórmulas lógicamente válidas son demostrables en el sistema deductivo.

Si un 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), y por lo tanto equivalente a cualquier otro sistema deductivo con la misma calidad (cualquier prueba en un sistema puede convertirse en el otro).

Primero fijamos un sistema deductivo de cálculo de predicados de primer orden, eligiendo cualquiera de los sistemas equivalentes conocidos. La demostración original de Gödel asumía el sistema de demostración de Hilbert - Ackermann .

Forma más general

El teorema puede expresarse de forma 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${\displaystyle T\vdash s}$, si s es demostrable a partir de T en nuestro sistema deductivo. Decimos que s es una consecuencia semántica de T , denotada${\displaystyle T\models s}$, si s se cumple en cada 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 sentencia s en el lenguaje de T ,

si${\displaystyle T\models s}$, entonces${\displaystyle T\vdash s}$.

Dado que lo contrario (la solidez) también se cumple, se deduce que${\displaystyle T\models s}$si y solo si${\displaystyle T\vdash s}$y, por lo tanto, que la consecuencia sintáctica y semántica son equivalentes para la lógica de primer orden.

Este teorema más general se utiliza 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 la oración es satisfecha por ese grupo.

La formulación original de Gödel se deduce tomando el caso particular de una teoría sin axiomas.

Teorema de existencia del modelo

El teorema de completitud también puede entenderse en términos de consistencia , como consecuencia del teorema de existencia de modelos de Henkin . Decimos que una teoría T es sintácticamente consistente si no hay ninguna oración s tal que tanto s como su negación ¬s sean demostrables a partir de T en nuestro sistema deductivo. El teorema de existencia de modelos dice que para cualquier teoría de primer orden T con un lenguaje bien ordenable,

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

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

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

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

Una consecuencia importante del teorema de completitud es que es posible enumerar computacionalmente las consecuencias semánticas de cualquier teoría de primer orden enumerable computacionalmente, 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 sobre todas las estructuras en un idioma particular, lo cual claramente no es una definición recursiva.

Además, convierte el concepto de "demostrabilidad" y, por lo tanto, de "teorema", en un concepto claro que solo depende del sistema de axiomas elegido para la teoría, y no de la elección de un sistema de demostración.

Los teoremas de incompletitud de Gödel muestran que existen limitaciones inherentes a lo que se puede demostrar dentro de cualquier teoría de primer orden dada en matemáticas. La "incompletitud" en su nombre se refiere a otro significado de completo (véase teoría de modelos: uso de los teoremas de compacidad y completitud ): una teoría${\displaystyle T}$es completa (o decidible) si cada oración${\displaystyle S}$en el idioma de${\displaystyle T}$es demostrable (${\displaystyle T\vdash S}$) o refutable (${\displaystyle T\vdash \neg S}$).

El primer teorema de incompletitud establece que cualquier${\displaystyle T}$que es consistente , computablemente enumerable y contiene aritmética de Robinson (" Q ") debe ser incompleto en este sentido, al construir explícitamente una oración${\displaystyle S_{T}}$que es demostrablemente ni probable ni refutable dentro${\displaystyle T}$. El segundo teorema de incompletitud extiende este resultado al demostrar que${\displaystyle S_{T}}$puede ser elegido de manera que exprese la consistencia de${\displaystyle T}$sí mismo.

Desde${\displaystyle S_{T}}$no se puede probar en${\displaystyle T}$, el teorema de completitud implica la existencia de un modelo de${\displaystyle T}$en el cual${\displaystyle S_{T}}$es falso. De hecho,${\displaystyle S_{T}}$es una oración Π ₁ , es decir, afirma que alguna propiedad finitista es verdadera para todos los números naturales; por lo tanto, si es falsa en un modelo, entonces uno de los números naturales del modelo es un contraejemplo. Si este contraejemplo existiera dentro de los números naturales estándar, su existencia refutaría${\displaystyle S_{T}}$dentro${\displaystyle T}$; pero el teorema de incompletitud demostró que esto era imposible, por lo que el contraejemplo no debe ser un número estándar y, por lo tanto, cualquier modelo de${\displaystyle T}$en el cual${\displaystyle S_{T}}$es 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, es siempre 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 recursiva (ya que las definiciones recursivas serían inequívocas).

Además, si${\displaystyle T}$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 pilares fundamentales de la lógica de primer orden. Si bien ninguno de estos teoremas puede demostrarse de forma totalmente efectiva , cada uno puede derivarse eficazmente del otro.

El teorema de compacidad establece 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 Γ. Esto es una consecuencia inmediata del teorema de completitud, ya que solo un número finito de axiomas de Γ pueden 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 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 puede medirse siguiendo las líneas de la matemática inversa . Cuando se consideran sobre un lenguaje numerable, los teoremas de completitud y compacidad son equivalentes entre sí y equivalentes a una forma débil de elección conocida como lema débil de Kőnig , con la equivalencia demostrable en RCA ₀ (una variante de segundo orden de la aritmética de Peano restringida a la inducción sobre fórmulas Σ ⁰ ₁ ). El lema débil de Kőnig es demostrable 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 numerables son demostrables en ZF. Sin embargo, la situación es diferente cuando el lenguaje tiene una cardinalidad arbitrariamente grande, ya que 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 conocida como lema del ultrafiltro . En particular, ninguna teoría que extienda ZF puede demostrar los teoremas de completitud o compacidad sobre lenguajes arbitrarios (posiblemente no numerables) sin demostrar también el lema del ultrafiltro en un conjunto de la misma cardinalidad.

El teorema de completitud es una propiedad fundamental de la lógica de primer orden que no se cumple para todas las lógicas. La lógica de segundo orden , por ejemplo, no posee un teorema de completitud para su semántica estándar (aunque sí para la semántica de Henkin ), y el conjunto de fórmulas lógicamente válidas en lógica de segundo orden no es recursivamente enumerable. Lo mismo ocurre con todas las lógicas de orden superior. Es posible construir 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 completitud.

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 con una determinada forma sintáctica, y luego tratando esta forma con un argumento ad hoc .

En los textos de lógica modernos, el teorema de completitud de Gödel se suele demostrar con la demostración de Henkin , en lugar de con la demostración original de Gödel. La demostración de Henkin se presenta a menudo con los siguientes pasos:

• Henkinizar la teoría, asegurándose de que para cada fórmula${\displaystyle \psi (x)}$hay una constante${\displaystyle c_{\psi }}$y axioma${\displaystyle \exists _{x}\psi (x)\to \psi (c_{\psi })}$.
• Aplique el lema de Lindenbaum para obtener una extensión completa.
• Construir el modelo de términos asociado. ^{[ 4 ]}

James Margetson (2004) desarrolló una demostración formal computarizada utilizando el demostrador de teoremas Isabelle . ^{[ 5 ]} También se conocen otras demostraciones.

• Demostración original del teorema de completitud de Gödel
• Teorema de Trakhtenbrot

• Godel, K (1929). Über die Vollständigkeit des Logikkalküls (Tesis). Tesis doctoral. Universidad de Viena.La primera demostración del teorema de completitud.
• Godel, 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 material es el mismo que el de la tesis doctoral, pero con demostraciones más breves, explicaciones más concisas y omitiendo la larga introducción.
• Hans Hermes (1973). Introducción a la lógica matemática . Hochschultext (Springer-Verlag). Londres: Springer. ISBN 3540058192ISSN 1431-4657​​ Capítulo 5: "El teorema de completitud de Gödel" .

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