Prueba de satisfacción dada la misma interpretación de la variable libre

Question

Estoy leyendo el libro de Enderton Introducción matemática a la lógica ( aquí un enlace a su segunda edición) y no estoy seguro de entender esta prueba, ¿alguien podría ayudar por favor?

Lo que no entiendo es cuál es la estructura de la prueba: concretamente sobre qué se hace la inducción y cuál es la hipótesis de inducción.

Me parece que la inducción se hace sobre la complejidad de la fórmula, es decir, el número de operadores lógicos. La fórmula atómica, que por definición no tiene operador lógico, se convierte naturalmente en el caso base, con $\lnot$ y $\to$ siendo los pasos inductivos.

El $\forall$ caso es el más confuso. Por suposición $s_1(x|d)$ está de acuerdo con $s_2(x|d)$ - que entiendo. Pero entonces Enderton cita la hipótesis inductiva como justificación de $\psi$ siendo satisfecha por $s_1(x|d)$ si es satisfecha por $s_2(x|d)$ - esto sólo parece posible si la inducción se hace sobre la complejidad de la fórmula, de lo contrario no veo cómo puede citar legítimamente la hipótesis aquí.

---

Satisfacción como se explica en el libro:

Answer 1

Como has dicho, la demostración del teorema 22A es por inducción sobre (la complejidad de) la fórmula $\varphi$ .

Hay dos sutilezas en esta prueba.

1. En el caso base, donde $\varphi$ es una fórmula atómica, la prueba utiliza el siguiente lema: dado un término $t$ , si $s_1$ y $s_2$ coinciden en todas las variables en $t$ entonces $\overline{s_1}(t) = \overline{s_2}(t)$ . Como se menciona en el texto, este lema debe demostrarse por separado, por inducción sobre la (complejidad del) término $t$ .

2. En el paso inductivo en el que $\varphi = \forall x \, \psi$ la hipótesis de inducción dice que si $s'_1$ y $s'_2$ son dos funciones de $V$ a $|\mathfrak{A}|$ que coinciden en todas las variables libres en $\psi$ entonces $\mathfrak{A}$ satisface $\psi$ con $s_1'$ si $\mathfrak{A}$ satisface $\psi$ con $s_2'$ . Lamentablemente, no se puede aplicar la hipótesis de inducción a $\psi$ con $s_1$ y $s_2$ porque $x$ no es una variable libre de $\varphi = \forall x \, \psi$ pero puede ser una variable libre en $\psi$ y no tenemos ninguna hipótesis sobre el comportamiento de $s_1$ y $s_2$ en $x$ (dicho de otro modo, la fórmula $\psi$ es menor que $\varphi$ pero las hipótesis no se satisfacen con $\psi$ con $s_1$ y $s_2$ ). Pero las funciones $s_1(x \mid d)$ y $s_2(x \mid d)$ coinciden en todas las variables libres de $\psi$ por lo que podemos aplicar la hipótesis de inducción a $\psi$ con $s_1(x \mid d)$ y $s_2(x \mid d)$ Por lo tanto, $\mathfrak{A}$ satisface $\psi$ con $s_1(x \mid d)$ si $\mathfrak{A}$ satisface $\psi$ con $s_2(x \mid d)$ . Por definición de satisfacción, esto significa que $\mathfrak{A}$ satisface $\varphi = \forall x \, \psi$ con $s_1$ si $\mathfrak{A}$ satisface $\varphi$ con $s_2$ .