Metateoria: síntese e desafios

Resumo

Esta aula encerra a unidade dedicada à metateoria e, com ela, o conteúdo do curso. Reconstrói a cadeia dedutiva que vai da validade dos axiomas à correção do sistema; dos dois lemas da negação conjunta ao lema de Kalmár e à completude para conjuntos finitos; do lema das duas testemunhas ao teorema da compacidade e, por meio dele, à completude forte; e da forma clausal à correção e à completude refutacional do método de resolução, indicando em cada elo que resultados usa e em que aula se demonstra. Mostra como as três partes anteriores do curso, linguagem, dedução e semântica, convergem na coincidência de $\vdash$ e $\models$ , e o que cada uma contribui para ela; distingue o que o curso demonstrou do que supôs e do que deixa em aberto. Repete na sua avaliação de saída as habilidades da avaliação de entrada e termina com seis desafios, mais difíceis do 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, e justificar a ordem da compacidade e da completude forte.
Explicar como linguagem, dedução e semântica convergem na coincidência de $\vdash$ e $\models$ , e que resultado de cada unidade do curso é indispensável para ela.
Distinguir o que o curso demonstrou do que supôs (os esquemas de axiomas, as regras primitivas e a indução) e do que deixa em aberto (o custo de decidir a satisfatibilidade e a lógica com quantificadores).
Resolver problemas que combinam marcas, o lema de Kalmár, a substituição uniforme, a compacidade e a resolução, usando em cada caso o lado fácil da coincidência.

O que a unidade alcançou

A unidade propôs-se comparar as duas relações que as unidades anteriores tinham construído sobre a mesma linguagem, a dedutibilidade $\Gamma \vdash \varphi$ e a consequência semântica $\Gamma \models \varphi$ , e demonstrar que coincidem. O objetivo foi alcançado sem ressalvas nos enunciados: as duas relações são a mesma para todo conjunto de premissas, finito ou infinito, e a resolução oferece uma terceira via, igualmente correta e completa, para decidir a consequência. As ressalvas estão nos métodos, e cada uma foi declarada no seu lugar: a completude da primeira aula é construtiva, mas não prática, porque produz deduções tão longas quanto a tabela; a compacidade assegura que uma valoração existe, mas não ensina a encontrá-la; e a resolução decide, mas o seu custo no pior caso é uma questão em aberto. Com essas ressalvas, o caminho percorrido lê-se como uma única cadeia dedutiva em quatro trechos.

Correção

A aula sobre correção e completude começou por fixar o vocabulário: o sistema é correto se $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , e completo se vale a recíproca, em três graus (fraca, para conjuntos finitos e forte). Desmontou um argumento circular que pretende obter a completude «pela correção» passando de $\nvdash \chi$ a $\not\models \chi$ , um passo que é a contrarrecíproca da completude fraca, e mostrou que as duas propriedades são independentes. Demonstrou depois que toda instância de A1, A2 e A3 é válida, supondo uma valoração que a refutasse e chegando, pela linha falsa da implicação, a valores impossíveis; e, por indução forte sobre o número de linhas, a correção, com um caso para os axiomas, outro para as premissas, o modus ponens semântico e, para a regra da substituição da dupla negação, a equivalência $\theta \eqsem \neg\neg\theta$ com o teorema da substituição semântica. A propriedade que se transmite de linha em linha não é a validade, mas a satisfação por uma valoração fixa que satisfaz as premissas, e é por isso que a correção vale com premissas, mesmo infinitas. Dela seguiram-se a consistência de todo conjunto satisfatível, em particular a do sistema, e o método que faltava à unidade de dedução: um contramodelo demonstra que uma dedução não existe.

Kalmár e a completude finita

A mesma aula demonstrou a recíproca em dois passos. O primeiro é o lema de Kalmár: se as variáveis de $\varphi$ estão entre $u_{1}, \ldots, u_{n}$ , então $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ para toda valoração $v$ , onde $\psi^{v}$ é $\psi$ se $v(\psi) = 1$ e $\neg\psi$ caso contrário; o sistema deduz de cada linha o que a linha diz da fórmula. A sua indução sobre a complexidade tem um único caso composto, $(\alpha \downarrow \beta)$ , porque a negação conjunta é o único conectivo primitivo, e dentro dele três subcasos, que pedem dois lemas do sistema, o segundo em duas formas: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , deduzido com a introdução da conjunção, a dupla negação e duas aplicações da regra SDN, e $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ e $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , deduzidos com a introdução da disjunção. O segundo passo elimina as premissas: se $\varphi$ é uma tautologia, deduz-se das premissas de cada uma das $2^{n}$ linhas, e a prova por casos elimina o literal da última variável, depois o da penúltima, até chegar a $\vdash \varphi$ , a completude fraca. Com o teorema da dedução semântico e a recíproca do sintático, a completude estendeu-se aos conjuntos finitos de premissas; donde, com premissas finitas, dedução e consequência coincidem, a equivalência demonstrável coincide com a semântica e a dedutibilidade é decidível, porque a tabela responde por ela.

