Semántica: síntesis y desafíos

Resumen

Esta clase cierra la unidad dedicada a la semántica. Reconstruye la cadena deductiva que va de la extensión de una valoración a todas las fórmulas y del lema de coincidencia a la consecuencia, la equivalencia y sus dos teoremas de trabajo, el reemplazo y la sustitución uniforme; de ahí a las leyes de cualquier número de términos, a la completitud funcional y a los conjuntos de conectores, y de ahí a las formas normales, a su algoritmo y a los circuitos, señalando en cada eslabón qué resultados usa y en qué clase se demuestra. Distingue lo que la unidad demostró de lo que tomó de las anteriores, decide de tres maneras un argumento que el curso arrastra desde la primera unidad y explica por qué la pregunta que la unidad deja abierta, la de saber si lo verdadero en toda valoración coincide con lo deducible, conduce a la metateoría. 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.
Explicar cómo la extensión recursiva, el lema de coincidencia, el reemplazo semántico y las leyes generalizadas conducen a la completitud funcional, a la existencia de las formas normales y a la corrección y la terminación de su algoritmo.
Distinguir lo que la unidad demostró de lo que tomó de las anteriores y de lo que dejó a la metateoría, en particular la coincidencia de la consecuencia semántica con la deducibilidad y la compacidad.
Resolver problemas que combinan el cálculo con los valores, la consecuencia, la sustitución uniforme, los conjuntos de conectores, las formas normales y los circuitos.

Lo logrado en la unidad

La unidad se propuso dar significado a las fórmulas del lenguaje construido en la primera unidad, sin tocar el sistema deductivo de la segunda, y obtener de ese significado procedimientos para decidir las preguntas que la lógica hace sobre ellas: si una fórmula es válida, si es satisfacible, si se sigue de otras, si dice lo mismo que otra. El propósito se ha cumplido con unas pocas salvedades, cada una declarada en su lugar: la bivalencia y la veritativo-funcionalidad, que no se demuestran sino que se eligen, y cuyo precio mostró la clase sobre la formalización; la lectura única, la definición por recursión, la inducción y las abreviaturas oficiales, que se demostraron o se fijaron en la primera unidad y aquí se usan; y lo indispensable de los conjuntos y de las funciones, que se recordó donde hizo falta. Con esas salvedades, el camino recorrido puede leerse como una sola cadena deductiva en seis tramos, uno por clase.

El valor de una fórmula

La clase sobre la semántica de la lógica proposicional definió una valoración como una función de las variables en $\{0, 1\}$ y demostró, con el teorema de definición por recursión, que se extiende de un único modo a todas las fórmulas con una sola cláusula: $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ . De las abreviaturas oficiales calculó, sin estipular nada más, el valor de cada conector derivado, escrito como un polinomio de los valores de las componentes, y con ello la tabla de la implicación, que es aquí un teorema. Demostró por inducción sobre la complejidad el lema de coincidencia, del que se sigue que la tabla de verdad, con $2^{n}$ filas, contiene todo lo que las infinitas valoraciones dicen de una fórmula de $n$ variables; definió la satisfacción, la validez, la satisfacibilidad, la contradicción y la contingencia, precisó que $\not\models \varphi$ dice que $\varphi$ no es válida y no que sea contradictoria, fijó $\top := (v_{1} \rightarrow v_{1})$ y $\bot := \neg\top$ , y obtuvo la decidibilidad de la validez y de la satisfacibilidad, a un costo exponencial que la búsqueda dirigida de una valoración refutadora atenúa sin eliminar.

Consecuencia y equivalencia

La clase sobre consecuencia y equivalencia semántica definió la consecuencia desde un conjunto de premisas, finito o infinito, y demostró que tiene las propiedades estructurales de la deducción (reflexividad, monotonía, corte y transitividad), con demostraciones que recorren valoraciones en lugar de manipular líneas. El teorema de deducción semántico, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , se redujo a la única fila falsa de la implicación, y la consecuencia se redujo a la insatisfacibilidad: $\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\}$ es insatisfacible. La equivalencia semántica, definida como la igualdad de los valores, resultó coincidir con la consecuencia mutua y con la validez de la doble implicación. Sus dos teoremas de trabajo se demostraron por inducción sobre la complejidad: el reemplazo de una aparición de una subfórmula por otra equivalente, con el caso de la aparición total, que el artículo de origen omitía, y la sustitución uniforme de variables por fórmulas cualesquiera, que conserva la validez, la equivalencia y la consecuencia. Con ellos, las leyes del catálogo, verificadas como identidades entre polinomios, se aplican en cualquier lugar de cualquier fórmula y se encadenan.

