Metateoría: síntesis y desafíos

Resumen

Esta clase cierra la unidad dedicada a la metateoría y, con ella, el contenido del curso. Reconstruye la cadena deductiva que va de la validez de los axiomas a la corrección del sistema; de los tres lemas de la negación conjunta al lema de Kalmár y a la completitud para premisas finitas; del lema de los dos testigos al teorema de compacidad y, por él, a la completitud fuerte; y de la forma clausal a la corrección y a la completitud refutacional del método de resolución, señalando en cada eslabón qué resultados usa y en qué clase se demuestra. Muestra cómo convergen en la coincidencia de $\vdash$ y $\models$ las tres partes anteriores del curso, el lenguaje, la deducción y la semántica, y qué aporta cada una a esa coincidencia; distingue lo que el curso demostró de lo que admitió y de lo que deja abierto. Repite en su evaluación de salida las destrezas de la evaluación de entrada, y termina con seis desafíos, de dificultad superior a la de los problemas de las clases, que exigen combinar los instrumentos de varias de ellas.

Objetivos de aprendizaje

Reconstruir el orden lógico de los resultados de la unidad, identificando los resultados anteriores en que se apoya cada uno y la clase en que se demuestra, y justificar el orden de la compacidad y la completitud fuerte.
Explicar cómo convergen el lenguaje, la deducción y la semántica en la coincidencia de $\vdash$ y $\models$ , y qué resultado de cada unidad del curso es indispensable para ella.
Distinguir lo que el curso demostró de lo que admitió (los esquemas de axiomas, las reglas primitivas, la inducción y la definición por recursión) y de lo que deja abierto (el costo de decidir la satisfacibilidad y la lógica con cuantificadores).
Resolver problemas que combinan las marcas, el lema de Kalmár, la sustitución uniforme, la compacidad y la resolución, usando en cada caso el lado fácil de la coincidencia.

Lo logrado en la unidad

La unidad se propuso comparar las dos relaciones que las unidades anteriores habían construido sobre la misma lengua, la deducibilidad $\Gamma \vdash \varphi$ y la consecuencia semántica $\Gamma \models \varphi$ , y demostrar que coinciden. El propósito se ha cumplido sin salvedades en los enunciados: ambas relaciones son la misma para todo conjunto de premisas, finito o infinito, y la resolución ofrece un tercer modo, igualmente correcto y completo, de decidir la consecuencia. Las salvedades están en los métodos, y cada una se declaró en su lugar: la completitud de la primera clase es constructiva pero no práctica, porque produce deducciones tan largas como la tabla; la compacidad asegura que existe una valoración, pero no enseña a encontrarla; y la resolución decide, pero su costo en el peor caso es una pregunta abierta. Con esas salvedades, el camino recorrido puede leerse como una sola cadena deductiva en cuatro tramos.

La corrección

La clase sobre la corrección y la completitud comenzó por fijar el vocabulario: el sistema es correcto si $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , y completo si vale el recíproco, en tres grados (débil, para conjuntos finitos y fuerte). Desmontó el argumento circular del artículo de origen, que obtenía la completitud «por la corrección» pasando de $\nvdash \chi$ a $\not\models \chi$ , paso que es la contrapositiva de la completitud débil, y mostró que ambas propiedades son independientes. Demostró después que toda instancia de A1, A2 y A3 es válida, suponiendo una valoración que la refutara y llegando, por la fila falsa de la implicación, a valores imposibles; y, por inducción fuerte sobre el número de líneas, la corrección, con un caso para los axiomas, otro para las premisas, el modus ponens semántico y, para la regla del reemplazo de la doble negación, la equivalencia $\theta \eqsem \neg\neg\theta$ con el teorema de reemplazo semántico. La propiedad que se transmite de línea en línea no es la validez, sino la satisfacción por una valoración fija que satisface las premisas, y por eso la corrección vale con premisas, también infinitas. De ella resultaron la consistencia de todo conjunto satisfacible, en particular la del sistema, y el método que la unidad de deducción no tenía: un contramodelo prueba que una deducción no existe.

Kalmár y la completitud finita

