Semântica: síntese e desafios

Resumo

Esta aula fecha a unidade dedicada à semântica. Reconstrói a cadeia dedutiva que vai da extensão de uma valoração a todas as fórmulas e do lema de coincidência à consequência, à equivalência e aos seus dois teoremas de trabalho, a substituição e a substituição uniforme; dali às leis para qualquer número de termos, à completude funcional e aos conjuntos de conectivos, e dali às formas normais, ao seu algoritmo e aos circuitos, indicando em cada elo que resultados usa e em que aula se demonstra. Distingue o que a unidade demonstrou do que tomou das anteriores, decide de três maneiras um argumento que o curso traz desde a primeira unidade e explica por que a pergunta que a unidade deixa aberta, a de saber se o verdadeiro em toda valoração coincide com o derivável, conduz à metateoria. Repete na sua avaliação de saída as habilidades da avaliação de entrada e termina com seis desafios, mais difíceis que os problemas das aulas, que exigem combinar as ferramentas de várias delas.

Objetivos de aprendizagem

Reconstruir a ordem lógica dos resultados da unidade, identificando os resultados anteriores em que cada um se apoia e a aula em que se demonstra.
Explicar como a extensão recursiva, o lema de coincidência, a substituição semântica e as leis generalizadas conduzem à completude funcional, à existência das formas normais e à correção e à terminação do seu algoritmo.
Distinguir o que a unidade demonstrou do que tomou das anteriores e do que deixou para a metateoria, em particular a coincidência da consequência semântica com a derivabilidade e a compacidade.
Resolver problemas que combinam o cálculo com valores, a consequência, a substituição uniforme, os conjuntos de conectivos, as formas normais e os circuitos.

O que a unidade alcançou

A unidade propôs-se dar significado às fórmulas da linguagem construída na primeira unidade, sem tocar no sistema dedutivo da segunda, e obter desse significado procedimentos para decidir as perguntas que a lógica faz sobre elas: se uma fórmula é válida, se é satisfatível, se se segue de outras, se diz o mesmo que outra. O propósito foi cumprido com algumas reservas, cada uma declarada no seu lugar: a bivalência e a vero-funcionalidade, que não se demonstram mas se escolhem, e cujo preço a aula sobre a formalização mostrou; a leitura única, a definição por recursão, a indução e as abreviaturas oficiais, que se demonstraram ou se fixaram na primeira unidade e aqui se usam; e os fatos indispensáveis sobre conjuntos e funções, que foram recordados onde fizeram falta. Com essas reservas, o caminho percorrido pode ler-se como uma única cadeia dedutiva em seis trechos, um por aula.

O valor de uma fórmula

A aula sobre a semântica da lógica proposicional definiu uma valoração como uma função das variáveis em $\{0, 1\}$ e demonstrou, com o teorema de definição por recursão sobre as fórmulas, que ela se estende de maneira única a todas as fórmulas com uma só cláusula: $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ . A partir das abreviaturas oficiais calculou, sem estipular nada mais, o valor de cada conectivo definido, escrito como um polinômio nos valores das componentes, e com ele a tabela da implicação, que aqui é um teorema. Demonstrou por indução na complexidade o lema de coincidência, do qual se segue que a tabela de verdade, com $2^{n}$ linhas, contém tudo o que as infinitas valorações dizem sobre uma fórmula com $n$ variáveis; definiu a satisfação, a validade, a satisfatibilidade, a contradição e a contingência, precisou que $\not\models \varphi$ diz que $\varphi$ não é válida e não que é contraditória, fixou $\top := (v_{1} \rightarrow v_{1})$ e $\bot := \neg\top$ , e obteve a decidibilidade da validade e da satisfatibilidade, com um custo exponencial que a busca dirigida de uma valoração que falsifique reduz sem eliminá-lo.

Consequência e equivalência

