Demonstrações e tableaux semânticos

1. O que é uma demonstração

Um argumento é a afirmação de que certa conclusão decorre de certas premissas. Uma demonstração é o que decide essa afirmação: um objeto finito e verificável que qualquer pessoa pode ler linha a linha e aceitar, sem ter de acreditar na sua palavra. O valor de uma demonstração não está em convencer - um bom discurso também convence -, mas em que cada um dos seus passos não poderia ter sido outro.

É uma exigência mais rigorosa do que parece. «Chove, logo o chão está molhado» é uma coisa razoável de se dizer, mas apoia-se no que você sabe sobre chuva e chão. A lógica formal põe isso de lado e faz uma pergunta mais estreita: dada apenas a forma das frases, há alguma maneira de as premissas serem verdadeiras e a conclusão falsa? Se não há, o argumento é válido, e a demonstração é o registo de por que não há.

Este guia trata de uma maneira de produzir esse registo: o método dos tableaux semânticos, também chamados árvores de verdade. É o método que este site usa sempre que você escreve um argumento na calculadora, e depois de o seguir uma vez basta uma caneta para verificar um argumento no papel.

2. Válido, e como saber

Escreva um argumento com um sinal de consequência: as premissas à esquerda, a conclusão à direita. A afirmação p → q, ¬q ⊨ ¬p diz que de um condicional e da negação do seu consequente decorre a negação do seu antecedente. O sinal de consequência não é mais um conetivo. É uma afirmação sobre as fórmulas de ambos os lados, e está certa ou errada.

A definição de validade aponta diretamente para um modo de a testar: percorra cada atribuição de verdadeiro e falso às variáveis e veja se alguma torna todas as premissas verdadeiras e a conclusão falsa. É o que faz uma tabela de verdade, e com duas ou três variáveis serve perfeitamente. O problema é que a tabela cresce como 2ⁿ. Dez variáveis exigem mil linhas, vinte exigem um milhão, e a tabela nada diz sobre quais linhas importaram.

Um tableau ataca a mesma pergunta pelo outro extremo. Em vez de listar todas as possibilidades e procurar uma má, supõe que existe uma má e tenta construí-la. Se a tentativa desaba em contradição por todos os caminhos possíveis, não existe tal atribuição e o argumento é válido. Se a tentativa der certo, o que foi construído é um contraexemplo que você pode ler diretamente.

3. O método dos tableaux

Um tableau é uma árvore de fórmulas assinadas. Cada linha é uma fórmula precedida de um T ou de um F, e o sinal diz o que o ramo supõe sobre essa fórmula: não qual é o seu valor de verdade, mas qual teria de ser para que o argumento falhasse. Todo o método são quatro passos:

1. Escreva cada premissa com um T. Você está a supor que todas as premissas do argumento valem.
2. Escreva a conclusão com um F. Você está a supor que ela falha mesmo assim - é a suposição que quer refutar.
3. Tome qualquer linha que ainda não seja um átomo e aplique a regra do seu conetivo principal e do seu sinal, acrescentando o que essa regra produz ao fim de cada ramo que passa por ela.
4. Feche um ramo assim que ele contenha ao mesmo tempo T A e F A para a mesma fórmula A. Pare quando todos os ramos estiverem fechados, ou quando não restar linha para decompor.

Nada neste ciclo exige argúcia ou uma escolha de estratégia. Cada linha tem exatamente uma regra, e aplicá-las em qualquer ordem dá o mesmo veredito - é por isso que uma máquina consegue fazê-lo, e por isso que você pode confiar no resultado quando ela o faz.

4. As regras

Há uma regra por conetivo e por sinal - dez ao todo. Dividem-se em duas espécies, e a diferença entre elas é toda a razão de um tableau ser uma árvore e não uma lista. Uma regra α diz que várias coisas têm de valer em conjunto, e por isso empilha os seus resultados ramo abaixo. Uma regra β diz que uma de duas coisas tem de valer, e por isso divide o ramo em dois e deixa cada caso seguir o seu caminho.

Cada regra não é senão a condição de verdade do seu conetivo, lida ao contrário. Uma conjunção só é verdadeira quando ambos os lados o são, portanto T (A ∧ B) empilha T A e T B. Uma conjunção é falsa quando pelo menos um lado o é, mas a fórmula não diz qual, portanto F (A ∧ B) tem de tentar os dois: ramifica. A mesma assimetria corre ao contrário na disjunção, e um condicional falso significa que o antecedente valeu e o consequente falhou - o único caso em que uma implicação se quebra.

Repare no que as regras nunca fazem: nunca inventam uma fórmula. Tudo o que uma regra produz é um pedaço da linha de onde veio. Essa propriedade - a propriedade da subfórmula - é o que torna o método finito, e voltamos a ela mais abaixo.

5. Fechar um ramo

Um ramo é um único fio de raciocínio: leia da raiz até uma folha e terá um conjunto completo de suposições. Um ramo fecha-se quando essas suposições se contradizem abertamente, isto é, quando ele carrega ao mesmo tempo T A e F A para uma única e mesma fórmula. Não importa quão complicada seja A nem quão distantes estejam as duas linhas: se um ramo exige que uma fórmula seja verdadeira e falsa ao mesmo tempo, nada o satisfaz.