La misma clase demostró el recíproco en dos pasos. El primero es el lema de Kalmár: si las variables de $\varphi$ están entre $u_{1}, \ldots, u_{n}$ , entonces $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ para toda valoración $v$ , donde $\psi^{v}$ es $\psi$ si $v(\psi) = 1$ y $\neg\psi$ si no; el sistema deduce de cada fila lo que la fila dice de la fórmula. Su inducción sobre la complejidad tiene un solo caso compuesto, $(\alpha \downarrow \beta)$ , porque la negación conjunta es el único conector primitivo, y en él tres subcasos, que piden tres lemas del sistema: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , deducido con la introducción de la conjunción, la doble negación y dos aplicaciones de la regla RDN, y $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ y $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , deducidos con la introducción de la disyunción. El segundo paso elimina las premisas: si $\varphi$ es una tautología, se deduce de las premisas de las $2^{n}$ filas, y la prueba por casos elimina el literal de la última variable, después el de la penúltima, hasta llegar a $\vdash \varphi$ , la completitud débil. Con el teorema de deducción semántico y el recíproco del sintáctico, la completitud se extendió a conjuntos finitos de premisas; de donde, para premisas finitas, la deducción y la consecuencia coinciden, la equivalencia probada coincide con la semántica y la deducibilidad es decidible, porque la tabla responde por ella.

Compacidad y completitud fuerte

La clase sobre el teorema de compacidad afrontó el caso infinito, que el lema de Kalmár no alcanza, porque infinitas premisas no se descargan en una implicación. Demostró, sin mencionar deducción alguna, que un conjunto es satisfacible si y solo si lo es cada uno de sus subconjuntos finitos. Una sucesión de valores para $v_{1}, \ldots, v_{n}$ es buena si todo subconjunto finito del conjunto se satisface con alguna valoración que la prolonga; el lema de los dos testigos asegura que una sucesión buena se prolonga en una buena, porque si ninguna de las dos prolongaciones lo fuera, la unión de los dos testigos finitos contradiría que la sucesión es buena; y la valoración que resulta de preferir siempre el $1$ cuando es posible satisface cada fórmula, por el lema de coincidencia, porque cada fórmula tiene finitas variables. La construcción no necesita el axioma de elección, porque las variables están numeradas y cada paso tiene una regla. De la compacidad se siguieron sus formas equivalentes, la de la insatisfacibilidad y la de la consecuencia; de esta, de la completitud para premisas finitas y de la monotonía, la completitud fuerte; y de ella y de la corrección, la coincidencia completa: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ para todo $\Gamma$ , y un conjunto es consistente si y solo si es satisfacible. La clase advirtió que este orden no es una preferencia: obtener la compacidad de una completitud fuerte que aún no se tiene sería circular. Terminó con la coloración de grafos numerables, que traduce un problema infinito a un conjunto de fórmulas cuyas partes finitas son satisfacibles, y con los límites de lo que un conjunto de fórmulas puede expresar.

La resolución

La clase sobre el método de resolución cambió los conjuntos de fórmulas por conjuntos de cláusulas, cada una un conjunto finito de literales, con dos representaciones: la forma clausal, que tiene los mismos modelos, y la forma definicional, que introduce una variable nueva por cada subescritura, conserva solo la satisfacibilidad y crece como la fórmula, no como una potencia de dos. Sobre las cláusulas actúa una sola regla: de $C$ y $D$ , con $\ell \in C$ y $\ell^{*} \in D$ , se infiere $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , y una refutación es una derivación que llega a $\Box$ . La corrección se demostró como la del sistema, por inducción sobre la derivación y con el resolvente como consecuencia de sus premisas; la completitud refutacional, por inducción sobre el número de variables, con la eliminación de una variable, que conserva la satisfacibilidad y cuya demostración construye un modelo; y para conjuntos infinitos, otra vez con la compacidad. De ello resultó que $\Gamma \models \varphi$ si y solo si una forma clausal de $\Gamma \cup \{\neg\varphi\}$ tiene una refutación, y que la saturación, finita porque con $n$ variables no hay más de $4^{n}$ cláusulas, decide la satisfacibilidad sin tablas. La clase presentó el problema de la satisfacibilidad, cuyo costo en el peor caso nadie conoce, y dos casos que se deciden deprisa, las cláusulas de Horn y las de dos literales.

La figura siguiente reúne los cuatro tramos en una sola cadena. Cada nudo de la columna es un resultado, numerado según el orden lógico y unido por un arco a los eslabones anteriores que su demostración usa; alrededor flotan los apoyos, es decir, los principios y los instrumentos a los que la cadena recurre una y otra vez, cada uno unido con un trazo firme a los eslabones que se apoyan en él y con uno punteado al eslabón donde se establece, salvo los que proceden de las unidades anteriores, que se dibujan como anillos. Al pulsar un apoyo se destacan todos los eslabones que lo usan, y cada eslabón remite a la clase en que se demuestra. Obsérvese que la corrección y la compacidad, establecidas una en el primer tramo y otra en el tercero, sostienen todo lo que viene después de ellas, y que la inducción, en sus tres formas, es el apoyo más visitado de la unidad: sobre las líneas de una deducción, sobre la complejidad de una fórmula y sobre el número de variables de un conjunto de cláusulas.

