Na parte anterior, delineamos essencialmente todos os elementos semânticos do Cálculo Proposicional (CP) e discutimos um pouco sobre satisfabilidade e consequências lógicas. Ainda temos que discutir sobre algumas coisas da semântica do CP, como a construção de fórmulas a partir de tabelas-verdade, mas esse é um artifício muito intuitivo. Este post focará na sintaxe do CP e sua relação com a semântica. Pessoalmente, vejo a sintaxe do CP como algo muito mais complexo que a semântica por estar diretamente relacionada à Teoria dos Modelos, mas isso também a torna mais interessante.

Vamos conhecer um método de construção de fórmulas a partir de tabelas-verdade. Em outras palavras, suponha que temos uma tabela-verdade com literais e queremos descobrir qual a fórmula referente à tabela-verdade. Para fazê-lo, nós podemos seguir duas rotas semelhantes que utilizam das chamadas formas normais de fórmulas do CP.  Existem várias formas normais, mas vamos focar nas Forma Normal Conjuntiva e Forma Normal Disjuntiva.

Uma fórmula está na Forma Normal Conjuntiva (FNC) se ela é uma conjunção de cláusulas, em que cada cláusula é uma disjunção. Ou seja, ela é composta por várias sub-fórmulas contendo apenas ou de forma que há um entre todas elas. Por exemplo, a fórmula está na FNC enquanto as fórmulas e não estão. Podemos formalizar um pouco mais essa definição. Seja um conjunto de fórmulas em que cada fórmula é composta apenas por literais e os operadores e . A fórmula está, por definição, de acordo com a FNC.

Uma fórmula está na Forma Normal Disjuntiva (FND) se o oposto acontece – ela é uma disjunção de cláusulas, em que cada cláusula é uma conjunção. A ideia é a mesma que a FNC, porém os conectivos lógicos são invertidos. Vamos pular direto à definição formal desta vez. Seja um conjunto de fórmulas em que cada fórmula é composta apenas por literais e os operadores e . A fórmula está, por definição, de acordo com a FND.

Agora podemos descrever dois métodos de obter fórmulas do CP dada a tabela-verdade. A ideia é criar uma fórmula exaustivamente que captura todas combinações em que a fórmula é verdadeira ou falsa. Vamos ver alguns exemplos. Considere a tabela-verdade abaixo:

F	F	V
F	V	F
V	F	V
V	V	F

Nosso objetivo é descobrir a fórmula . Podemos considerar todas as situações em é verdadeira e construir uma fórmula na FND ou todas as situações em que é falsa e construir uma fórmula na FNC. Primeiro construiremos a fórmula na FND. Observe que é verdadeira quando e  são ambos falsos ou  é verdadeiro e  é falso. Apenas notando essas situações, acabamos de construir a fórmula! Isto é, . Quando temos uma meta-variável da fórmula com o valor-verdade falso na linha em que a fórmula é verdadeira, temos que negá-lo. Agora faremos o mesmo porém com a finalidade de construir a fórmula na FNC. A construção da fórmula na FNC é um pouco menos intuitiva, mas o procedimento é semelhante. Observe que é falsa na 2ª linha, em que é falso e é verdadeiro e na 4ª linha, em que tanto quando são verdadeiros. Logo a fórmula resultante é . Em suma, os procedimentos para obter fórmulas na FND e FNC consistem em escrever todas as cláusulas em que a fórmula é verdadeira ou falsa, respectivamente. Sem surpresas, a conversão de fórmulas na FNC para FND é tão complexa quanto o Problema da Satisfabilidade, ou seja, NP-complexo.

Agora finalmente podemos discutir sobre sintaxe! A sintaxe do CP é construída com o objetivo de criar um sistema de demonstrações que é correto, no sentido de que se deduzirmos uma fórmula de um conjunto de fórmulas (usando um conjunto de regras de dedução ou axiomas), então podemos dizer que é consequência lógica de , i.e. . Na verdade, há diversos meios de caracterizar o CP como um sistema formal que tem essa propriedade, chamada de correção. Vamos apresentar alguns desses sistemas formais. Para definir um sistema forma , precisamos definir uma 4-tupla em que

• é o conjunto finito alfabeto, contém todos os símbolos necessários para representar fórmulas e literais;
• é o conjunto dos conectivos lógicos ou, mais abstratamente, símbolos de operadores;
• é o conjunto dos axiomas do sistema formal;
• é o conjunto das regras de inferência.