Compacidade e completude forte

A aula sobre o teorema da compacidade enfrentou o caso infinito, que o lema de Kalmár não alcança, porque infinitas premissas não se descarregam numa implicação. Demonstrou, sem mencionar nenhuma dedução, que um conjunto é satisfatível se e somente se cada um dos seus subconjuntos finitos o é. Uma sequência de valores para $v_{1}, \ldots, v_{n}$ é boa se todo subconjunto finito do conjunto é satisfeito por alguma valoração que a prolonga; o lema das duas testemunhas assegura que uma sequência boa se prolonga numa boa, porque, se nenhum dos dois prolongamentos fosse bom, a união das duas testemunhas finitas contradiria que a sequência é boa; e a valoração que resulta de preferir sempre o valor $1$ quando é possível satisfaz cada fórmula, pelo lema de coincidência, porque cada fórmula tem um número finito de variáveis. A construção não precisa do axioma da escolha, porque as variáveis estão numeradas e cada passo tem uma regra. Da compacidade seguiram-se as suas formas equivalentes, a forma da insatisfatibilidade e a forma da consequência; desta, da completude para conjuntos finitos e da monotonia, a completude forte; e desta e da correção, a coincidência plena: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ para todo $\Gamma$ , e um conjunto é consistente se e somente se é satisfatível. A aula advertiu que essa ordem não é uma questão de preferência: obter a compacidade de uma completude forte ainda não disponível seria circular. Terminou com a coloração de grafos enumeráveis, que traduz um problema infinito num conjunto de fórmulas cujas partes finitas são satisfatíveis, e com os limites do que um conjunto de fórmulas pode expressar.

Resolução

A aula sobre o método de resolução substituiu os conjuntos de fórmulas por conjuntos de cláusulas, cada uma um conjunto finito de literais, com duas representações: a forma clausal, que tem os mesmos modelos, e a forma definicional, que introduz uma variável nova para cada subescrita composta, conserva apenas a satisfatibilidade e cresce como a fórmula, não como uma potência de dois. Uma única regra atua sobre as cláusulas: de $C$ e $D$ , com $\ell \in C$ e $\ell^{*} \in D$ , infere-se $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , e uma refutação é uma derivação que chega a $\Box$ . A correção demonstrou-se como a do sistema, por indução sobre a derivação e com a resolvente como consequência das suas premissas; a completude refutacional, por indução sobre o número de variáveis, com a eliminação de uma variável, que conserva a satisfatibilidade e cuja demonstração constrói um modelo; e para conjuntos infinitos, de novo com a compacidade. Seguiu-se que $\Gamma \models \varphi$ se e somente se uma forma clausal de $\Gamma \cup \{\neg\varphi\}$ tem uma refutação, e que a saturação, finita porque com $n$ variáveis não há mais de $4^{n}$ cláusulas, decide a satisfatibilidade sem tabelas. A aula apresentou o problema da satisfatibilidade, cujo custo no pior caso ninguém conhece, e dois casos que se decidem depressa, as cláusulas de Horn e as de dois literais.

A figura seguinte reúne os quatro trechos numa única cadeia. Cada nó da coluna é um resultado, numerado segundo a ordem lógica e unido por um arco aos elos anteriores que a sua demonstração usa; à sua volta flutuam os apoios, isto é, os princípios e ferramentas a que 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, exceto os que vêm das unidades anteriores, que se desenham como anéis. Clicar num apoio destaca todos os elos que o usam, e cada elo remete para a aula em que se demonstra. Observe-se que a correção e a compacidade, estabelecidas uma no primeiro trecho e a outra no terceiro, reaparecem nos trechos seguintes, e que o apoio mais visitado da unidade são as valorações e coincidência, seguidas da indução, nas suas três formas: sobre as linhas de uma dedução, sobre a complexidade de uma fórmula e sobre o número de variáveis de um conjunto de cláusulas.