Apoyos de la cadena

AInducción y recursión. Inducción fuerte sobre los naturales, inducción sobre la complejidad de las fórmulas, con el único caso compuesto $(\alpha \downarrow \beta)$ , y definición por recursión. Se demostraron en la primera unidad. Se admite sin demostración en esta unidad.
BSistema del curso. A1, A2 y A3, el modus ponens y la regla RDN; presunción, monotonía, modus ponens entre deducciones, carácter finito y $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . Se fijaron en la segunda unidad. Se admite sin demostración en esta unidad.
CTécnicas clásicas. Introducción de la conjunción y de la disyunción, doble negación, reducción al absurdo y prueba por casos: si $\Gamma \cup \{\psi\} \vdash \chi$ y $\Gamma \cup \{\neg\psi\} \vdash \chi$ , entonces $\Gamma \vdash \chi$ . Se demostraron en la segunda unidad. Se admite sin demostración en esta unidad.
DValoraciones y coincidencia. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; si dos valoraciones coinciden en $V(\varphi)$ , dan a $\varphi$ el mismo valor; la validez se decide con $2^{n}$ filas. Se demostraron en la tercera unidad. Se admite sin demostración en esta unidad.
EConsecuencia semántica. Fila falsa de la implicación, monotonía, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ si y solo si $\Gamma \cup \{\neg\varphi\}$ es insatisfacible, y el teorema de reemplazo semántico. Se demostraron en la tercera unidad. Se admite sin demostración en esta unidad.
FFormas conjuntivas. Lema del valor; toda fórmula equivale a una forma normal conjuntiva, que puede necesitar $2^{n}$ cláusulas; una disyunción de literales es válida si y solo si contiene un par complementario. Se demostraron en la tercera unidad. Se admite sin demostración en esta unidad.
GCorrección. Si $\Gamma \vdash \varphi$ , entonces $\Gamma \models \varphi$ , para todo conjunto $\Gamma$ ; un contramodelo prueba que una deducción no existe. Se establece en: 2. Corrección.
HCompacidad. Un conjunto de fórmulas es satisfacible si y solo si todo subconjunto finito suyo es satisfacible; de donde lo insatisfacible lo es ya en una parte finita. Se establece en: 11. Teorema de compacidad.

Tramo 1 La corrección
- Comprobar que toda instancia de los esquemas es válida sin construir su tabla.
- Demostrar la corrección por inducción fuerte sobre el número de líneas, con el caso de la regla del reemplazo de la doble negación.
- Probar con un contramodelo que una fórmula no se deduce, y obtener de la corrección la consistencia.
1. Validez de los axiomas. Toda instancia de A1, A2 y A3 es válida: una valoración que la refutara exigiría, por la fila falsa de la implicación, valores imposibles.
  Se apoya en: E (Consecuencia semántica). Se demuestra en: Corrección y completitud.
2. Corrección. Si $\Gamma \vdash \varphi$ , entonces $\Gamma \models \varphi$ , para todo $\Gamma$ : por inducción fuerte sobre el número de líneas, con un caso para los axiomas, otro para las premisas, el modus ponens semántico y, para la regla RDN, $\theta \eqsem \neg\neg\theta$ con el reemplazo semántico.
  Usa: 1. Validez de los axiomas. Se apoya en: A (Inducción y recursión), B (Sistema del curso), E (Consecuencia semántica). Se demuestra en: Corrección y completitud.
3. Consistencia y contramodelos. Todo conjunto satisfacible es consistente; el sistema es consistente y $\nvdash v_{1}$ ; si una valoración satisface $\Gamma$ y refuta $\varphi$ , entonces $\Gamma \nvdash \varphi$ , y la tabla certifica que lo que no es válido no es teorema.
  Se apoya en: G (Corrección), D (Valoraciones y coincidencia). Se demuestra en: Corrección y completitud.
Tramo 2 Kalmár y la completitud finita
- Deducir en el sistema los tres lemas de la negación conjunta, con la regla del reemplazo de la doble negación donde hace falta.
- Demostrar el lema de Kalmár por inducción sobre la complejidad, con un solo caso compuesto.
- Eliminar con la prueba por casos las premisas de las filas, y descargar premisas finitas con los dos teoremas de deducción.
- Decidir la deducibilidad, la equivalencia probada y la consistencia desde premisas finitas con la tabla.
1. Introducción de la negación conjunta. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ y $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : la conjunción de las negaciones es $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; la doble negación quita la exterior, y la regla RDN, las dos interiores.
  Se apoya en: B (Sistema del curso), C (Técnicas clásicas). Se demuestra en: Corrección y completitud.