A aula sobre consequência e equivalência semânticas definiu a consequência a partir de um conjunto de premissas, finito ou infinito, e demonstrou que ela tem as propriedades estruturais da dedução (reflexividade, monotonicidade, corte e transitividade), com provas que passam pelas valorações em vez de manipular linhas. O teorema da dedução semântico, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , reduziu-se à única linha falsa da implicação, e a consequência reduziu-se à insatisfatibilidade: $\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\}$ é insatisfatível. A equivalência semântica, definida como igualdade de valores, mostrou coincidir com a consequência mútua e com a validade do bicondicional. Os seus dois teoremas de trabalho demonstraram-se por indução na complexidade: a substituição de uma ocorrência de uma subfórmula por outra equivalente, com o caso da ocorrência total, que não pode ser omitido, e a substituição uniforme de variáveis por fórmulas quaisquer, que preserva a validade, a equivalência e a consequência. Com eles, as leis do catálogo, verificadas como identidades entre polinômios, aplicam-se em qualquer lugar de qualquer fórmula e podem ser encadeadas.

Leis para qualquer número de termos

A aula sobre as leis generalizadas de De Morgan e distributivas definiu por recursão, associando à esquerda, a conjunção e a disjunção de $n$ fórmulas, e demonstrou por indução no número de termos o lema do valor, que diz que uma conjunção é verdadeira se e somente se todos os seus termos o são e uma disjunção se e somente se algum o é. Com ele e com a compatibilidade dos conectivos com a equivalência, obteve a associatividade generalizada, que se demonstrou com uma cadeia de equivalências para que valha também para a equivalência demonstrável, a independência da ordem e das repetições, as leis de De Morgan generalizadas e a distributividade generalizada, cuja indução em dois índices se organizou para que a hipótese de indução cubra todos os comprimentos da segunda lista; a lei dual obteve-se por De Morgan, sem repetir a indução dupla.

Funções de verdade

A aula sobre a completude funcional percorreu o caminho inverso, da tabela à fórmula. Contou as funções de verdade de $n$ argumentos, $2^{2^{n}}$ , mostrou que cada fórmula representa exatamente uma delas e que duas fórmulas são equivalentes se e somente se representam a mesma, e demonstrou o teorema de completude funcional: a conjunção de uma linha é verdadeira exatamente na sua linha, e a disjunção das conjunções das linhas em que a função vale $1$ a representa. Como essa fórmula é uma cadeia de círculos e discos, a negação conjunta basta por si só; com o critério da negação conjunta, também bastam $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ e a negação alternativa; e com o princípio do fecho demonstrou que todas as fórmulas de $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ preservam o $1$ , de modo que esse conjunto não basta.

Formas normais

A aula sobre as formas normais escolheu, em cada classe de fórmulas equivalentes, representantes de forma fixa. Definiu os literais, as cláusulas e as conjunções elementares, e demonstrou que a negação de uma forma normal é equivalente à sua dual, que troca cada conjunção por uma disjunção e cada literal pelo seu oposto. Construiu a partir da tabela as formas canônicas, únicas uma vez fixadas as variáveis, e demonstrou a existência das duas formas normais de duas maneiras: pela tabela, como corolário da completude funcional, e por indução na complexidade, com o único caso da negação conjunta, que equivale à conjunção das negações das suas componentes, e com uma hipótese de indução que pede as duas formas ao mesmo tempo, porque a negação as intercambia. Mostrou, por fim, que a validade de uma forma conjuntiva e a satisfatibilidade de uma disjuntiva se leem à primeira vista nos seus pares complementares.

O algoritmo e os circuitos

A aula sobre o algoritmo das formas normais e as suas aplicações converteu a segunda prova de existência num procedimento que atua sobre escritas: eliminar os conectivos distintos de $\neg$ , $\wedge$ e $\vee$ , baixar as negações até as variáveis e distribuir. Demonstrou a sua correção com a substituição numa escrita, que adapta o teorema da substituição às abreviaturas, e a sua terminação com três medidas que decrescem a cada passo, a última das quais lê a conjunção como um produto; demonstrou, além disso, que a forma conjuntiva de $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ tem forçosamente $2^{n}$ cláusulas, de modo que o crescimento não é um defeito do algoritmo. Depois obteve as formas normais de uma caixa-preta a partir da sua tabela, encurtou-as fundindo linhas vizinhas e converteu-as em circuitos de interruptores, cuja condução é o valor da sua fórmula.