Leyes de cualquier número de términos

La clase sobre las leyes generalizadas de De Morgan y de distribución definió por recursión, asociando por la izquierda, la conjunción y la disyunción de $n$ fórmulas, y demostró por inducción sobre el número de términos el lema del valor, que dice que una conjunción es verdadera si y solo si lo son todos sus términos y una disyunción si y solo si lo es alguno. Con él y con la compatibilidad de los conectores con la equivalencia, obtuvo la asociatividad generalizada, que se demostró con una cadena de equivalencias para que valga también para la equivalencia probada, la independencia del orden y de las repeticiones, las leyes de De Morgan generalizadas y la distributividad generalizada, cuya inducción sobre dos índices se organizó de modo que la hipótesis abarque todas las longitudes de la segunda lista; la ley dual se obtuvo por De Morgan, sin repetir la doble inducción.

Funciones de verdad

La clase sobre la completitud funcional recorrió el camino inverso, de la tabla a la fórmula. Contó las funciones de verdad de $n$ argumentos, $2^{2^{n}}$ , mostró que cada fórmula representa exactamente una y que dos fórmulas son equivalentes si y solo si representan la misma, y demostró el teorema de completitud funcional: la conjunción de una fila es verdadera exactamente en su fila, y la disyunción de las conjunciones de las filas en que la función vale $1$ la representa. Como esa fórmula es una cadena de círculos y discos, la negación conjunta basta por sí sola; con el criterio de la negación conjunta, también bastan $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ y la negación alternativa; y con el principio del cierre, que todas las fórmulas de $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ conservan el $1$ , de modo que ese conjunto no basta.

Formas normales

La clase sobre las formas normales eligió, en cada clase de fórmulas equivalentes, representantes de forma fija. Definió los literales, las cláusulas y las conjunciones elementales, y demostró que la negación de una forma normal equivale a su dual, que cambia cada conjunción por una disyunción y cada literal por su opuesto. Construyó desde la tabla las formas canónicas, únicas una vez fijadas las variables, y demostró la existencia de ambas formas normales de dos maneras: por la tabla, como corolario de la completitud funcional, y por inducción sobre la complejidad, con el único caso de la negación conjunta, que equivale a la conjunción de las negaciones de sus componentes, y con una hipótesis que pide a la vez las dos formas, porque la negación las intercambia. Mostró, por último, que la validez de una forma conjuntiva y la satisfacibilidad de una disyuntiva se leen a simple vista en sus pares complementarios.

El algoritmo y los circuitos

La clase sobre el algoritmo de las formas normales y sus aplicaciones convirtió la segunda demostración de existencia en un procedimiento que actúa sobre las escrituras: eliminar los conectores distintos de $\neg$ , $\wedge$ y $\vee$ , llevar las negaciones hasta las variables y distribuir. Demostró su corrección con el reemplazo en una escritura, que adapta el teorema de reemplazo a las abreviaturas, y su terminación con tres medidas que bajan en cada paso, la última de las cuales lee la conjunción como un producto; demostró también que la forma conjuntiva de $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ tiene necesariamente $2^{n}$ cláusulas, de modo que el crecimiento no es un defecto del algoritmo. Obtuvo después las formas normales de una caja negra desde su tabla, las acortó fusionando filas vecinas y las convirtió en circuitos de interruptores, cuya conducción es el valor de su fórmula.

La figura siguiente reúne los seis tramos en una sola cadena. Cada nudo de la columna es una definición o 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 esta cadena no demuestra (la lectura única con la recursión, la inducción y las abreviaturas oficiales, de la primera unidad), 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 inducción y los valores de los conectores son los apoyos más visitados de la unidad, y que el lema del valor, aunque se demuestra en la tercera clase, sostiene casi todo lo que las tres últimas dicen de las conjunciones y las disyunciones.