Apoios da cadeia

AIndução e recursão. Indução forte sobre os naturais, indução sobre a complexidade das fórmulas, com o único caso composto $(\alpha \downarrow \beta)$ , e definição por recursão. Demonstraram-se na primeira unidade. Admitido sem demonstração nesta unidade.
BSistema do curso. A1, A2 e A3, o modus ponens e a regra SDN; reflexividade, monotonia, modus ponens entre deduções, finitude e $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . Estabeleceram-se na segunda unidade. Admitido sem demonstração nesta unidade.
CTécnicas derivadas. Dupla negação, da aula sobre as quatro técnicas; introdução da conjunção e da disjunção e prova por casos (se $\Gamma \cup \{\psi\} \vdash \chi$ e $\Gamma \cup \{\neg\psi\} \vdash \chi$ , então $\Gamma \vdash \chi$ ), da aula sobre as técnicas da lógica clássica. Demonstraram-se na segunda unidade. Admitido sem demonstração nesta unidade.
DValorações e coincidência. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; se duas valorações coincidem em $V(\varphi)$ , dão a $\varphi$ o mesmo valor; a validade decide-se com $2^{n}$ linhas. Demonstraram-se na terceira unidade. Admitido sem demonstração nesta unidade.
EConsequência semântica. Linha falsa da implicação, monotonia, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ se e somente se $\Gamma \cup \{\neg\varphi\}$ é insatisfatível, e o teorema da substituição semântica. Demonstraram-se na terceira unidade. Admitido sem demonstração nesta unidade.
FFormas conjuntivas. Lema do valor; toda fórmula equivale a uma forma normal conjuntiva, que pode precisar de $2^{n}$ cláusulas; uma disjunção de literais é válida se e somente se contém um par complementar. Demonstraram-se na terceira unidade. Admitido sem demonstração nesta unidade.
GCorreção. Se $\Gamma \vdash \varphi$ , então $\Gamma \models \varphi$ , para todo conjunto $\Gamma$ ; um contramodelo demonstra que uma dedução não existe. Estabelecido em: 2. Correção.
HCompacidade. Um conjunto de fórmulas é satisfatível se e somente se todo subconjunto finito dele é satisfatível; donde o que é insatisfatível já o é numa parte finita. Estabelecido em: 11. Teorema da compacidade.

Trecho 1 Correção
- Verificar que toda instância dos esquemas é válida sem construir a sua tabela.
- Demonstrar a correção por indução forte sobre o número de linhas, com o caso da regra da substituição da dupla negação.
- Demonstrar com um contramodelo que uma fórmula não se deduz, e obter a consistência a partir da correção.
1. Validade dos axiomas. Toda instância de A1, A2 e A3 é válida: uma valoração que a refutasse exigiria, pela linha falsa da implicação, valores impossíveis.
  Apoia-se em: E (Consequência semântica). Demonstrado em: Correção e completude.
2. Correção. Se $\Gamma \vdash \varphi$ , então $\Gamma \models \varphi$ , para todo $\Gamma$ : por indução forte sobre o número de linhas, com um caso para os axiomas, outro para as premissas, o modus ponens semântico e, para a regra SDN, $\theta \eqsem \neg\neg\theta$ com a substituição semântica.
  Usa: 1. Validade dos axiomas. Apoia-se em: A (Indução e recursão), B (Sistema do curso), E (Consequência semântica). Demonstrado em: Correção e completude.
3. Consistência e contramodelos. Todo conjunto satisfatível é consistente; o sistema é consistente e $\nvdash v_{1}$ ; se uma valoração satisfaz $\Gamma$ e refuta $\varphi$ , então $\Gamma \nvdash \varphi$ , e a tabela certifica que o que não é válido não é teorema.
  Apoia-se em: G (Correção), D (Valorações e coincidência). Demonstrado em: Correção e completude.
Trecho 2 Kalmár e a completude finita
- Deduzir no sistema os dois lemas da negação conjunta, com a regra da substituição da dupla negação onde for preciso.
- Demonstrar o lema de Kalmár por indução sobre a complexidade, com um único caso composto.
- Eliminar com a prova por casos as premissas das linhas, e descarregar premissas finitas com os dois teoremas da dedução.
- Decidir com a tabela a dedutibilidade, a equivalência demonstrável e a consistência a partir de premissas finitas.
1. Introdução da negação conjunta. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ e $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : a conjunção das negações é $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; a dupla negação retira a exterior, e a regra SDN as duas interiores.
  Apoia-se em: B (Sistema do curso), C (Técnicas derivadas). Demonstrado em: Correção e completude.
