Correção e completude

Duas perguntas sobre o sistema do curso

A unidade sobre a dedução fixou o sistema do curso: os esquemas de axiomas A1, A2 e A3 de Łukasiewicz e duas regras, o modus ponens (MP) e a substituição da dupla negação (SDN), que a aula sobre as quatro técnicas de dedução acrescentou depois de demonstrar a dupla negação. Uma dedução a partir de um conjunto $\Gamma$ é uma sequência finita de fórmulas em que cada uma é um axioma, um elemento de $\Gamma$, o resultado do modus ponens aplicado a duas fórmulas anteriores ou o resultado da SDN aplicada a uma anterior; $\Gamma \vdash \varphi$ significa que há uma dedução a partir de $\Gamma$ cuja última fórmula é $\varphi$. A unidade sobre a semântica, por sua vez, definiu na aula sobre consequência e equivalência semânticas a relação $\Gamma \models \varphi$: toda valoração que satisfaz todas as fórmulas de $\Gamma$ satisfaz $\varphi$. Ambas as relações se escrevem com o mesmo padrão, um conjunto à esquerda e uma fórmula à direita; ora, sua natureza é oposta. A primeira é sintática e existencial: afirma que existe um objeto finito, uma dedução, que se pode revisar símbolo por símbolo. A segunda é semântica e universal: afirma algo de todas as valorações, que são infinitas, e cada uma das quais dá valor a infinitas variáveis.

Duas perguntas se colocam, portanto, sobre o sistema. A primeira: ele deduz só o que deve? Diz-se que o sistema é correto se, para todo conjunto $\Gamma$ e toda fórmula $\varphi$, $\Gamma \vdash \varphi$ implica $\Gamma \models \varphi$: o que se deduz de certas premissas é verdadeiro sob toda valoração que torna verdadeiras as premissas. A segunda: ele deduz tudo o que deve? Diz-se que o sistema é completo se $\Gamma \models \varphi$ implica $\Gamma \vdash \varphi$. A completude admite três graus, segundo os conjuntos de premissas que abrange:

• completude fraca: se $\models \varphi$, então $\vdash \varphi$; toda tautologia é um teorema;
• completude para conjuntos finitos: se $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi$, então $\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$;
• completude forte: se $\Gamma \models \varphi$, então $\Gamma \vdash \varphi$, para um conjunto $\Gamma$ qualquer, também infinito.

Esta aula demonstra a correção e os dois primeiros graus da completude. O terceiro se demonstra na aula sobre o teorema da compacidade, e a razão dessa divisão será explicada no final da aula.

O que não se deve dizer

Em espanhol, chama-se às vezes a correção de “solvencia”, decalque do inglês soundness; o termo espanhol é “corrección”, e é o que o curso usa em espanhol. Tampouco se deve defini-la como a propriedade do sistema “de inferir uma expressão a partir de um conjunto de expressões”, que é a própria dedutibilidade e não uma propriedade do sistema. Os erros de fundo, no entanto, são outros dois.

O primeiro é afirmar que a correção e a completude “podem ser inferidas uma da outra”. São propriedades independentes: o sistema de Łukasiewicz, sem a regra SDN, é correto (a demonstração desta aula o prova, suprimindo um caso) e não é completo (a aula sobre os sistemas dedutivos formais exibiu uma tautologia que ele não deduz); e um sistema que adotasse todas as fórmulas como axiomas seria completo sem ser correto. O problema resolvido 2 examina ambos os exemplos.

O segundo erro é mais grave, porque apresenta como demonstração da completude um argumento circular. Diz, em substância: se $\varphi \nvdash \psi$, então, pelo teorema da dedução, $\nvdash (\varphi \rightarrow \psi)$; “pela correção”, $\not\models (\varphi \rightarrow \psi)$; e pelo teorema da dedução semântico, $\varphi \not\models \psi$. Ora, a correção diz que o dedutível é válido, e sua contrapositiva, que o que não é válido não é dedutível:

O passo do argumento vai no outro sentido, de $\nvdash \chi$ a $\not\models \chi$, que é a contrapositiva de $\models \chi \Rightarrow \vdash \chi$, isto é, da completude fraca. Se isso é assim, o argumento supõe o que pretende demonstrar. Disso se segue que a completude não se “infere de um modo simples”: é o resultado mais profundo do curso, e sua demonstração ocupa a maior parte desta aula. Por último, é inexato resumir a completude dizendo que “todas as expressões verdadeiras têm uma demonstração”; o que tem demonstração é o válido, verdadeiro sob toda valoração, não o verdadeiro sob alguma: a variável $v_{1}$ é verdadeira sob muitas valorações, e não é um teorema.