Apoyos de la cadena

ALectura única y recursión. Si $\sigI\varphi\psi = \sigI\varphi'\psi'$ , con las cuatro cadenas fórmulas, entonces $\varphi = \varphi'$ y $\psi = \psi'$ ; de donde una regla que calcula el valor de $\sigI\varphi\psi$ a partir de $\varphi$ , de $\psi$ y de sus valores define una sola función sobre las fórmulas. Se demostró en la primera unidad. Se admite sin demostración en esta unidad.
BInducción. Simple y fuerte sobre los naturales, y sobre la complejidad de las fórmulas, cuyos únicos casos son las variables y la negación conjunta $(\varphi \downarrow \psi)$ . Se demostró en la primera unidad. Se admite sin demostración en esta unidad.
CAbreviaturas oficiales. $\neg\varphi := (\varphi \downarrow \varphi)$ , $(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)$ , $(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)$ , $(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)$ , $(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$ y $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$ . Se fijaron en la primera unidad. Se admite sin demostración en esta unidad.
DValores de los conectores. Con $a = v(\varphi)$ y $b = v(\psi)$ : $v(\neg\varphi) = 1 - a$ , $v((\varphi \vee \psi)) = a + b - ab$ , $v((\varphi \wedge \psi)) = ab$ , $v((\varphi \rightarrow \psi)) = 1 - a(1 - b)$ , $v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b)$ y $v((\varphi \veebar \psi)) = a + b - 2ab$ , donde $a^{2} = a$ . Se establece en: 1. Extensión de una valoración.
ELema de coincidencia. Si dos valoraciones coinciden en las variables de $\varphi$ , dan a $\varphi$ el mismo valor; por eso la tabla de $2^{n}$ filas lo dice todo. Se establece en: 2. Lema de coincidencia y tablas.
FReemplazo semántico. Si $\theta \eqsem \theta'$ y $\chi'$ resulta de reemplazar en $\chi$ una aparición de $\theta$ por $\theta'$ , entonces $\chi \eqsem \chi'$ . Se establece en: 7. Teorema de reemplazo semántico.
GLeyes de la equivalencia. Doble negación, idempotencia, conmutatividad, asociatividad, distributividad, De Morgan, absorción, identidad, dominación, tercero excluido y no contradicción, para fórmulas cualesquiera. Se establece en: 9. Leyes de la equivalencia.
HLema del valor. $v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1$ si y solo si $v(\varphi_i) = 1$ para todo $i$ ; $v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1$ si y solo si $v(\varphi_i) = 1$ para algún $i$ . Se establece en: 10. Lema del valor y compatibilidad.

Tramo 1 El valor de una fórmula
- Calcular el valor de una fórmula con la cláusula de la negación conjunta y deducir de las abreviaturas el de cada conector derivado.
- Demostrar el lema de coincidencia y justificar con él que una tabla de $2^{n}$ filas basta.
- Clasificar fórmulas y conjuntos sin confundir $\not\models \varphi$ con la contradicción, y decidir la validez buscando una valoración que refute.
1. Extensión de una valoración. Cada valoración $v$ se extiende de un único modo a todas las fórmulas con la cláusula $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ ; desplegando las abreviaturas se calcula el valor de $\neg$ , $\vee$ , $\wedge$ , $\rightarrow$ , $\leftrightarrow$ y $\veebar$ .
  Se apoya en: A (Lectura única y recursión), C (Abreviaturas oficiales). Se demuestra en: Semántica de la lógica proposicional.
2. Lema de coincidencia y tablas. Si $v$ y $v'$ coinciden en $V(\varphi)$ , entonces $v(\varphi) = v'(\varphi)$ , por inducción sobre la complejidad; de donde los valores de $\varphi$ bajo todas las valoraciones son exactamente los de las $2^{n}$ filas de su tabla.
  Usa: 1. Extensión de una valoración. Se apoya en: B (Inducción). Se demuestra en: Semántica de la lógica proposicional.
