Gödel ' s Teorema de lo completo y satisfacibilidad de una fórmula en lógica de primer orden

Question

Gödel original de la prueba del Teorema de Completitud de la lógica de primer orden se demuestra en la forma equivalente :

una fórmula $\varphi$ es válido o $\varphi$ es rebatible (es decir,$\vdash \lnot \varphi$).

Suponiendo que la lógica clásica, alguien puede exhibir un ejemplo de primer orden de la fórmula $\varphi$ para las que no somos capaces de decidir si es comprobable (es decir,$\vdash \varphi$) o si hay un contraejemplo (es decir,$\lnot \varphi$ es válido) ? En otras palabras, una fórmula $\varphi$ para las que no somos capaces de decidir si es válido o no ?

Añadido el 1 de Marzo

Siguiente de Carl respuesta, un ejemplo de una frase como la anterior puede ser costructed de la siguiente manera; ref Elliott Mendelson, Introducción a la Lógica Matemática (4ª ed - 1997), Ch.4: la Teoría de conjuntos Axiomática [página 225] :

(i) deje $\mathcal N$ la fórmula obtenida por la conjunción de los siguientes axiomas para $\mathsf {NBG}$ : Axioma T, Axioma D, Axioma N, Axiomas B1-B7, Axioma U, Axioma P, Axioma S, Axioma I, Axioma de CA, Axioma Reg (ningún axioma shemas), después de haber "unwinded" todo el conjunto de la teoría de las definiciones (como : $\emptyset$$\subseteq$) y después de haber sustituido en las fórmulas de arriba todas las ocurrencias de $\in$ binario con un símbolo de predicado $R$;

(ii) vamos a $RH$ la fórmula que se expresa en el lenguaje de la $\mathsf {NBG}$ la Hipótesis de Riemann, sujeto a las mismas "traducción".

Entonces :

$\mathcal N \land \lnot RH$

es un ejemplo de fórmula para la que no sabemos si es válido o si es rebatible.

Answer 1

Decidability - lo que significa que la computabilidad en esta cuestión - siempre se trata de un conjunto de fórmulas. No tiene mucho sentido buscar una fórmula única de la satisfiability de que no es decidable.

Esto es debido a que, si la fórmula es válido, entonces el programa que siempre salidas "Sí" será correcta, y si la fórmula no es válido, el programa que se emite siempre en "No" será correcta. Así que, en cierta forma trivial, el satisfiability de cada fórmula es decidable. Pero esto es tan trivial que no nos ven como muy interesante.

Lo cierto es que, cuando consideramos lo suficientemente ricos lenguajes de la lógica de primer orden, no hay un solo programa que, dado un arbitrario fórmula, decidirá si esa fórmula es válido o no. El punto clave es que este es un problema que involucra un conjunto infinito de fórmulas; el mismo programa tendría que decidir correctamente si cada uno de ellos es válido.

---

Todavía es el caso, por supuesto, que hay de las declaraciones individuales de la lógica de primer orden tal, que no sé si esas declaraciones son conste o no. Por ejemplo, supongamos $C$ ser cualquiera sin resolver la conjetura, expresado en el lenguaje de la teoría de conjuntos. Deje $A$ ser la conjunción de los conjunto finito de axiomas de NBG la teoría de conjuntos (que es más fuerte que la teoría de conjuntos ZFC). Entonces no sabremos si la fórmula $A \land \lnot C$ es válido o no. Podríamos tomar a $C$ a ser la hipótesis de Riemann, o cualquier otro problema sin resolver que se puede formalizar en la teoría de conjuntos.

El punto clave es que hay foundationally fuerte teorías que han finito de axiomas de los sistemas, por lo que podemos código de todo el sistema de axiomas como una sola fórmula. Que es también el hecho clave detrás de la prueba de que la lógica de primer orden no es decidable cuando el idioma es lo suficientemente rico.

Answer 2

Simplemente reemplace $\varphi$ $\lnot \varphi$ en la citada Declaración. Por lo tanto:

una fórmula $\lnot \varphi$ es solicitado o $\lnot \varphi$ es refutable ($\vdash \lnot \lnot \varphi$).

El punto es que $\lnot \lnot \varphi$ y $\varphi$ son lógicamente equivalentes en lógica clásica.

Dicho esto, es difícil decidir cual de los dos casos pasa por una determinada fórmula $\varphi$. De hecho, esto es equivalente a poder decidir si es o no una determinada teoría de primer orden consistente.

Answer 3

Primero de todo es que no es definitivamente una pregunta tonta, yo también soy todavía struggeling con ella.

Hay una diferencia entre decidability y la Integridad

Y el Teorema de Completitud de los estados que de la lógica de primer orden es.... Completa (el nombre es un poco de un dado).

mi punto de vista sobre las cosas: (por favor, ser conscientes de que todo esto puede estar equivocado)

• hay alguna fórmula donde la respuesta acerca de la validez depende del tamaño de la de dominio.

$\exists x R(x) \to \forall x R(x) $ es verdadero cuando el dominio contiene un solo elemento, pero falso en cualquier dominio más grande.

Supongamos ahora que tenemos una fórmula $\phi $ que es falso en cada finito de dominio, pero es cierto, en un infinito de dominio.

• No podemos hacer un contramodelo de $\phi $ sólo porque se requiere de un infinito de dominio.
• También no podemos prueba de $\lnot \phi $ porque no es sólo una declaración verdadera

Por lo $\phi $ $\lnot \phi $ son indecidible declaraciones

Y para $\phi $ podemos utilizar $( \forall x \forall y \forall z (((Rxy \land Ryz) \to Rxz ) \land \lnot Rxx) \land \forall y \exists x Rxy )$

($\phi $ es sólo la aritmética en el disfraz, interprete Rxy como $ x > y $)

Esto es sólo una primera idea, tal vez estoy equivocado.