A figura seguinte reúne os seis trechos numa única cadeia. Cada nó da coluna é uma definição ou um resultado, numerado segundo a ordem lógica e unido por um arco aos elos anteriores que a sua prova usa; à sua volta flutuam os apoios, isto é, os princípios e as ferramentas aos quais a cadeia recorre uma e outra vez, cada um unido por uma linha cheia aos elos que se apoiam nele e por uma pontilhada ao elo onde se estabelece, salvo os que esta cadeia não demonstra (a leitura única com a recursão, a indução e as abreviaturas oficiais, da primeira unidade), que se desenham como anéis. Clicar num apoio destaca todos os elos que o usam, e cada elo remete à aula em que se demonstra. Note-se que a indução e os valores dos conectivos são os apoios mais visitados da unidade, e que o lema do valor, embora se demonstre na terceira aula, sustenta quase tudo o que as três últimas dizem sobre conjunções e disjunções.

Apoios da cadeia

ALeitura única e recursão. Se $\sigI\varphi\psi = \sigI\varphi'\psi'$ , com as quatro cadeias fórmulas, então $\varphi = \varphi'$ e $\psi = \psi'$ ; por isso, uma regra que calcula o valor de $\sigI\varphi\psi$ a partir de $\varphi$ , de $\psi$ e dos seus valores define uma única função sobre as fórmulas. Demonstrou-se na primeira unidade. Admitido sem demonstração nesta unidade.
BIndução. Simples e forte sobre os naturais, e na complexidade das fórmulas, cujos únicos casos são as variáveis e a negação conjunta $(\varphi \downarrow \psi)$ . Demonstrou-se na primeira unidade. Admitido sem demonstração nesta unidade.
CAbreviaturas oficiais. $\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))$ e $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$ . Fixaram-se na primeira unidade. Admitido sem demonstração nesta unidade.
DValores dos conectivos. Com $a = v(\varphi)$ e $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)$ e $v((\varphi \veebar \psi)) = a + b - 2ab$ , onde $a^{2} = a$ . Estabelecido em: 1. Extensão de uma valoração.
ELema de coincidência. Se duas valorações concordam nas variáveis de $\varphi$ , dão a $\varphi$ o mesmo valor; por isso a tabela com $2^{n}$ linhas diz tudo. Estabelecido em: 2. Lema de coincidência e tabelas.
FSubstituição semântica. Se $\theta \eqsem \theta'$ e $\chi'$ resulta de substituir em $\chi$ uma ocorrência de $\theta$ por $\theta'$ , então $\chi \eqsem \chi'$ . Estabelecido em: 7. Teorema da substituição semântica.
GLeis de equivalência. Dupla negação, idempotência, comutatividade, associatividade, distributividade, De Morgan, absorção, identidade, dominação, terceiro excluído e não contradição, para fórmulas quaisquer. Estabelecido em: 9. Leis de equivalência.
HLema do valor. $v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1$ se e somente se $v(\varphi_i) = 1$ para todo $i$ ; $v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1$ se e somente se $v(\varphi_i) = 1$ para algum $i$ . Estabelecido em: 10. Lema do valor e compatibilidade.

Trecho 1 O valor de uma fórmula
- Calcular o valor de uma fórmula com a cláusula da negação conjunta e derivar das abreviaturas o de cada conectivo definido.
- Demonstrar o lema de coincidência e justificar com ele que basta uma tabela com $2^{n}$ linhas.
- Classificar fórmulas e conjuntos sem confundir $\not\models \varphi$ com a contradição, e decidir a validade buscando uma valoração que falsifique.
1. Extensão de uma valoração. Cada valoração $v$ estende-se de maneira única a todas as fórmulas com a cláusula $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ ; desdobrando as abreviaturas calcula-se o valor de $\neg$ , $\vee$ , $\wedge$ , $\rightarrow$ , $\leftrightarrow$ e $\veebar$ .
  Apoia-se em: A (Leitura única e recursão), C (Abreviaturas oficiais). Demonstrado em: Semântica da lógica proposicional.
2. Lema de coincidência e tabelas. Se $v$ e $v'$ concordam em $V(\varphi)$ , então $v(\varphi) = v'(\varphi)$ , por indução na complexidade; por isso, os valores de $\varphi$ em todas as valorações são exatamente os das $2^{n}$ linhas da sua tabela.
  Usa: 1. Extensão de uma valoração. Apoia-se em: B (Indução). Demonstrado em: Semântica da lógica proposicional.