2. Negação da negação conjunta. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ e $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , porque $\neg(\alpha \downarrow \beta)$ é $(\alpha \vee \beta)$ e basta a introdução da disjunção.
  Apoia-se em: B (Sistema do curso), C (Técnicas derivadas). Demonstrado em: Correção e completude.
3. Lema de Kalmár. Se $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , então $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ para toda valoração $v$ ; o passo indutivo tem um único caso, $(\alpha \downarrow \beta)$ , com três subcasos segundo os valores de $\alpha$ e de $\beta$ .
  Usa: 4. Introdução da negação conjunta, 5. Negação da negação conjunta. Apoia-se em: A (Indução e recursão), D (Valorações e coincidência), B (Sistema do curso). Demonstrado em: Correção e completude.
4. Completude fraca. Se $\models \varphi$ , então $\vdash \varphi$ : o lema de Kalmár deduz $\varphi$ de cada linha, e a prova por casos elimina os literais da última variável à primeira, com $2^{n}$ usos do lema e $2^{n} - 1$ da prova por casos.
  Usa: 6. Lema de Kalmár. Apoia-se em: C (Técnicas derivadas). Demonstrado em: Correção e completude.
5. Completude para conjuntos finitos. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : o teorema da dedução semântico leva a uma tautologia, a completude fraca deduz-na e a recíproca do teorema da dedução devolve as premissas.
  Usa: 7. Completude fraca. Apoia-se em: E (Consequência semântica), B (Sistema do curso). Demonstrado em: Correção e completude.
6. Coincidência finita e decisão. Para $\Gamma$ finito, $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ , e $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; donde a dedutibilidade a partir de premissas finitas é decidível, pela tabela.
  Usa: 8. Completude para conjuntos finitos. Apoia-se em: G (Correção), D (Valorações e coincidência). Demonstrado em: Correção e completude.
Trecho 3 Compacidade e completude forte
- Demonstrar a compacidade fixando um a um os valores das variáveis, com o invariante das sequências boas e o argumento das duas testemunhas.
- Passar entre a forma da satisfatibilidade, a da insatisfatibilidade e a da consequência.
- Obter a completude forte a partir da compacidade, sem circularidade, e dela a coincidência da consistência com a satisfatibilidade.
- Codificar em conjuntos de fórmulas problemas sobre objetos infinitos e resolvê-los com a compacidade.
1. Lema das duas testemunhas. Se a sequência $s$ de valores fixados é boa (todo subconjunto finito do conjunto é satisfeito por uma valoração que a prolonga), também o é $(s, 1)$ ou $(s, 0)$ : se nenhuma o fosse, a união das duas testemunhas finitas contradiria que $s$ é boa.
  Apoia-se em: D (Valorações e coincidência). Demonstrado em: O teorema da compacidade.
2. Teorema da compacidade. $\Gamma$ é satisfatível se e somente se todo subconjunto finito o é: fixa-se $v_{n + 1}$ em $1$ se $(s_{n}, 1)$ é boa e em $0$ caso contrário, e a valoração resultante satisfaz cada fórmula pelo lema de coincidência. Não é necessário o axioma da escolha, porque as variáveis estão numeradas.
  Usa: 10. Lema das duas testemunhas. Apoia-se em: A (Indução e recursão), D (Valorações e coincidência). Demonstrado em: O teorema da compacidade.
3. Formas equivalentes. $\Gamma$ é insatisfatível se e somente se alguma parte finita o é; $\Gamma \models \varphi$ se e somente se $\Gamma_{0} \models \varphi$ para algum $\Gamma_{0} \subseteq \Gamma$ finito; e esta última forma implica, por sua vez, o teorema.
  Usa: 11. Teorema da compacidade. Apoia-se em: E (Consequência semântica). Demonstrado em: O teorema da compacidade.
4. Completude forte. Se $\Gamma \models \varphi$ , então $\Gamma \vdash \varphi$ , para todo $\Gamma$ : a forma da consequência dá um $\Gamma_{0}$ finito, a completude para conjuntos finitos dá $\Gamma_{0} \vdash \varphi$ , e a monotonia $\Gamma \vdash \varphi$ .
  Usa: 8. Completude para conjuntos finitos, 12. Formas equivalentes. Apoia-se em: B (Sistema do curso). Demonstrado em: O teorema da compacidade.
