¿Cómo es la lógica de primer orden completa pero no decidible?

NO , la completitud de la lógica de primer orden no implica decidibilidad.

Estás mezclando dos usos de la integridad .

El primer uso se refiere a la integridad de los sistemas de prueba "estándar" para la lógica de primer orden .

Este es el Teorema de Completitud de Gödel , que dice:

El teorema de completitud dice que si una fórmula es lógicamente válida , entonces existe una deducción finita (una prueba formal) de la fórmula.

El teorema de completitud de Gödel dice que un sistema deductivo de cálculo de predicados de primer orden 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 opuesto a la completitud es la solidez, el hecho de que solo las fórmulas lógicamente válidas son demostrables 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 sólo si es la conclusión de una deducción formal.

Es fácilmente generalizable a la relación de consecuencia lógica entre un conjunto Γ de fórmulas de primer orden y una fórmula φ , en símbolos:

Γ ⊨ φ .

En este caso tenemos que:

Γ ⊨ φ si y solo Γ ⊢ φ (es decir, φ es demostrable a partir de Γ ).

Para simplificar, consideraremos el caso cuando Γ es el conjunto vacío; en este caso tenemos la versión anterior:

⊨ φ (es decir, φ es válido ) si y solo si ⊢ φ (es decir, φ es demostrable ).

Su falacia se refiere a la "propiedad básica" de validez :

no es cierto que si φ no es válido entonces ¬φ es válido .

Considere la fórmula:

∃x∃y ¬(x = y).

Significa: "hay al menos dos cosas x e y tales que no son iguales". Esta fórmula no es cierta en un universo con un solo elemento. Por lo tanto, no es válido (validez significa: verdadero en todos los universos).

Su negación es:

¬∃x∃y ¬(x = y)

lo que equivale a:

∀x∀y (x = y).

Significa "todas las cosas son iguales". Tampoco esta fórmula es válida, porque no es cierta en un universo con más de un elemento.

Compare con la lógica proposicional , donde una fórmula válida se llama tautología (la negación de una tautología se llama contradicción : una fórmula que siempre es falsa).

En este caso, tenemos un procedimiento de decisión : el algoritmo de la tabla de verdad (es muy "ineficiente", pero funciona...).

Aplíquelo a una fórmula A cualquiera: si en su columna tiene todas "T", entonces la fórmula es una tautología .

También en este caso hay un teorema de completitud: si A es una tautología, podemos encontrar una prueba de ello en los sistemas de prueba "habituales", como la Deducción Natural .

Pero nótese que también en este caso no es cierto que, para una fórmula A cualquiera, A sea una tautología o ¬A lo sea.

La formula :

pvq

no es ni una tautología ni una contradicción.

El segundo significado de completitud se refiere a las teorías , y es la clave de los famosos teoremas de incompletitud de Gödel que dice que:

El primer teorema de incompletitud establece que ningún sistema consistente de axiomas cuyos teoremas puedan enumerarse mediante un "procedimiento efectivo" (p. ej., un programa de computadora, pero podría ser cualquier tipo de algoritmo) es capaz de probar todas las verdades sobre las relaciones de la naturaleza. números (aritmética). Para cualquier sistema de este tipo, siempre habrá afirmaciones sobre los números naturales que sean verdaderas, pero que no se puedan probar dentro del sistema.

Este resultado (negativo) se refiere a otro aspecto de la "completitud" intuitiva (en el sentido de adecuación): para una teoría matemática, como la aritmética o la teoría de conjuntos, es razonable esperar que los axiomas (formalizados con lógica de primer orden) sean capaces de para "capturar" toda la verdad matemática expresable en esa teoría.

Para la mayoría de las teorías matemáticas "un poco complejas", esto no es posible.

Adicional

La decidibilidad está ligada al segundo significado de completitud .

