Validez indecidible en lógica de primer orden

Question

Estoy un poco confuso sobre la decidibilidad de la validez de las fórmulas lógicas de primer orden. Tengo un libro de texto que parece tener 2 afirmaciones contradictorias.

1)Teorema de Church: La validez de un enunciado lógico de primer orden es indecidible. (Lo que supongo significa que no se puede demostrar si una fórmula es válida o no) 2)Si A es válido, entonces la tabla semántica de not(A) se cierra. (A es un enunciado lógico de primer orden)

Según yo 2 contradice a uno ya que entonces podrías simplemente aplicar el algoritmo semántico tableau sobre A y demostrar su validez.

Estoy seguro de que me estoy perdiendo algo, pero ¿qué?

Answer 1

La lógica de primer orden no es indecidible exactamente, sino que a menudo se denomina semidecidible. Una afirmación válida de primer orden es siempre demostrablemente válida. Este es un resultado de los teoremas de completitud. Para todos los enunciados válidos existe un cálculo de demostración decidible, sólido y completo.

Sin embargo, la satisfacción es indecidible como consecuencia del teorema de Church. Si se puede resolver el Entscheidungsproblem para un enunciado de primer orden y es negación tienes un algoritmo para la satisfabilidad de primer orden, pero el teorema de Church demuestra que esto no es posible.

Ahora puede abordarlo con varios ejemplos de declaraciones: $\phi$ Una afirmación válida, $\psi$ Una afirmación cuya negación es válida, y $\chi$ una afirmación en la que ni ella ni su negación son válidas. Enunciados $\phi$ y $\psi$ son decidibles y demostrables, con tableau o resolución; utilizamos nuestro cálculo de prueba sobre $\phi$ , $\lnot$$ \phi $, $ \psi $, and $ \no $$\psi$ para saber qué declaraciones son válidas. Las sentencias no válidas no terminan, pero podemos abandonar nuestra búsqueda después de encontrar las válidas.

Para la declaración $\chi$ sin embargo, no existe ningún algoritmo para determinar que no es válido que garantice su terminación. Esto se debe a que puedes usar tu cálculo de prueba (elige el que quieras) para determinar la validez de una afirmación, o su negación. Si ni $\chi$ ni $\lnot$$ \chi$ son válidos sin embargo, su cálculo de prueba para determinar la validez no le dará ninguna información sobre la validez, ya que no terminará.

Answer 2

¿Y si la sentencia no es válida? Entonces el algoritmo no terminará.

Alternativamente, para cualquiera de los sistemas de prueba habituales, podemos enumerar todas las secuencias de sentencias y comprobar mecánicamente para cada secuencia si es una prueba de $\varphi$ . No es muy útil si $\varphi$ no es un teorema.

Observación: Podemos sacar algo útil de la idea. Supongamos que $T$ es una teoría axiomatizada recursivamente que es completa (para cualquier $\varphi$ o bien $\varphi$ es un teorema de $T$ o $\lnot\varphi$ es un teorema de $T$ ). Entonces existe un algoritmo que, para cualquier entrada $\varphi$ determinará si $\varphi$ es un teorema de $T$ .