2. Negación de la negación conjunta. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ y $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , porque $\neg(\alpha \downarrow \beta)$ es $(\alpha \vee \beta)$ y basta la introducción de la disyunción.
  Se apoya en: B (Sistema del curso), C (Técnicas clásicas). Se demuestra en: Corrección y completitud.
3. Lema de Kalmár. Si $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , entonces $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ para toda valoración $v$ ; el paso inductivo tiene un solo caso, $(\alpha \downarrow \beta)$ , con tres subcasos según los valores de $\alpha$ y de $\beta$ .
  Usa: 4. Introducción de la negación conjunta, 5. Negación de la negación conjunta. Se apoya en: A (Inducción y recursión), D (Valoraciones y coincidencia), B (Sistema del curso). Se demuestra en: Corrección y completitud.
4. Completitud débil. Si $\models \varphi$ , entonces $\vdash \varphi$ : el lema de Kalmár deduce $\varphi$ desde cada fila, y la prueba por casos elimina los literales de la última variable a la primera, con $2^{n}$ usos del lema y $2^{n} - 1$ de la prueba por casos.
  Usa: 6. Lema de Kalmár. Se apoya en: C (Técnicas clásicas). Se demuestra en: Corrección y completitud.
5. Completitud para premisas finitas. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : el teorema de deducción semántico lleva a una tautología, la completitud débil la deduce y el recíproco del teorema de deducción devuelve las premisas.
  Usa: 7. Completitud débil. Se apoya en: E (Consecuencia semántica), B (Sistema del curso). Se demuestra en: Corrección y completitud.
6. Coincidencia finita y decisión. Para $\Gamma$ finito, $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ , y $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; de donde la deducibilidad desde premisas finitas es decidible, por la tabla.
  Usa: 8. Completitud para premisas finitas. Se apoya en: G (Corrección), D (Valoraciones y coincidencia). Se demuestra en: Corrección y completitud.
Tramo 3 Compacidad y completitud fuerte
- Demostrar la compacidad fijando uno a uno los valores de las variables, con el invariante de las sucesiones buenas y el argumento de los dos testigos.
- Pasar entre la forma de la satisfacibilidad, la de la insatisfacibilidad y la de la consecuencia.
- Obtener la completitud fuerte de la compacidad, sin circularidad, y de ella la coincidencia de la consistencia con la satisfacibilidad.
- Codificar en conjuntos de fórmulas problemas sobre objetos infinitos y resolverlos con la compacidad.
1. Lema de los dos testigos. Si la sucesión $s$ de valores fijados es buena (todo subconjunto finito del conjunto se satisface con una valoración que la prolonga), lo es $(s, 1)$ o $(s, 0)$ : si ninguna lo fuera, la unión de los dos testigos finitos contradiría que $s$ es buena.
  Se apoya en: D (Valoraciones y coincidencia). Se demuestra en: El teorema de compacidad.
2. Teorema de compacidad. $\Gamma$ es satisfacible si y solo si todo subconjunto finito lo es: se fija $v_{n + 1}$ en $1$ si $(s_{n}, 1)$ es buena y en $0$ si no, y la valoración resultante satisface cada fórmula por el lema de coincidencia. No se necesita el axioma de elección, porque las variables están numeradas.
  Usa: 10. Lema de los dos testigos. Se apoya en: A (Inducción y recursión), D (Valoraciones y coincidencia). Se demuestra en: El teorema de compacidad.
3. Formas equivalentes. $\Gamma$ es insatisfacible si y solo si alguna parte finita lo es; $\Gamma \models \varphi$ si y solo si $\Gamma_{0} \models \varphi$ para algún $\Gamma_{0} \subseteq \Gamma$ finito; y esta última forma implica, a su vez, el teorema.
  Usa: 11. Teorema de compacidad. Se apoya en: E (Consecuencia semántica). Se demuestra en: El teorema de compacidad.
4. Completitud fuerte. Si $\Gamma \models \varphi$ , entonces $\Gamma \vdash \varphi$ , para todo $\Gamma$ : la forma de la consecuencia da un $\Gamma_{0}$ finito, la completitud para premisas finitas da $\Gamma_{0} \vdash \varphi$ , y la monotonía, $\Gamma \vdash \varphi$ .
  Usa: 8. Completitud para premisas finitas, 12. Formas equivalentes. Se apoya en: B (Sistema del curso). Se demuestra en: El teorema de compacidad.