3. Classificação e decisão. Toda fórmula é exatamente uma de três coisas: válida, contingente ou contradição; $\varphi$ é válida se e somente se $\neg\varphi$ é contradição, e é contradição se e somente se $\models \neg\varphi$ . $\top$ e o terceiro excluído são válidos, $\bot$ é contradição, e a validade e a satisfatibilidade decidem-se percorrendo as linhas.
  Apoia-se em: D (Valores dos conectivos), E (Lema de coincidência). Demonstrado em: Semântica da lógica proposicional.
Trecho 2 Consequência e equivalência
- Decidir consequências a partir de conjuntos finitos ou infinitos, exibindo um contramodelo ou demonstrando que não existe.
- Aplicar o teorema da dedução semântico e a redução da consequência à insatisfatibilidade.
- Distinguir a substituição de uma ocorrência da substituição uniforme, e demonstrar ambas por indução na complexidade.
- Estabelecer equivalências por cadeias, nomeando corretamente cada lei.
1. A consequência e as suas propriedades. $\Gamma \models \varphi$ se toda valoração que satisfaz $\Gamma$ satisfaz $\varphi$ ; $\emptyset \models \varphi$ se e somente se $\models \varphi$ ; valem a reflexividade, a monotonicidade, o corte e a transitividade, e um conjunto insatisfatível tem como consequência qualquer fórmula.
  Usa: 3. Classificação e decisão. Demonstrado em: Consequência e equivalência semânticas.
2. Dedução semântica e insatisfatibilidade. $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , pela única linha falsa da implicação; $\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots))$ ; e $\Gamma \models \varphi$ se e somente se $\Gamma \cup \{\neg\varphi\}$ é insatisfatível.
  Usa: 4. A consequência e as suas propriedades. Apoia-se em: D (Valores dos conectivos). Demonstrado em: Consequência e equivalência semânticas.
3. Equivalência semântica. $\varphi \eqsem \psi$ se e somente se $\varphi \models \psi$ e $\psi \models \varphi$ , se e somente se $\models (\varphi \leftrightarrow \psi)$ ; a equivalência é reflexiva, simétrica e transitiva, e duas fórmulas equivalentes são intercambiáveis como premissas e como conclusões.
  Usa: 4. A consequência e as suas propriedades. Apoia-se em: D (Valores dos conectivos). Demonstrado em: Consequência e equivalência semânticas.
4. Teorema da substituição semântica. Se $\theta \eqsem \theta'$ , substituir em $\chi$ uma ocorrência de $\theta$ por $\theta'$ , incluída a ocorrência total, dá uma fórmula equivalente a $\chi$ ; e também substituir todas as ocorrências de uma vez.
  Usa: 1. Extensão de uma valoração, 6. Equivalência semântica. Apoia-se em: A (Leitura única e recursão), B (Indução). Demonstrado em: Consequência e equivalência semânticas.
5. Substituição uniforme. Se $w(v_n) = v(\sigma(v_n))$ , então $v(\sigma(\chi)) = w(\chi)$ ; por isso, se $\models \chi$ , também $\models \sigma(\chi)$ , e a substituição uniforme preserva a equivalência e a consequência, mas não a satisfatibilidade nem a contingência.
  Usa: 1. Extensão de uma valoração, 4. A consequência e as suas propriedades, 6. Equivalência semântica. Apoia-se em: A (Leitura única e recursão), B (Indução). Demonstrado em: Consequência e equivalência semânticas.
6. Leis de equivalência. As leis do catálogo verificam-se como identidades entre polinômios com $a^{2} = a$ ; com a substituição e a transitividade, aplicam-se a subfórmulas e encadeiam-se.
  Usa: 3. Classificação e decisão, 6. Equivalência semântica. Apoia-se em: D (Valores dos conectivos), F (Substituição semântica). Demonstrado em: Consequência e equivalência semânticas.
