El teorema de completitud de Gödel y la indecidibilidad de la lógica de primer orden

Question

Estoy trabajando a través de este módulo En este sentido, me gustaría hablar de los dos ejercicios que aparecen inmediatamente después del enunciado del teorema de completitud de Godel.

En primer lugar, observe la definición 2.1 del texto: Una frase $\varphi$ es válido si es cierto en todos los modelos. Por el contrario, $\varphi$ es satisfaciendo si es verdadera en algún modelo. Entonces los ejercicios se dan de la siguiente manera:

1. Dejemos que $\varphi$ sea una sentencia en lógica de primer orden. Demuestre que $\varphi$ es válido si y sólo si $\neg\varphi$ no es satisfacible, y en consecuencia que $\varphi$ es satisfacible si y sólo si $\neg\varphi$ no es válido.

2. Supongamos que tenemos un algoritmo $\mathcal{A}$ para saber si una sentencia de la lógica de primer orden es satisfacible o no. Demuestre que podemos usar esto para obtener un algoritmo $\mathcal{B}$ para saber si una sentencia de la lógica de primer orden es demostrable o no. A la inversa, supongamos que tenemos un algoritmo $\mathcal{B}$ para saber si una sentencia de la lógica de primer orden es demostrable o no. Demuestre que podemos usar esto para obtener un algoritmo $\mathcal{A}$ para saber si una sentencia de la lógica de primer orden es satisfacible o no.

El primer ejercicio parece bastante sencillo. Mi respuesta:

1. Dejemos que $\mathscr{M}$ ser un modelo y leer " $\varphi$ es cierto en $\mathscr{M}$ " para $\mathscr{M}\models\varphi$ . Entonces, por las definiciones anteriores y los hechos básicos de la lógica (como las leyes de DeMorgan para los cuantificadores), la equivalencia $\forall \mathscr{M} (\mathscr{M}\models\varphi) \equiv \neg\exists \mathscr{M} (\mathscr{M}\models\neg\varphi)$ se mantiene como se desea. Lo mismo ocurre con el replanteamiento introducido por "en consecuencia" en el ejercicio, es decir $\exists \mathscr{M}(\mathscr{M}\models \varphi) \equiv \neg\forall(\mathscr{M}\models\neg\varphi)$ .

¿Tiene sentido? ¿Alguien ha detectado algún error o tiene ganas de sugerir mejoras de algún tipo?

Muy bien. Ahora el segundo ejercicio es donde las cosas se ponen más interesantes, al menos para mí, porque no entiendo del todo esta idea de correspondencia entre "válido" y "demostrable", que es el núcleo del teorema de completitud de Gödel.

Mirando lo que Wikipedia tiene que decir sobre el teorema, siento que básicamente entiendo el resultado, pero todavía no estoy seguro de cómo lo aplicaría en términos del segundo ejercicio.

Tomemos la primera parte del problema: todo lo que tengo es un algoritmo $\mathcal{A}$ que decide la satisfacción de $\varphi$ . El teorema de completitud establece una equivalencia entre la demostrabilidad sintáctica y la validez semántica. No consigo averiguar cómo cruzar el abismo que va de la satisfabilidad a la validez, ni encontrar la conexión lógica que necesitaría para utilizar el teorema para resolver mi problema.

Mientras buscaba preguntas similares antes de publicar, encontré este que ofrece algunos estímulos para la reflexión, pero que se ocupa de diferentes supuestos, a saber: un algoritmo que toma un $\varphi$ y devuelve $\varphi'$ tal que $\varphi$ es satisfacible si $\varphi'$ es válido. Veo que esto se acerca a lo que necesito, pero de nuevo no veo cómo adaptarlo a mis propósitos.

¿Alguien puede ofrecer una pista, una sugerencia o una indicación de algún tipo? Se lo agradecería mucho.

Answer 1