3. Clasificación y decisión. Toda fórmula es exactamente una de tres cosas: válida, contingente o contradicción; $\varphi$ es válida si y solo si $\neg\varphi$ es una contradicción, y es una contradicción si y solo si $\models \neg\varphi$ . $\top$ y el tercero excluido son válidos, $\bot$ es una contradicción, y la validez y la satisfacibilidad se deciden recorriendo las filas.
  Se apoya en: D (Valores de los conectores), E (Lema de coincidencia). Se demuestra en: Semántica de la lógica proposicional.
Tramo 2 Consecuencia y equivalencia
- Decidir consecuencias desde conjuntos finitos o infinitos, exhibiendo un contramodelo o demostrando que no existe.
- Aplicar el teorema de deducción semántico y la reducción de la consecuencia a la insatisfacibilidad.
- Distinguir el reemplazo de una aparición de la sustitución uniforme, y demostrar ambos por inducción sobre la complejidad.
- Establecer equivalencias por cadenas, nombrando correctamente cada ley.
1. Consecuencia y sus propiedades. $\Gamma \models \varphi$ si toda valoración que satisface $\Gamma$ satisface $\varphi$ ; $\emptyset \models \varphi$ si y solo si $\models \varphi$ ; valen la reflexividad, la monotonía, el corte y la transitividad, y un conjunto insatisfacible tiene por consecuencia toda fórmula.
  Usa: 3. Clasificación y decisión. Se demuestra en: Consecuencia y equivalencia semántica.
2. Deducción semántica e insatisfacibilidad. $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , por la única fila falsa de la implicación; $\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots))$ ; y $\Gamma \models \varphi$ si y solo si $\Gamma \cup \{\neg\varphi\}$ es insatisfacible.
  Usa: 4. Consecuencia y sus propiedades. Se apoya en: D (Valores de los conectores). Se demuestra en: Consecuencia y equivalencia semántica.
3. Equivalencia semántica. $\varphi \eqsem \psi$ si y solo si $\varphi \models \psi$ y $\psi \models \varphi$ , si y solo si $\models (\varphi \leftrightarrow \psi)$ ; la equivalencia es reflexiva, simétrica y transitiva, y dos fórmulas equivalentes son intercambiables como premisas y como conclusiones.
  Usa: 4. Consecuencia y sus propiedades. Se apoya en: D (Valores de los conectores). Se demuestra en: Consecuencia y equivalencia semántica.
4. Teorema de reemplazo semántico. Si $\theta \eqsem \theta'$ , reemplazar en $\chi$ una aparición de $\theta$ por $\theta'$ , incluida la aparición total, da una fórmula equivalente a $\chi$ ; y lo mismo sustituir a la vez todas las apariciones.
  Usa: 1. Extensión de una valoración, 6. Equivalencia semántica. Se apoya en: A (Lectura única y recursión), B (Inducción). Se demuestra en: Consecuencia y equivalencia semántica.
5. Sustitución uniforme. Si $w(v_n) = v(\sigma(v_n))$ , entonces $v(\sigma(\chi)) = w(\chi)$ ; de donde, si $\models \chi$ , también $\models \sigma(\chi)$ , y la sustitución conserva la equivalencia y la consecuencia, pero no la satisfacibilidad ni la contingencia.
  Usa: 1. Extensión de una valoración, 4. Consecuencia y sus propiedades, 6. Equivalencia semántica. Se apoya en: A (Lectura única y recursión), B (Inducción). Se demuestra en: Consecuencia y equivalencia semántica.
6. Leyes de la equivalencia. Las leyes del catálogo se verifican como identidades entre polinomios con $a^{2} = a$ ; con el reemplazo y la transitividad, se aplican a subfórmulas y se encadenan.
  Usa: 3. Clasificación y decisión, 6. Equivalencia semántica. Se apoya en: D (Valores de los conectores), F (Reemplazo semántico). Se demuestra en: Consecuencia y equivalencia semántica.