5. La deducción es la consecuencia. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ para todo $\Gamma$ ; los teoremas son exactamente las tautologías, y un conjunto es consistente si y solo si es satisfacible.
  Usa: 13. Completitud fuerte. Se apoya en: G (Corrección). Se demuestra en: El teorema de compacidad.
6. Coloración de grafos numerables. Con una variable $x_{i,c}$ por cada vértice y color, y fórmulas que dicen que cada vértice tiene un color y uno solo y que los vecinos difieren, un grafo numerable admite una coloración con $k$ colores si la admite cada subgrafo finito.
  Se apoya en: H (Compacidad), F (Formas conjuntivas). Se demuestra en: El teorema de compacidad.
Tramo 4 La resolución
- Representar un conjunto de fórmulas como un conjunto de cláusulas, por la forma conjuntiva o por la definicional.
- Construir refutaciones sin eliminar dos pares complementarios en un paso.
- Demostrar la corrección y la completitud refutacional de la resolución, para conjuntos finitos y, con la compacidad, para cualesquiera.
- Decidir consecuencias por saturación y reconocer los casos que se deciden deprisa.
1. Forma clausal. Una cláusula es un conjunto finito de literales, satisfecho si alguno vale $1$ , y $\Box$ es insatisfacible; una forma clausal de $\Gamma$ tiene sus mismos modelos, y $\Gamma \models \varphi$ si y solo si una forma clausal de $\Gamma \cup \{\neg\varphi\}$ es insatisfacible.
  Se apoya en: F (Formas conjuntivas), E (Consecuencia semántica). Se demuestra en: El método de resolución.
2. Forma clausal definicional. Con una variable nueva por subescritura y sus cláusulas de definición, $T(\varphi)$ es equisatisfacible con $\varphi$ y tiene a lo sumo $4k + 1$ cláusulas de a lo sumo tres literales; las formas definicionales deciden la consecuencia desde premisas finitas.
  Usa: 16. Forma clausal. Se apoya en: A (Inducción y recursión), D (Valoraciones y coincidencia). Se demuestra en: El método de resolución.
3. Corrección de la resolución. $\{C, D\} \models R_{\ell}(C, D)$ , por casos sobre el valor de $\ell$ ; por inducción fuerte sobre la derivación, $S \models C$ para toda cláusula $C$ derivada de $S$ , y si $S$ tiene una refutación, es insatisfacible.
  Usa: 16. Forma clausal. Se apoya en: A (Inducción y recursión). Se demuestra en: El método de resolución.
4. Eliminación de una variable. $E_{p}(S)$ , que conserva las cláusulas sin $p$ ni $\neg p$ y añade los resolventes sobre $p$ , no contiene $p$ y es equisatisfacible con $S$ ; de un modelo suyo se obtiene uno de $S$ eligiendo el valor de $p$ .
  Usa: 18. Corrección de la resolución. Se apoya en: D (Valoraciones y coincidencia). Se demuestra en: El método de resolución.
5. Completitud refutacional finita. Todo conjunto finito e insatisfacible de cláusulas tiene una refutación, por inducción sobre el número de variables: se elimina la última y se insertan las premisas de cada resolvente.
  Usa: 19. Eliminación de una variable. Se apoya en: A (Inducción y recursión). Se demuestra en: El método de resolución.
6. Completitud refutacional. Un conjunto de cláusulas, finito o infinito, es insatisfacible si y solo si tiene una refutación; de donde $\Gamma \models \varphi$ si y solo si una forma clausal de $\Gamma \cup \{\neg\varphi\}$ tiene una refutación.
  Usa: 16. Forma clausal, 18. Corrección de la resolución, 20. Completitud refutacional finita. Se apoya en: H (Compacidad). Se demuestra en: El método de resolución.
7. La saturación decide. Con $n$ variables, el conjunto de las cláusulas derivadas tiene a lo sumo $4^{n}$ elementos; la saturación termina y decide la satisfacibilidad sin tablas, aunque no siempre más deprisa que ellas.
  Usa: 18. Corrección de la resolución, 20. Completitud refutacional finita. Se demuestra en: El método de resolución.

El final del curso. La cadena termina donde las dos caras del curso se reconocen como una sola relación y se dispone de un método para decidirla. Lo que queda abierto ya no es una pregunta sobre la lógica proposicional, sino sobre su costo y sobre su extensión a los cuantificadores.