5. Dedução é consequência. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ para todo $\Gamma$ ; os teoremas são exatamente as tautologias, e um conjunto é consistente se e somente se é satisfatível.
  Usa: 13. Completude forte. Apoia-se em: G (Correção). Demonstrado em: O teorema da compacidade.
6. Coloração de grafos enumeráveis. Com uma variável $x_{i,c}$ para cada vértice e cor, e fórmulas que dizem que cada vértice tem uma cor e só uma e que os vizinhos diferem, um grafo enumerável admite coloração com $k$ cores se todo subgrafo finito a admite.
  Apoia-se em: H (Compacidade), F (Formas conjuntivas). Demonstrado em: O teorema da compacidade.
Trecho 4 Resolução
- Representar um conjunto de fórmulas como conjunto de cláusulas, pela forma conjuntiva ou pela definicional.
- Construir refutações sem eliminar dois pares complementares num só passo.
- Demonstrar a correção e a completude refutacional da resolução, para conjuntos finitos e, com a compacidade, para quaisquer.
- Decidir consequências por saturação e reconhecer os casos que se decidem depressa.
1. Forma clausal. Uma cláusula é um conjunto finito de literais, satisfeito se algum literal toma o valor $1$ , e $\Box$ é insatisfatível; uma forma clausal de $\Gamma$ tem os mesmos modelos, e $\Gamma \models \varphi$ se e somente se uma forma clausal de $\Gamma \cup \{\neg\varphi\}$ é insatisfatível.
  Apoia-se em: F (Formas conjuntivas), E (Consequência semântica). Demonstrado em: O método de resolução.
2. Forma clausal definicional. Com uma variável nova por subescrita e as suas cláusulas de definição, $T(\varphi)$ é equissatisfatível com $\varphi$ e tem no máximo $4k + 1$ cláusulas de no máximo três literais; as formas definicionais decidem a consequência a partir de premissas finitas.
  Usa: 16. Forma clausal. Apoia-se em: A (Indução e recursão), D (Valorações e coincidência). Demonstrado em: O método de resolução.
3. Correção da resolução. $\{C, D\} \models R_{\ell}(C, D)$ , por casos sobre o valor de $\ell$ ; por indução forte sobre a derivação, $S \models C$ para toda cláusula $C$ derivada de $S$ , e se $S$ tem uma refutação, é insatisfatível.
  Usa: 16. Forma clausal. Apoia-se em: A (Indução e recursão). Demonstrado em: O método de resolução.
4. Eliminação de uma variável. $E_{p}(S)$ , que conserva as cláusulas sem $p$ nem $\neg p$ e acrescenta as resolventes sobre $p$ , não contém $p$ e é equissatisfatível com $S$ ; de um modelo dele obtém-se um de $S$ escolhendo o valor de $p$ .
  Usa: 18. Correção da resolução. Apoia-se em: D (Valorações e coincidência). Demonstrado em: O método de resolução.
5. Completude refutacional finita. Todo conjunto finito insatisfatível de cláusulas tem uma refutação, por indução sobre o número de variáveis: elimina-se a última e inserem-se as premissas de cada resolvente.
  Usa: 19. Eliminação de uma variável. Apoia-se em: A (Indução e recursão). Demonstrado em: O método de resolução.
6. Completude refutacional. Um conjunto de cláusulas, finito ou infinito, é insatisfatível se e somente se tem uma refutação; donde $\Gamma \models \varphi$ se e somente se uma forma clausal de $\Gamma \cup \{\neg\varphi\}$ tem uma refutação.
  Usa: 16. Forma clausal, 18. Correção da resolução, 20. Completude refutacional finita. Apoia-se em: H (Compacidade). Demonstrado em: O método de resolução.
7. A saturação decide. Com $n$ variáveis, o conjunto das cláusulas derivadas tem no máximo $4^{n}$ elementos; a saturação termina e decide a satisfatibilidade sem tabelas, embora nem sempre mais depressa do que elas.
  Usa: 18. Correção da resolução, 20. Completude refutacional finita. Demonstrado em: O método de resolução.

O fim do curso. A cadeia termina onde as duas faces do curso se reconhecem como uma única relação e se dispõe de um método para decidi-la. O que fica em aberto já não é uma pergunta sobre a lógica proposicional, mas sobre o seu custo e sobre a sua extensão aos quantificadores.