Tramo 3 Leyes de cualquier número de términos
- Desplegar conjunciones y disyunciones de $n$ términos como cadenas asociadas por la izquierda y calcular su valor.
- Demostrar por inducción sobre el número de términos la asociatividad generalizada, la independencia del orden y las leyes de De Morgan generalizadas.
- Demostrar la distributividad generalizada con una inducción sobre dos índices, y contar los términos que produce.
1. Lema del valor y compatibilidad. Si $\alpha \eqsem \alpha'$ y $\beta \eqsem \beta'$ , entonces $\neg\alpha \eqsem \neg\alpha'$ , $(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')$ y $(\alpha \vee \beta) \eqsem (\alpha' \vee \beta')$ ; una conjunción de $n$ términos vale $1$ si y solo si todos valen $1$ , una disyunción si y solo si alguno vale $1$ , y términos equivalentes dan conjunciones y disyunciones equivalentes.
  Usa: 6. Equivalencia semántica. Se apoya en: D (Valores de los conectores), B (Inducción). Se demuestra en: Leyes generalizadas de De Morgan y de distribución.
2. Asociatividad y orden. La conjunción de las conjunciones de dos listas equivale a la de su concatenación, y toda agrupación equivale a la asociada por la izquierda; dos listas con los mismos términos dan conjunciones y disyunciones equivalentes, cualesquiera que sean el orden y las repeticiones.
  Se apoya en: H (Lema del valor), G (Leyes de la equivalencia), B (Inducción). Se demuestra en: Leyes generalizadas de De Morgan y de distribución.
3. De Morgan generalizadas. $\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i$ y $\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i$ , aplicando la ley binaria a la última unión y la hipótesis a lo que queda dentro.
  Se apoya en: H (Lema del valor), G (Leyes de la equivalencia), B (Inducción). Se demuestra en: Leyes generalizadas de De Morgan y de distribución.
4. Distributividad generalizada. $\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j)$ , con $nm$ términos en orden lexicográfico; y su dual, que reparte la disyunción de dos conjunciones, por De Morgan.
  Usa: 11. Asociatividad y orden, 12. De Morgan generalizadas. Se apoya en: H (Lema del valor), G (Leyes de la equivalencia), B (Inducción). Se demuestra en: Leyes generalizadas de De Morgan y de distribución.
Tramo 4 Funciones de verdad
- Contar las funciones de verdad y decidir la equivalencia comparando las funciones que representan dos fórmulas.
- Construir la fórmula de una tabla y escribir cualquier función con la sola negación conjunta.
- Demostrar que un conjunto de conectores es adecuado con el criterio de la negación conjunta, o que no lo es con una propiedad que sus fórmulas conservan.
1. Funciones de verdad. Hay $2^{2^{n}}$ funciones de verdad de $n$ argumentos; una fórmula con variables entre $v_1, \ldots, v_n$ representa exactamente una, $f_\varphi$ , y $\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi$ .
  Usa: 6. Equivalencia semántica. Se apoya en: E (Lema de coincidencia). Se demuestra en: Completitud funcional.
2. Completitud funcional. La conjunción de una fila vale $1$ exactamente en su fila; la disyunción de las conjunciones de las filas en que $f$ vale $1$ , o $(v_{1} \wedge \neg v_{1})$ si no hay ninguna, representa $f$ ; y toda fórmula equivale a la fórmula de su tabla.
  Usa: 14. Funciones de verdad. Se apoya en: H (Lema del valor), D (Valores de los conectores). Se demuestra en: Completitud funcional.
3. Conjuntos adecuados e inadecuados. La negación conjunta basta, porque las abreviaturas se despliegan; si las fórmulas de $K$ expresan el valor $(1 - a)(1 - b)$ , $K$ es adecuado, como $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ y $\{\uparrow\}$ ; las fórmulas de $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ valen $1$ cuando todas las variables valen $1$ , y ese conjunto no es adecuado.
  Usa: 15. Completitud funcional. Se apoya en: C (Abreviaturas oficiales), B (Inducción), D (Valores de los conectores). Se demuestra en: Completitud funcional.