Trecho 3 Leis para qualquer número de termos
- Desdobrar conjunções e disjunções de $n$ termos como cadeias associadas à esquerda e calcular o seu valor.
- Demonstrar por indução no número de termos a associatividade generalizada, a independência da ordem e as leis de De Morgan generalizadas.
- Demonstrar a distributividade generalizada com uma indução em dois índices, e contar os termos que produz.
1. Lema do valor e compatibilidade. Se $\alpha \eqsem \alpha'$ e $\beta \eqsem \beta'$ , então $\neg\alpha \eqsem \neg\alpha'$ , $(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')$ e $(\alpha \vee \beta) \eqsem (\alpha' \vee \beta')$ ; uma conjunção de $n$ termos vale $1$ se e somente se todos os seus termos valem $1$ , uma disjunção se e somente se algum vale $1$ , e termos equivalentes dão conjunções e disjunções equivalentes.
  Usa: 6. Equivalência semântica. Apoia-se em: D (Valores dos conectivos), B (Indução). Demonstrado em: Leis generalizadas de De Morgan e distributivas.
2. Associatividade e ordem. A conjunção das conjunções de duas listas é equivalente à da sua concatenação, e todo agrupamento é equivalente ao associado à esquerda; duas listas com os mesmos termos dão conjunções e disjunções equivalentes, quaisquer que sejam a ordem e as repetições.
  Apoia-se em: H (Lema do valor), G (Leis de equivalência), B (Indução). Demonstrado em: Leis generalizadas de De Morgan e distributivas.
3. Leis de De Morgan generalizadas. $\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i$ e $\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i$ , aplicando a lei binária à última união e a hipótese de indução ao que fica dentro.
  Apoia-se em: H (Lema do valor), G (Leis de equivalência), B (Indução). Demonstrado em: Leis generalizadas de De Morgan e distributivas.
4. Distributividade 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)$ , com $nm$ termos em ordem lexicográfica; e a sua dual, que distribui a disjunção de duas conjunções, por De Morgan.
  Usa: 11. Associatividade e ordem, 12. Leis de De Morgan generalizadas. Apoia-se em: H (Lema do valor), G (Leis de equivalência), B (Indução). Demonstrado em: Leis generalizadas de De Morgan e distributivas.
Trecho 4 Funções de verdade
- Contar as funções de verdade e decidir a equivalência comparando as funções que duas fórmulas representam.
- Construir a fórmula de uma tabela e escrever qualquer função só com a negação conjunta.
- Demonstrar que um conjunto de conectivos é adequado com o critério da negação conjunta, ou que não o é com uma propriedade que as suas fórmulas preservam.
1. Funções de verdade. Há $2^{2^{n}}$ funções de verdade de $n$ argumentos; uma fórmula com variáveis entre $v_1, \ldots, v_n$ representa exatamente uma, $f_\varphi$ , e $\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi$ .
  Usa: 6. Equivalência semântica. Apoia-se em: E (Lema de coincidência). Demonstrado em: Completude funcional.
2. Completude funcional. A conjunção de uma linha vale $1$ exatamente na sua linha; a disjunção das conjunções das linhas em que $f$ vale $1$ , ou $(v_{1} \wedge \neg v_{1})$ se não há nenhuma, representa $f$ ; e toda fórmula é equivalente à fórmula da sua tabela.
  Usa: 14. Funções de verdade. Apoia-se em: H (Lema do valor), D (Valores dos conectivos). Demonstrado em: Completude funcional.
3. Conjuntos adequados e inadequados. A negação conjunta basta, porque as abreviaturas se desdobram; se as fórmulas de $K$ expressam o valor $(1 - a)(1 - b)$ , $K$ é adequado, e assim o são $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ e $\{\uparrow\}$ ; as fórmulas de $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ valem $1$ quando todas as variáveis valem $1$ , e esse conjunto não é adequado.
  Usa: 15. Completude funcional. Apoia-se em: C (Abreviaturas oficiais), B (Indução), D (Valores dos conectivos). Demonstrado em: Completude funcional.