Vamos considerar particularmente dois sistemas formais, um voltado para automatização de deduções e outro para uso humano. O primeiro sistema formal do CP com um sistema axiomático é de autoria de Gottlob Frege, no livro Begriffsschrift, porém apresentaremos uma formulação mais recente cuja autor é Elliott Mendelson (Introduction to Mathematical Logic, 1979), porém essa axiomatização é uma redução do esquema axiomático de lógica ternária de Jan Łukasiewicz.

Na formulação de Mendelson temos em que: é o conjunto finito dos símbolos para fórmulas e meta-fórmulas. Por exemplo, . contém apenas os símbolos e e todos os outros símbolos são abreviações. Portanto fórmulas são construídas indutivamente com os símbolos de . contém apenas uma regra de inferência, chamada modus ponens – de podemos deduzir . Por fim, contém os seguintes meta-axiomas:

1. 
2. 
3. 

O sistema formal descrito acima é muito incomodo para humanos pois as deduções podem resultar em fórmulas muito grandes. Sistemas formais que descrevem o CP com um conjunto de axiomas e poucas regras de inferência estão de acordo com o estilo descrito por David Hilbert no artigo Neubegründung der Mathematik (erste Mitteilung), traduzido livremente como “Reformulações da Matemática (primeira Comunicação”, publicado na revista alemã Gesammelte Abhandlungen em 1922. Em 1934, Gerhard Gentzen publicou um artigo chamado Untersuchungen über das logische Schließen I na revista Mathematische Zeitschrift, a primeira parte de uma dissertação entregue à Universidade de Göttingen contendo uma resposta ao estilo de dedução fundamentado em vários axiomas – o qual, segundo Gentzen, não capturava a essência do raciocínio matemático. Na dissertação, Gentzen descreveu o CP como um sistema formal sem axiomas e com cerca de 20 regras de inferência, cunhando o termo “dedução natural”.

Não apresentaremos o sistema de Gentzen aqui, mas um sistema formal “híbrido” mais recente, formulado por Carnielli, Coniglio e Bianconi em Lógica e Aplicações em Ciência da Computação (2002). Novamente temos tais que contém os símbolos de fórmulas necessários para a discussão, e os símbolos , e são abreviações para as respectivas fórmulas formadas pelas tabelas-verdade, só contém um axioma (que captura a Lei do Meio Excluído) e as regras de inferência são as seguintes:

• Expansão: se uma fórmula qualquer é teorema, é teorema, em que é uma fórmula qualquer. Podemos representar essa regra de inferência através de uma barra horizontal, assim como todas as outras.

• Eliminação: se é teorema, é teorema.

• Associatividade: se é teorema, é teorema.

• Corte: se e são teoremas, é teorema.

Uma prova formal é uma sequência de fórmulas de forma que, para cada , é um axioma ou é deduzido através das regras de inferência utilizando e/ou , com e . Um teorema é a última fórmula de uma prova formal, logo é um teorema, assim como todas as outras fórmulas da prova formal descrita anteriormente – pois podemos “parar” as deduções da prova onde quisermos. Se uma fórmula é um teorema, escrevemos . Se uma fórmula é um teorema, escrevemos . Um sistema formal é decidível se há um algoritmo para verificar se uma fórmula qualquer é teorema dentro do próprio sistema formal. O CP é decidível.

Escrevemos se é dedutível a partir de um conjunto de premissas , ou seja, há uma prova formal de que pode utilizar as fórmulas de como verdadeiras a priori – axiomas.

Note que esse sistema formal não define, por exemplo, a regra modus ponens mas nós podemos deduzi-la e, consequentemente, utilizá-la como teorema. Vamos demonstrar que :

1. , por hipótese.
2. , expansão com 1 e .
3. , por hipótese.
4. , corte  com 2 e 3.
5. , por eliminação.

Podemos escrever essa prova por meio da representação de barras horizontais:

Como é, por definição, , demonstramos que – a regra modus ponens (MP) – e agora podemos usá-la sempre que aplicável. Por exemplo, podemos demonstrar facilmente que , basta aplicar a regra MP repetidamente. Vamos fazer apenas mais uma prova, a comutatividade de , :

1. , por hipótese.
2. , axioma.
3. , corte com 1 e 2.

A representação por linhas horizontais pode ser feita de forma semelhante àquela acima. Outras provas podem ser encontradas aqui.

Agora vamos descrever o Teorema da Dedução. Alguns sistemas formais tomam o Teorema da Dedução como uma regra de inferência, porém não é o caso do sistema formal em que estamos tratando agora. Sejam e fórmulas e um conjunto de fórmulas. O teorema diz que  se e somente se (sse) . O Teorema da Dedução foi formulado e demonstrado independentemente por Jacques Herbrand, no artigo Recherches sur la théorie de la démonstration publicado na revista Travaux de la Societé des Sciences et des Lettres de Varsovie em 1930, e por Alfred Tarski num artigo em Comptes Rendus des Séances de la Société des Sciences et des Lettres de Varsovie, também em 1930. Há um outro teorema chamado Teorema da Eliminação do Corte ou Haupsatz de Gerhard Gentzen, importante para outras formulações do CP e para o Cálculo de Sequentes, porém não discursaremos sobre ele aqui.

A sintaxe do CP não é definida de maneira aleatória, ela tem o objetivo de refletir a semântica do CP e construir teoremas. De fato, o reflexo da semântica está no fato que todo teorema é tautologia. Trata-se do Teorema da Correção:

• Sejam um conjunto de fórmulas e uma fórmula qualquer. Se , então . Ou seja, se é dedutível de , então também é consequência lógica do mesmo conjunto.

O Teorema da Correção é facilmente demonstrável por indução e verificação de casos. Não o demonstraremos aqui mas a ideia geral é mostrar indutivamente como os axiomas do sistema formal (no caso, só temos um) são tautologias e todas as regras de inferência criam outras tautologias. O converso do Teorema da Correção também é verdadeiro e recebe o nome de Teorema da Completude:

• Sejam um conjunto de fórmulas e uma fórmula qualquer. Se , então .

Demonstrar o Teorema da Completude não é tão simples quando demonstrar o Teorema da Correção. Na verdade, a primeira demonstração do Teorema da Completude foi feita por Kurt Gödel em sua tese de doutorado  Über die Vollständigkeit des Logikkalküls, publicada em 1929. Gödel contribuiu imensamente para a Lógica e a sua demonstração do Teorema da Completude é realmente brilhante. Não demonstraremos o teorema aqui, mas demonstrações podem ser encontradas aqui (Teorema 3.4.6, p. 63 – uma demonstração bem curta por contraposição que se fundamenta em vários outros teoremas) e aqui (duas demonstrações, uma construtiva e outra contrapositiva). Alguns autores se referem ao Teorema da Completude como também englobando o Teorema da Correção, mas fazemos a distinção neste artigo.

Através dos teoremas da Correção e Completude podemos chegar a duas conclusões. Primeiramente, o CP é consistente, isto é, não há nenhuma fórmula tal que e são ambos teoremas. Isso deve-se ao fato de que se é teorema, pelo Teorema da Correção, também é tautologia e se é tautologia, não pode ser tautologia pela Lei do Meio Excluído. Segundamente, as questões quanto a satisfabilidade e validade de uma fórmula e se essa mesma fórmula é logicamente equivalente ou consequente de outra fórmula são todos um mesmo problema – novamente segundo os teoremas da Correção e Completude. Portanto vamos agora apresentar dois métodos de verificação de satisfabilidade de fórmulas. Esses métodos se chamam algoritmos de Horn e da Resolução.

Podemos verificar a satisfabilidade de fórmulas de Horn com o algoritmo de Horn (note que nem todas as fórmulas do CP podem ser convertidas para a forma de Horn). A forma de Horn recebe esse nome por ter sido inicialmente objeto de estudo de Alfred Horn, o qual tratou delas no artigo On sentences which are true of direct unions of algebras publicado no Journal of Symbolic Logic em 1951. Uma fórmula está na forma de Horn se está na FNC e contém no máximo um literal ou fórmula atômica sem negação. Por exemplo, a fórmula está na forma de Horn enquanto as fórmulas e não estão. Podemos transformar as fórmulas na forma de Horn em uma conjunção de implicações: basta transformarmos os literais negados em premissas. Exemplificando: nós podemos transformar a fórmula   em .

O Algoritmo de Horn contém três passos, com a entrada sendo uma fórmula na forma de Horn e a saída sendo “sim, a fórmula H é satisfazível” ou “não, a fórmula H não é satisfazível”. Os passos são:

1. Marcar todas as fórmulas que estão nas implicações do tipo .
2. Se há sub-fórmula da forma em que todos os foram marcados e não foi marcado, então marcar . Se ainda há sub-fórmulas do tipo descrito, repetir até não haver mais.
3. Se há alguma sub-fórmula em que todos os foram marcados, então concluir que não é satisfazível. Caso contrário, concluir que é satisfazível.

Uma prova para o algoritmo pode ser encontrada aqui. A demonstração não é muito complexa mas requer a consideração de vários casos. O problema de verificação de satisfabilidade de fórmulas na forma de Horn é conhecido como HORNSAT e é um dos problemas mais “difíceis” a ser P-completo, lembrando que ele não abrange todas as fórmulas do CP. O artigo Linear-time algorithms for testing the satisfiability of propositional horn formulae de William Dowling e Jean Gallier descreve detalhadamente a construção de um algoritmo linear, ou seja, requer “passos” de execução para uma fórmula na forma de Horn com literais.

O Algoritmo da Resolução requer uma fórmula na FNC como entrada e diz se essa fórmula é satisfazível ou não como saída. pode ser escrita como em que cada é uma disjunção de literais, chamada de claúsula. Podemos reescrever em forma de um conjunto de cláusulas . Por exemplo, se , seu respectivo conjunto é . Se temos duas cláusulas e tais que e , a fórmula é chamada de resolvente de e , é o resultado da aplicação da regra do corte. Se deduzirmos o resolvente ou de uma fórmula , ou seja, o conjunto vazio, concluímos que a fórmula é insatisfazível. Isso se deve ao fato de que o conjunto vazio só é deduzido como resolvente de alguma contradição, como por exemplo de , que corresponde à fórmula – uma contradição.

Vamos escrever agora a definição do Algoritmo da Resolução:

1. Seja uma fórmula na FNC escrita como um conjunto de cláusulas, . Construímos uma sequência de conjuntos de forma que e cada é obtido pela inclusão dos resolventes do conjunto anterior, . O algoritmo termina quando não conseguimos obter mais nenhum resolvente. Chamaremos o conjunto final de , formado por todos os possíveis resolventes criados pelas premissas em .
2. Se , dizemos que é insatisfazível. Caso contrário, é satisfazível.

Observe que na verdade é mais fácil para humanos verificar se uma fórmula é insatisfazível através do Algoritmo da Resolução. Mas se considerarmos uma fórmula , aplicarmos o Algoritmo da Resolução em e obtermos como um resolvente, podemos concluir que é satisfazível pela Lei do Meio Excluído. Logo se quisermos verificar se uma fórmula é satisfazível, é mais simples verificar se a sua negação é insatisfazível.

Para verificarmos se uma fórmula é consequência lógica de um conjunto de cláusulas ou, equivalentemente, é dedutível de podemos aplicar o Algoritmo da Resolução da seguinte maneira: se , pelo Teorema da Completude, e, pelo Teorema da Dedução, . Para verificar se é satisfazível, devemos aplicar o Algoritmo da Resolução em e verificar se o resolvente foi deduzido.

Não demonstraremos o algoritmo neste artigo, mas uma discussão acerca do Algoritmo da Resolução e outras técnicas para resolver o problema de satisfabilidade encontra-se no artigo Resolution vs Search: Two Strategies for SAT, de Irina Rish e Rina Dechter, e também nos slides de Fahiem Bacchus.

Terminamos, enfim, uma apresentação superficial porém introdutória de lógica matemática e Cálculo Proposicional. Os algoritmos que descrevemos são facilmente implementáveis em computadores (exemplos de implementação são CARINE, Gandalf e Prover9 e linguagens de programação que utilizam esses algoritmos incluem Prolog e Coq), por serem mecânicos e feitos para automatização. Em outras palavras, o uso de computadores para criação e verificação de provas matemáticas é algo muito recente e interessante para a matemática e até ocasionou a criação de um novo campo – a teoria dos tipos. Por fim, recomendamos a leitura do artigo Proofs are Programs: 19th Century Logic and 21st Century Computing, de Philip Wadler.

---

Hedman, S. (2004). A first course in logic : an introduction to model theory, proof theory, computability, and complexity. Oxford New York: Oxford University Press.

Rautenberg, W. (2010). A concise introduction to mathematical logic. New York: Springer.

Oliveira, J. G. de (2016). Lógica para Computação. Sorocaba: Universidade Federal de São Carlos.