¿Cómo verificar la satisfacibilidad en un modelo? (Confusiones con el Teorema de Completitud de Gödel)

Question

No puedo creer que el Teorema de Completitud de Gödel sea correcto.

Supongamos que hemos fijado alguna lógica de primer orden con alguna estructura. El teorema afirma que para cualquier enunciado $P$ en esta lógica tenemos que

$$\vdash P\iff \mathcal{M}\vDash P \hspace{5pt}\text{para cada modelo}\hspace{5pt}\mathcal{M}.$$ Mis dudas se deben a las definiciones de los símbolos anteriores.

$\vdash P$ significa que hay una prueba formal de $P$ con respecto a la lógica clásica.

$\mathcal{M}\vDash P$ significa que $P$ es verdadero en $\mathcal{M$. Lo que significa que $P$ tratado como fórmula se cumple para cualquier asignación de valores $g.$ Se denota como $\mathcal{M},g\vDash P.$ Satisfacción como se escribe en este gran sitio está definido recursivamente. Considera solo el primer paso de la recursión, es decir, $$M,g\vDash R(\tau_1,\dots,\tau_k) \hspace{5pt}\text{si y solo si}\hspace{5pt}(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$$ donde $R$ es alguna relación de la estructura de la lógica de primer orden y $I^g_F,F$ son partes de la interpretación.

Veo el problema porque en algunos modelos $(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$ puede ser indeterminado. De hecho, considera $R$ como la relación $=.$ Podemos terminar con una situación teórica de conjunto $\mathfrak{c}=\aleph_1$. No se puede decir si esto es verdad o no.

En resumen, $\vdash P$ parece ser una definición muy concreta con formas claras de verificación. Por otro lado, $\mathcal{M} \vDash P$ no nos dice cómo verificar nada en el modelo.

Por favor, dime qué está mal con este razonamiento.

Answer 1

Yo diría que están a la derecha - no hay ninguna razón para esperar que Goedel del teorema de completitud para ser verdad!

Excepto para la prueba.

Considero que el teorema de completitud para ser el más contrario a la intuición como resultado básicas de la lógica, mucho más que el teorema de la incompletitud (cuyo surprisingness es, de hecho, discutible. Como usted dice, muestra que de una forma muy concreta de la declaración "$T\vdash \varphi$" es equivalente a una aparentemente mucho más complicado declaración "Cada modelo de $T$ satisface $\varphi$", y la complejidad de este último es sugerido por el hecho de que, de fijo,$M$$\varphi$, a la pregunta "¿ $M\models\varphi$ ? " es en general de muy alta complejidad.

Una manera de pensar acerca de lo que sucede es esto: saber si cada modelo de $T$ satisface $\varphi$ puede ser más fácil de decir si un determinado modelo de $T$ satisface $\varphi$. Modelos específicos, puede ser muy complicado; sin embargo, cada teoría también tiene modelos que son "razonablemente simple" (ver más abajo para más información sobre esto). Estos modelos suelen ser antinatural, pero que existen, y que llevan a la pregunta de si $T\models\varphi$; y es que estos modelos, esencialmente, que la hacen la pregunta de un responsable.

---

Habiendo reconocido que la GCT es contrario a la intuición, ahora me intente convencer de que es cierto.

Vamos a probar el contrapositivo: que si $T\cup\{\neg\varphi\}$ es consistente, entonces podemos construir un modelo de $M$$T$$M\not\models\varphi$. Tenga en cuenta que esto hace nuestro trabajo mucho más fácil - sólo tenemos que construir un modelo! Y aunque el general problema "No $N\models \psi$?" es muy complicado, la específica cuestión que nos interesa ("No $M\models\varphi$?") no puede ser tan malo.

Aquí está la construcción natural a tener en cuenta: tome el conjunto de términos en el idioma de $T$, y "mod" por $(T\cup\{\neg\varphi\})$-comprobable de equivalencia. E. g. en una adecuada teoría de la aritmética, "$1+1$" y "$(1+1)\times 1$" son términos que seguramente son iguales, por lo que representan la misma clase de equivalencia. No es difícil mostrar que las operaciones y las relaciones de la lengua están bien definidos en estas clases de equivalencia. Así que hay una estructura natural asignado a la teoría de la $T\cup\{\neg\varphi\}$; si se para a pensarlo un poco, debe ser plausible que este es de hecho un modelo de $T\cup\{\neg\varphi\}$!

. . . Por supuesto, es no, sin embargo. La prueba no es tan sencillo. Pero la idea es correcto, sólo necesita un poco de trabajo. Parte de este trabajo consiste en la mejora de la teoría de la $T\cup\{\neg\varphi\}$ sí ($T\cup\{\neg\varphi\}$ no pueden "decidir" ciertas preguntas importantes; por otra parte, el lenguaje de la $T\cup\{\neg\varphi\}$ no pueden "tener suficiente términos" para construir la estructura que queremos); la otra parte de la obra consiste en trabajar con las propiedades específicas de la provability relación "$\vdash$". (Ver, por ejemplo, estas dos preguntas, respectivamente).

---

A un lado: "simple" de los modelos. (No, no me refiero a que tipo de simplicidad.) La prueba de la Integridad Teorema hizo un gesto vagamente a la de arriba es una construcción de un modelo - aunque sea uno que no es computable. Pero podemos preguntar cómo noncomputable es. Resulta que en realidad no es muy noncomputable - es decir, tenemos:

Supongamos $T$ es una contables de la teoría en una contables idioma. A continuación, hay un modelo de $T$ que es baja en relación a $T$.

Aquí, "bajo" es una computabilidad teoría de la propiedad: un conjunto $X$ es baja si la detención problema relativo a $X$ no es más complicada que la clásica detener problema. Bajeza relativa a $A$ se define de manera similar. Por comparación, a la pregunta "¿$T$ probar $\varphi$?" es en el nivel de la suspensión problema relativo a $T$; así que, en realidad, estamos construyendo un modelo que es más simple que el original provability pregunta!

---

Tenga en cuenta que una de las consecuencias de la GCT es que preguntas como "¿ $2^{\aleph_0}=\aleph_1$?" nunca surgen cuando se trata de responder a preguntas como "¿ todos los modelos de $T$ satisfacer $\varphi$?"

Pero esto es sólo un resultado de primer orden de la lógica! De vista de la lógica general, el conjunto teórico de cuestiones de hecho puede recortar.

Un gran ejemplo de esto es de segundo orden de la lógica (con el estándar, como contraposición a Henkin, la semántica; la semántica de Henkin hace esencialmente equivalente a la lógica de primer orden). De segundo orden, la lógica permite cuantificar las relaciones y funciones en el dominio, además de los individuos (que es lo que la lógica de primer orden permite cuantificar el exceso). Por ejemplo, hay un segundo orden de la frase verdadera exactamente en el infinito de estructuras: parece que "Hay un inyectiva, no surjective función", o más formalmente $$\exists F[\forall x, y(F(x)=F(y)\implies x=y)\wedge \exists z\forall x(F(x)\not=z)].$$ Para Compacidad inmediatamente falla de segundo orden de la lógica. Pero el que se lleva la palma es:

Hay una frase que $\chi$ en el segundo orden de la lógica, que es una de validez (= true en cada estructura) si y sólo si el Continuum de la Hipótesis es verdadera.

Esto toma un poco de trabajo para probar; si usted está interesado, voy a añadir su construcción en detalle.

Mi punto es que el conjunto teórico de cuestiones de hecho vienen cuando se trata de analizar la satisfacción de la relación arbitraria de la lógica; pero GCT muestra que la lógica de primer orden es especialmente agradable. Y este es, de hecho, una muy trivial hecho!

Si usted está interesado en la comparación de la lógica de primer orden con otras lógicas, usted puede estar interesado en el modelo abstracto de la teoría!

Answer 2

Observa que el lado derecho dice "para cada modelo $\mathcal{M}$. Si algo es indecidible, entonces será verdadero para algunos modelos y falso para otros. Así que el lado derecho falla, y también lo hace el lado izquierdo, es decir, no hay una prueba formal de una afirmación indecidible en lógica de primer orden. Todo esto es como se esperaba.

Answer 3

Veo el problema porque en algunos modelos $(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$ puede ser indecidible.

Creo que estás confundiendo demostrabilidad con satisfacción, ya que para cualquier modelo en particular una oración siempre será verdadera o falsa. La indecidibilidad se aplica a la demostrabilidad, ya que puede ser el caso que una oración sea verdadera en algunos modelos y no en otros.

Podemos terminar con una situación teórica de conjuntos $\mathfrak{c}=\aleph_1$. Uno no puede decir si esto es cierto o no.

Podemos decir si esto es cierto en algún modelo particular. Recuerda que Gödel y Cohen juntos demostraron que CH es cierto en algunos modelos de ZFC y no en otros. La completitud simplemente dice que este hecho es suficiente para demostrar que CH es independiente de ZFC.