Tienes la idea correcta para la parte 1, pero es inusual usar la notación lógica que haces: $\neg$ , $\forall$ y $\exists$ son operadores lógicos, pero $\models$ es un símbolo metalógico; a los puristas no les gustará que los mezcles. Por lo tanto, es mejor utilizar los términos ingleses "some" y "all" y "not".

Para la parte 2: ¡aquí es donde se utiliza el resultado de la parte 1! En particular, para decidir si $\varphi$ es válido o no, puede decidir si $\neg \varphi$ es satisfacible o no: si $\neg \varphi$ es satisfacible, entonces $\varphi$ no es válido, pero si $\neg \varphi$ no es satisfacible, entonces $\varphi$ es válido. Y ahora sólo hay que combinar eso con el resultado de completitud de Godel (para ser precisos: el teorema de que un enunciado es demostrable si y sólo si es válido... la parte más difícil de "si" es el teorema de completitud): si $\varphi$ es válido, entonces es demostrable, y si $\varphi$ no es válido, entonces no es demostrable.

Así que para la primera parte: si tienes algoritmo $\mathcal{A}$ que puede averiguar si $\varphi$ es satisfactoria o no para cualquier $\varphi$ , entonces diseñe el algoritmo $\mathcal{B}$ que está tratando de averiguar si $\varphi$ es demostrable o no de la siguiente manera:

1. Toma en $\varphi$

2. Negar $\varphi$

3. Algoritmo de llamada $\mathcal{A}$ con $\neg \varphi$

4a. Si el algoritmo $\mathcal{A}$ dice que $\neg \varphi$ es satisfacible, entonces imprime ' $\varphi$ no es demostrable".

4b. Si el algoritmo $\mathcal{A}$ dice que $\neg \varphi$ no es satisfacible, entonces imprime ' $\varphi$ es demostrable".

Answer 2

Para mis propios fines, archivo aquí mi mejor intento de integrar, de manera compacta, todo lo que se mencionó en las respuestas a mi pregunta original. Cualquier comentario o crítica de cualquier tipo es siempre bienvenido. Gracias de nuevo a los colaboradores.

Definiciones. Una sentencia $\varphi$ es válido si es cierto en todos los modelos. Por el contrario, $\varphi$ es satisfaciendo si es verdadera en algún modelo.

Teorema de integridad con solidez. Una sentencia en lógica de primer orden es demostrable si y sólo si es válida.

Entonces, las respuestas a los problemas planteados anteriormente pueden darse de la siguiente manera:

1. Dejemos que $\mathscr{M}_x$ ser un modelo, $x\in\mathbb{N}$ . Sea $\varphi$ sea una sentencia en lógica de primer orden. Sea $P(x)$ sea el predicado " $\varphi$ es cierto en $\mathscr{M}_x$ ." Entonces $\forall x P(x) \equiv \neg \exists x P(x)$ y $\exists x P(x) \equiv \neg \forall x \neg P(x)$ por las definiciones anteriores y las leyes de De Morgan.

2. Supongamos que tenemos $\mathcal{A}$ . Sea $\mathcal{B}$ sea el algoritmo definido por el siguiente procedimiento. Paso 1: tomar $\varphi$ como entrada. Paso 2: negar $\varphi$ . Paso 3: llamar $\mathcal{A}$ con entrada $\neg\varphi$ , escrito $\mathcal{A}(\neg\varphi)$ . Paso 4, caso (a): Si $\mathcal{A}(\neg\varphi)$ vuelve " $\neg\varphi$ es satisfacible", entonces por las equivalencias anteriores $\varphi$ no es válida y por el teorema de completitud no es demostrable. Paso 4, caso (b): Si $\mathcal{A}(\neg\varphi)$ vuelve " $\neg\varphi$ no es satisfacible", entonces por las equivalencias anteriores $\varphi$ es válida y por el teorema de completitud es demostrable. Así, haciendo uso de $\mathcal{A}$ hemos obtenido $\mathcal{B}$ tal que $\mathcal{B}$ decide si $\varphi$ es demostrable o no. Por un argumento simétrico podemos obtener $\mathcal{A}$ si se da $\mathcal{B}$ .