Si una teoría T es completa (en el segundo sentido, más una segunda condición "técnica": efectivamente axiomatizada), es decir, T es capaz de probar todas las oraciones verdaderas φ expresables en el lenguaje de la teoría, debido al hecho de que φ es verdadero en T o ¬φ es verdadero en T , entonces T es decidible .

[ Nota . Si consideramos las dos fórmulas anteriores y consideramos su significado con respecto a la interpretación aritmética única, ahora tenemos que una de ellas es verdadera y la otra es falsa. Debido al hecho de que hay infinitos números naturales (y por lo tanto, más de uno), tenemos que la fórmula: ∃x∃y ¬(x = y) es verdadera en la interpretación aritmética (considere, por ejemplo , 1 y 2 ), mientras que su negación ∀x∀y (x = y) es obviamente falsa (no todos los números son iguales)].

Volviendo a la decidibilidad, ¿por qué una teoría completa es así?

Exactamente porque el "procedimiento" descrito en su pregunta funciona: comience a probar teoremas en T . Después de una cantidad finita de tiempo, si φ es cierto, encontrarás la prueba de ello; si no lo es, entonces ¬φ es cierto y encontrarás una prueba de ello.

Como se dijo antes, este "procedimiento" no sirve para la validez porque no es cierto que una fórmula o su negación sean válidas.

El teorema de incompletitud de Gödel demuestra que las teorías formalizadas que tienen suficiente "capacidad" para expresar hechos aritméticos no son completas en el segundo sentido: no pueden "capturar" todos los hechos aritméticos verdaderos.

Por lo tanto, las teorías anteriores no son decidibles.

¿Cuál es el "vínculo" entre los dos usos de la completitud ?

Considere una teoría T de primer orden que incluya el lenguaje de la aritmética.

La lógica "subyacente" de fo es completa (primer sentido): es decir, es capaz de probar todas las consecuencias lógicas de los axiomas de la teoría T.

Pero la teoría T es incompleta (según el teorema de incompletitud de Gödel), es decir, hay una oración aritmética verdadera φ no demostrable a partir de los axiomas de T.

Y qué ?

No es una contradicción. Considere la definición de consecuencia lógica aplicada a T :

T ⊨ φ iff φ es cierto en todos los modelos de T .

Siendo φ cierto en el "modelo previsto" de aritmética (los números "habituales") concluimos que no es cierto en algún otro modelo [ver el comentario de Francis Davey]: hay un modelo de aritmética no estándar .

Siendo así, no es una consecuencia lógica de los axiomas de T y esta es la razón por la cual su indemostrabilidad en T no entra en conflicto con la completitud de la lógica subyacente.

Dado que Taylor Hornby ya auto-corrigió la definición de completitud (gracias a la primera definición de Mauro ALLEGRANZA), solo quiero señalar dónde exactamente se extravía su razonamiento.

¿Por qué la completitud no implica decidibilidad para la lógica de primer orden? Taylor Hornby razona de la siguiente manera:

¿Por qué no funciona esto? Enumerar todas las cadenas x. Si x codifica la derivación válida de B de A, acepte. Si x codifica la derivación válida de ~B de A, rechace.

Debido a la completitud, eventualmente este proceso tropezará con una x que es una prueba de B o ~B de A. Si B, entonces A implica B en todas las interpretaciones. Si ~B, entonces no es el caso que A implique B en todas las interpretaciones. Entonces FOL es decidible.

lo que está mal aquí es la frase:

Debido a la completitud, eventualmente este proceso tropezará con una x que es una prueba de B o ~B de A.

Completitud por definición significa "Si B está lógicamente implicado, entonces B es demostrable". Es una declaración condicional. Ahora bien, en general, no sabemos de antemano si un B dado está lógicamente implicado o no. Entonces no sabemos si hay una prueba de B o no. Así que lo que realmente sucede es esto:

Eventualmente, este proceso tropezará con una x que es una prueba de B o ~B de A, O BIEN, este proceso continuará ejecutándose para siempre.