Marque um ramo fechado com ×, indicando as duas linhas que o fecharam, e deixe de trabalhar nele. Nada mais se aprende de uma suposição que já era impossível.

Quando todos os ramos se fecham, o tableau está fechado, e isso é a demonstração. Mostra que a suposição de partida - todas as premissas verdadeiras, a conclusão falsa - leva a contradição por cada caminho que poderia tomar. Como não restou caminho algum, não existe tal atribuição, e o argumento é válido. É uma demonstração por absurdo, disposta de modo que nenhum caso possa escapar.

6. Uma demonstração, linha a linha

Tomemos o modus tollens: p → q, ¬q ⊨ ¬p. As linhas 1 e 2 são as premissas, supostas verdadeiras. A linha 3 é a conclusão, suposta falsa - e como a conclusão é ¬p, supô-la falsa é supor p verdadeira, o que a linha 5 regista. A linha 4 vem da regra da negação aplicada à linha 2: se ¬q é verdadeira, q é falsa. O condicional da linha 1 é a única linha que ainda tem um conetivo, e é uma regra β, portanto a árvore bifurca:

O ramo da esquerda supõe que o condicional valeu porque o seu antecedente falhou - mas a linha 5 já tem p verdadeira, portanto o ramo contradiz-se e fecha. O ramo da direita supõe que valeu porque o seu consequente era verdadeiro - mas a linha 4 já tem q falsa, portanto também fecha.

Ambos os ramos fecharam, portanto não há maneira de ter p → q e ¬q verdadeiras com ¬p falsa. O argumento é válido, e a árvore é a razão. Repare que a demonstração nunca menciona chuva, chão, nem o que p e q representam. Não precisou.

7. Quando um ramo fica aberto

Nem todo argumento é válido, e é aqui que o método se justifica. Se você trabalhar um ramo até que nada nele possa ser decomposto mais - restam apenas átomos e átomos negados - e ele ainda assim não tiver fechado, esse ramo está saturado e aberto. Não deixou de fechar por você ter parado cedo demais: não há mais nada a tentar.

Um ramo aberto é mais do que um veredito de «inválido». Leia os sinais dos seus átomos e terá uma atribuição: todo átomo marcado com T é verdadeiro, todo átomo marcado com F é falso. Essa atribuição torna todas as premissas verdadeiras e a conclusão falsa, que é exatamente o que é um contraexemplo. Os lógicos chamam-lhe um contramodelo, e é uma resposta concreta a «porque não?» em vez de uma recusa.

A afirmação do consequente, p → q, q ⊨ p, é o caso clássico. O seu tableau deixa um ramo aberto com p falsa e q verdadeira - uma situação em que o condicional vale e o seu consequente vale, e ainda assim o antecedente não. Essa única atribuição refuta o argumento por si só.

8. Por que termina sempre

Cada regra substitui uma fórmula pelas suas próprias subfórmulas, e toda subfórmula é estritamente mais curta do que a fórmula de onde veio. Nenhum ramo pode, portanto, crescer para sempre: cada passo desce uma escada finita de pedaços do argumento original, e a escada tem fundo. Mais cedo ou mais tarde, cada linha de um ramo é um átomo ou a negação de um, e não há mais nada a fazer.

É uma garantia real, não uma esperança. Significa que o método é um procedimento de decisão para a lógica proposicional: aplique-o a qualquer argumento e ele para, com uma árvore fechada ou com um ramo aberto, e nunca com um encolher de ombros. O demonstrador deste site impõe além disso um limite de nós, mas apenas como proteção contra uma fórmula patológica esgotar um separador do navegador - a matemática não precisa de limite algum.

9. Outros sistemas de demonstração

Os tableaux são um sistema de demonstração entre vários, e são o que tem forma de refutação: trabalham excluindo o fracasso. A dedução natural faz o inverso e constrói a conclusão para a frente a partir das premissas, com regras como o modus ponens e a prova condicional, e lê-se muito mais como um matemático argumenta em prosa. Uma demonstração em dedução natural é em geral mais curta; encontrá-la exige em geral mais invenção.

O cálculo de sequentes formaliza o próprio sinal de consequência e trata as afirmações de consequência como objetos, o que faz dele a ferramenta de eleição para demonstrar coisas sobre demonstrações. A resolução reduz tudo a cláusulas e a uma única regra, o que é pouco vistoso de ler e extremamente rápido de executar - é sobre ela que assentam a maioria dos demonstradores automáticos e dos solucionadores SAT.

Todos concordam sobre quais argumentos proposicionais são válidos; diferem no aspeto de uma demonstração e no que é fácil de encontrar. Os tableaux são os mais acolhedores para aprender, porque uma demonstração falhada não é um beco sem saída: entrega-lhe o contraexemplo.

10. Praticar

A maneira mais rápida de aprender o método é executá-lo. Escreva um argumento na calculadora com ⊨, ⊢ ou |= e o tableau é desenhado ao lado da tabela de verdade, para que possa conferir a árvore com as linhas. Depois trabalhe algumas demonstrações no papel antes de espreitar.