Tramo 5 Formas normales
- Reconocer literales, cláusulas y formas normales, distinguiendo la forma de la cadena de su significado.
- Construir las formas canónicas desde la tabla y demostrar su unicidad.
- Demostrar por inducción la existencia de las formas normales, con la hipótesis que pide ambas.
- Decidir a simple vista la validez de una forma conjuntiva y la satisfacibilidad de una disyuntiva.
1. Literales y dualidad. $\neg\ell \eqsem \ell^{*}$ ; una conjunción elemental es satisfacible si y solo si no contiene un par complementario, y una cláusula es válida si y solo si lo contiene; la negación de una forma normal equivale a su dual, de modo que la forma conjuntiva de $\varphi$ es la dual de la disyuntiva de $\neg\varphi$ .
  Usa: 12. De Morgan generalizadas. Se apoya en: G (Leyes de la equivalencia), F (Reemplazo semántico), H (Lema del valor). Se demuestra en: Formas normales.
2. Formas canónicas. Si $\varphi$ es satisfacible, equivale a su forma canónica disyuntiva, y si no es válida, a la conjuntiva; dos formas canónicas son equivalentes si y solo si son la misma cadena, y dos fórmulas son equivalentes si y solo si tienen la misma forma canónica.
  Usa: 15. Completitud funcional, 17. Literales y dualidad. Se apoya en: H (Lema del valor), E (Lema de coincidencia). Se demuestra en: Formas normales.
3. Existencia por inducción. $(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)$ ; las formas normales se conservan al conjuntar y al disyuntar, la disyuntiva de una conjunción y la conjuntiva de una disyunción por la distributividad generalizada; por inducción, con la hipótesis de ambas formas, toda fórmula tiene una forma disyuntiva y una conjuntiva.
  Usa: 17. Literales y dualidad, 11. Asociatividad y orden, 13. Distributividad generalizada. Se apoya en: B (Inducción), F (Reemplazo semántico). Se demuestra en: Formas normales.
4. Lo que se ve a simple vista. Una forma conjuntiva es válida si y solo si cada cláusula contiene un par complementario; una forma disyuntiva es satisfacible si y solo si alguna conjunción elemental no contiene ninguno.
  Usa: 17. Literales y dualidad. Se apoya en: H (Lema del valor). Se demuestra en: Formas normales.
Tramo 6 El algoritmo y los circuitos
- Aplicar el algoritmo de reescritura y elegir la eliminación de la doble implicación que conviene.
- Demostrar su corrección y su terminación, y explicar por qué la forma conjuntiva puede crecer exponencialmente.
- Obtener y simplificar las formas normales de una caja negra, y diseñar con ellas circuitos de interruptores.
1. Corrección y terminación del algoritmo. Cambiar una subescritura por otra equivalente da una escritura equivalente; cada regla es una equivalencia, y una escritura irreducible es una forma normal agrupada de algún modo; las medidas $M_1$ , $M_2$ , con $M_2(\neg\varphi) = 2^{M_2(\varphi)}$ , y $M_3$ , con $M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi)$ , bajan en cada paso.
  Usa: 19. Existencia por inducción, 11. Asociatividad y orden. Se apoya en: G (Leyes de la equivalencia), D (Valores de los conectores), B (Inducción). Se demuestra en: El algoritmo de las formas normales y sus aplicaciones.
2. Crecimiento exponencial. $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ equivale a una forma conjuntiva de $2^{n}$ cláusulas, y toda forma conjuntiva equivalente tiene al menos $2^{n}$ cláusulas no válidas.
  Usa: 19. Existencia por inducción, 17. Literales y dualidad. Se apoya en: H (Lema del valor). Se demuestra en: El algoritmo de las formas normales y sus aplicaciones.
3. Filas vecinas y circuitos. $(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa$ y su dual; un circuito de serie y paralelo conduce en el estado $v$ si y solo si $v(\varphi_C) = 1$ , y toda función de verdad la realiza algún circuito.
  Usa: 15. Completitud funcional, 18. Formas canónicas, 17. Literales y dualidad, 11. Asociatividad y orden. Se apoya en: G (Leyes de la equivalencia), F (Reemplazo semántico), D (Valores de los conectores), B (Inducción). Se demuestra en: El algoritmo de las formas normales y sus aplicaciones.

Hacia la metateoría. La cadena se detiene donde la semántica alcanza un procedimiento para cada pregunta sobre las fórmulas. Queda por saber si lo que es verdadero en toda valoración es exactamente lo que se deduce en el sistema: la unidad siguiente comparará ambas nociones.