Es decir, este algoritmo no siempre determina si B está lógicamente implicado (o de manera equivalente, si B es demostrable, gracias a las propiedades de solidez y completitud de FOL). Si B o ~B son demostrables, eventualmente encontraremos su prueba. Pero si ni B ni ~B son demostrables, entonces nunca podemos saber si no hay prueba o si solo necesitamos seguir buscando. Entonces, este algoritmo no nos da una respuesta para cada B, pero podemos preguntarnos si hay un algoritmo mejor que nos dé una respuesta para cada B. El problema de detención de Turing se usa para mostrar que no hay un algoritmo para determinar si B es lógicamente implicado.

La lógica de primer orden es completa porque todos los enunciados implicados son demostrables, pero es indecidible porque no existe un algoritmo para decidir si una oración dada está o no implicada lógicamente.

Hay límites definitivos para las máquinas, sin importar cuán inteligentemente estén diseñadas. En 1936, Turing demostró matemáticamente que nunca puede existir un algoritmo general para resolver el problema para todos los pares programa-entrada posibles. Es decir, no se puede escribir ningún algoritmo de modo que siempre decida correctamente, para cualquier par programa-entrada dado, si el programa se detendrá o no. En informática, esto se llama el problema de detención. Turing demostró que se puede hacer que cualquier algoritmo se contradiga a sí mismo y, por lo tanto, no puede decidir correctamente. Como ilustración, podemos hacer uso de un par de entrada de programa "patológico" diseñado para hacer lo contrario de lo que el algoritmo predice que hará.

La prueba de Turing implica que es imposible predecir si la máquina de Turing programada para atacar ciertos problemas matemáticos alguna vez tendrá éxito y se detendrá, o seguirá funcionando para siempre. En realidad, un límite último equivalente se aplica a los humanos: también es imposible predecir si los matemáticos alguna vez tendrán éxito en la resolución de estos mismos problemas.

La pregunta crucial se refiere a la completitud y la decidibilidad (en cuanto a si un teorema es verdadero o falso, pero no ambos), que es equivalente al problema de detención en la informática. La incompletitud abre la puerta a la posibilidad de la indecidibilidad. Una demostración exitosa de un problema particular implica que no es indecidible en la teoría (o sistema) donde se formula. Pero tal prueba no implica que la teoría misma sea completa o decidible. Puede haber otros problemas en la teoría que son indecidibles, en cuyo caso no existe solución. En una teoría incompleta, hay teoremas o ecuaciones, por ejemplo, que parecen intuitivamente verdaderos pero que no se pueden demostrar. Por lo tanto, es imposible predecir si un problema particular formulado en una teoría incompleta podrá resolverse alguna vez.

Estoy bastante seguro de que esto es correcto, pero no estoy 100% seguro:

Una posible confusión es que podemos pensar que estamos hablando de un solo modelo, cuando en realidad estamos hablando de todos los modelos posibles que satisfacen un conjunto particular de axiomas. Entonces, si estamos hablando de un modelo, entonces P o NOT P es verdadero, pero si estamos hablando de varios, entonces P puede ser válido, NOT P puede ser válido o puede ser mixto (aquí válido = siempre verdadero).

Completitud significa que si P es válida lo probaremos eventualmente y dado que NOT P es solo otra proposición, si es válida lo mismo para eso. Sin embargo, esto no garantiza nada sobre las proposiciones mixtas. Nunca podemos saber que si no seguimos buscando por más tiempo no encontraremos una prueba para P o NOT P.

O para aclarar aún más, las siguientes dos afirmaciones son diferentes:

• "NO P" es válido
• NO "P es válida"

El último también incluye P siendo mezclado

La lógica de primer orden es solo álgebra, disfrazada, mientras que la lógica de orden superior es análisis. Las teorías formuladas en lógica de primer orden pueden expresarse como sistemas algebraicos: un sistema que contiene un conjunto de operaciones, un conjunto de objetos distinguidos y un conjunto de identidades ecuacionales; mientras que las teorías formuladas en lógica de orden superior que no son equivalentemente expresables o reducibles a teorías de primer orden, pueden considerarse correctamente como cálculos.