Trecho 5 Formas normais
- Reconhecer literais, cláusulas e formas normais, distinguindo a forma da cadeia do seu significado.
- Construir as formas canônicas a partir da tabela e demonstrar a sua unicidade.
- Demonstrar por indução a existência das formas normais, com a hipótese de indução que pede as duas.
- Decidir à primeira vista a validade de uma forma conjuntiva e a satisfatibilidade de uma disjuntiva.
1. Literais e dualidade. $\neg\ell \eqsem \ell^{*}$ ; uma conjunção elementar é satisfatível se e somente se não contém nenhum par complementar, e uma cláusula é válida se e somente se contém algum; a negação de uma forma normal é equivalente à sua dual, de modo que a forma conjuntiva de $\varphi$ é a dual da forma disjuntiva de $\neg\varphi$ .
  Usa: 12. Leis de De Morgan generalizadas. Apoia-se em: G (Leis de equivalência), F (Substituição semântica), H (Lema do valor). Demonstrado em: Formas normais.
2. Formas canônicas. Se $\varphi$ é satisfatível, é equivalente à sua forma canônica disjuntiva, e se não é válida, à conjuntiva; fixadas as variáveis $v_1, \ldots, v_n$ , duas formas canônicas são equivalentes se e somente se são a mesma cadeia, e duas fórmulas satisfatíveis são equivalentes se e somente se têm a mesma forma canônica disjuntiva.
  Usa: 15. Completude funcional, 17. Literais e dualidade. Apoia-se em: H (Lema do valor), E (Lema de coincidência). Demonstrado em: Formas normais.
3. Existência por indução. $(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)$ ; as formas normais preservam-se pela conjunção e pela disjunção, a forma disjuntiva de uma conjunção e a conjuntiva de uma disjunção por distributividade generalizada; por indução, com a hipótese de indução para as duas formas, toda fórmula tem uma forma disjuntiva e uma conjuntiva.
  Usa: 17. Literais e dualidade, 11. Associatividade e ordem, 13. Distributividade generalizada. Apoia-se em: B (Indução), F (Substituição semântica). Demonstrado em: Formas normais.
4. O que se vê à primeira vista. Uma forma conjuntiva é válida se e somente se cada cláusula contém um par complementar; uma forma disjuntiva é satisfatível se e somente se alguma conjunção elementar não contém nenhum.
  Usa: 17. Literais e dualidade. Apoia-se em: H (Lema do valor). Demonstrado em: Formas normais.
Trecho 6 O algoritmo e os circuitos
- Aplicar o algoritmo de reescrita e escolher a eliminação do bicondicional que convém.
- Demonstrar a sua correção e a sua terminação, e explicar por que a forma conjuntiva pode crescer exponencialmente.
- Obter e simplificar as formas normais de uma caixa-preta, e projetar com elas circuitos de interruptores.
1. Correção e terminação do algoritmo. Substituir uma subescrita por outra equivalente dá uma escrita equivalente; cada regra é uma equivalência, e uma escrita irredutível é uma forma normal agrupada de algum modo; as medidas $M_1$ , $M_2$ , com $M_2(\neg\varphi) = 2^{M_2(\varphi)}$ , e $M_3$ , com $M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi)$ , decrescem a cada passo.
  Usa: 19. Existência por indução, 11. Associatividade e ordem. Apoia-se em: G (Leis de equivalência), D (Valores dos conectivos), B (Indução). Demonstrado em: O algoritmo das formas normais e as suas aplicações.
2. Crescimento exponencial. $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ é equivalente a uma forma conjuntiva com $2^{n}$ cláusulas, e toda forma conjuntiva equivalente tem pelo menos $2^{n}$ cláusulas não válidas.
  Usa: 19. Existência por indução, 17. Literais e dualidade. Apoia-se em: H (Lema do valor). Demonstrado em: O algoritmo das formas normais e as suas aplicações.
3. Linhas vizinhas e circuitos. $(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa$ e a sua dual; um circuito série-paralelo conduz no estado $v$ se e somente se $v(\varphi_C) = 1$ , e toda função de verdade é realizada por algum circuito.
  Usa: 15. Completude funcional, 18. Formas canônicas, 17. Literais e dualidade, 11. Associatividade e ordem. Apoia-se em: G (Leis de equivalência), F (Substituição semântica), D (Valores dos conectivos), B (Indução). Demonstrado em: O algoritmo das formas normais e as suas aplicações.

Rumo à metateoria. A cadeia detém-se onde a semântica alcança um procedimento para cada pergunta sobre fórmulas. Resta saber se o verdadeiro em toda valoração é exatamente o que se deduz no sistema: a próxima unidade comparará as duas noções.