Por ejemplo, un grupo abeliano se puede expresar como un álgebra que contiene una sola operación ("-" para resta), un objeto distinguido ("0") y las siguientes identidades: 0 - 0 = 0, x - (x - y ) = y y x - (y - z) = z - (y - x).

Además, por ejemplo, una Geometría Afín A sobre un campo específico F se puede expresar como un álgebra de dos tipos que contiene los operadores ternarios a,f,b ∈ A×F×A ↦ [a,f,b] ∈ A y a ,b,c ∈ A×A×A ↦ abc ∈ A que encarna las operaciones [a,f,b] = (1 - f)a + fb y abc = a - b + c. Un ejemplo de axiomas (adecuados, excepto por los dos campos F = GF(2) de tamaño 2 y F = GF(3) de tamaño 3) es: [a,0,b] = a, [a,1,b ] = b, [a,rt(1-t),[b,s,c]] = [[a,rt(1-s),b],t,[a,rs(1-t),c ]], abc = [[b,1/(1-t),a],t,[b,1/t,c]], donde t se elige arbitrariamente como cualquier miembro del campo F distinto de 0 o 1 .

Para las teorías algebraicas, el "álgebra libre" es la que contiene sólo los objetos distinguidos y cualquier otro objeto que se pueda hacer a partir de ellos usando las operaciones del álgebra. También se puede hablar de "álgebra libre generada a partir de un conjunto X", donde los miembros del conjunto X se agregan a la lista de objetos distinguidos. Por ejemplo, el álgebra de resta, arriba, generada libremente a partir del conjunto {1} es una y la misma que el álgebra de resta de enteros, y contiene también el álgebra de suma de enteros por medio de las definiciones, -x = (x - x ) - x, y x + y = x - (-y). (Se puede probar x - x = 0 usando los axiomas, a saber: x = 0 - (0 - x) = x - (0 - 0) = x - 0, y x - x = x - (x - 0) = 0, entonces -x = 0 - x es una definición equivalente, pero menos independiente).

Entonces, las teorías de primer orden siempre pueden realizarse mediante modelos, lo que hace que la lógica de primer orden sea completa. Esto se afirma con mayor precisión en el resumen, extraído a continuación, de "Teorías de primer orden como álgebras clasificadas por muchos" (Notre Dame Journal Of Formal Logic 25 (1), enero de 1984 https://www.researchgate.net/publication/ 38355700_First-order_theories_as_many-sorted_algebras )

La completitud asegura que se pueda encontrar una prueba para cualquier declaración válida mediante una búsqueda finita. La imposibilidad de encontrar una prueba, cuando una declaración no es válida, ocurre solo después de que la búsqueda interminable a través de todas las pruebas posibles nunca termina. Entonces, tendría que esperar una eternidad para que nunca termine, primero, antes de ver un "no" como respuesta a la consulta "¿es válido?". Para que sea decidible, la respuesta "no" tiene que llegar algún tiempo antes de que el siempre nunca termine de suceder.

El extracto clave del resumen:

"En este artículo, al desarrollar el estudio de la lógica de primer orden a través de álgebras de orden múltiple, mostramos que cada teoría de primer orden es un álgebra particular que verifica axiomas en forma ecuacional (ver Sección 2); por lo tanto, podemos aplicar el método de Birkhoff teoremas relativos a las variedades (ver Sección 1 [y dos referencias contenidas en el documento]) y para obtener los modelos de Henkin algebraicamente, de donde surge el teorema de completitud de la lógica de primer orden (ver Sección 3)."

Remate: "Muchos ordenados" es la frase clave; por lo tanto, agregue un tipo booleano y rehaga los predicados como operadores con valores booleanos.