Laboratório de
Árvores Lógicas

A Lógica Proposicional Clássica (CPL, também referida como Cálculo Proposicional Clássico ou Lógica Bivalente) é o sistema formal que estuda as relações de inferência entre proposições compostas a partir de conectivos veritativo-funcionais — negação, conjunção, disjunção, condicional e bicondicional — aplicados a proposições atômicas cujo valor de verdade é fixado independentemente do conectivo utilizado. É o sistema proposicional de referência: aceita integralmente os princípios da Não-Contradição, do Terceiro Excluído e da Explosão (ex falso quodlibet), e funciona como o "caso zero" a partir do qual quase todas as lógicas não clássicas se definem por comparação — seja por enfraquecimento (intuicionista, paraconsistente, paracompleta, multivalorada), seja por extensão (modal, temporal, de descrição).

A origem da CPL não pode ser atribuída a um único autor: resulta de um processo cumulativo que começa na lógica algébrica de George Boole (Mathematical Analysis of Logic, 1847; An Investigation of the Laws of Thought, 1854), passa pela primeira formalização rigorosa de um cálculo proposicional numa linguagem simbólica plenamente artificial — a Begriffsschrift de Gottlob Frege (1879) — e se consolida na apresentação axiomática de Whitehead e Russell nos Principia Mathematica (1910-1913), cujo cálculo das "proposições elementares" viria a ser isolado e estudado autonomamente. É exatamente esse fragmento que Emil Post trata com rigor semântico em sua tese de doutorado, publicada como "Introduction to a General Theory of Elementary Propositions" (American Journal of Mathematics, 1921): Post introduz as tabelas de verdade como técnica sistemática de decisão e demonstra a completude do cálculo proposicional de Principia. No mesmo ano, Ludwig Wittgenstein chega independentemente ao mesmo dispositivo no Tractatus Logico-Philosophicus, associando-o a uma leitura da proposição como figuração (Bild) dos fatos possíveis.

Convém separar três camadas na história da CPL, que frequentemente se confundem em apresentações apressadas: (i) a construção do sistema sintático-dedutivo — obra coletiva de Boole, Frege, Russell e Whitehead; (ii) a semântica bivalente por tabelas de verdade — devida independentemente a Post e a Wittgenstein, ambos em 1921; e (iii) o método de tableaux semânticos, que surge apenas décadas depois, com Evert Beth ("Semantic entailment and formal derivability", 1955) e, por via distinta — os "conjuntos-modelo" (model sets) —, com Jaakko Hintikka, também em 1955. A apresentação hoje padrão em manuais — fórmulas assinaladas com T/F, regras α não ramificantes e regras β ramificantes — deve-se à sistematização de Raymond Smullyan em First-Order Logic (1968), que unifica e simplifica as propostas de Beth e Hintikka num único cálculo elegante.

O problema que motivou a emergência da CPL como disciplina autônoma foi duplo: de um lado, o projeto logicista de reduzir a aritmética à lógica (Frege, Russell), que exigia um cálculo proposicional explícito e livre de ambiguidade; de outro, a busca por um critério mecânico de validade — o que Hilbert chamaria de Entscheidungsproblem — que a tabela de verdade de Post resolve completamente para o caso proposicional, ao demonstrar que a validade de qualquer fórmula é decidível por um procedimento finito e puramente combinatório.

Semanticamente, a CPL assume que toda proposição atômica recebe exatamente um entre dois valores, verdadeiro (V) ou falso (F), e que o valor de qualquer fórmula composta é determinado unicamente pelos valores de suas partes através das cláusulas veritativo-funcionais usuais dos conectivos. Uma valoração v é uma função total das fórmulas atômicas em {V,F}, estendida homomorficamente aos conectivos. Uma fórmula é consequência lógica de um conjunto Γ se toda valoração que torna verdadeiras todas as fórmulas de Γ também torna verdadeira a fórmula em questão — não há espaço para valorações parciais, múltiplos valores ou mundos possíveis alternativos.

O método de tableaux para a CPL trabalha com fórmulas assinaladas: TA significa "supõe-se A verdadeira", FA significa "supõe-se A falsa". A partir do conjunto de fórmulas que se quer testar, aplicam-se regras de expansão que decompõem cada fórmula assinalada em fórmulas assinaladas mais simples. As regras α — como T(A∧B), que gera TA e TB na mesma linha sem ramificar — preservam um único ramo; as regras β — como T(A∨B), que gera dois ramos, um com TA e outro com TB — multiplicam os ramos, representando uma disjunção de possibilidades semânticas. Um ramo fecha quando contém simultaneamente TA e FA para alguma fórmula A; um tableau inteiro fecha quando todos os seus ramos fecham. Um ramo está saturado quando todas as regras aplicáveis às suas fórmulas já foram aplicadas; se um ramo saturado permanece aberto, ele fornece diretamente um contramodelo, atribuindo V a toda fórmula atômica assinalada com T e F a toda fórmula atômica assinalada com F nesse ramo. Como não há operadores modais, quantificadores ou construções que gerem cópias indefinidas de uma mesma fórmula, o tableau proposicional clássico sempre termina em número finito de passos: cada regra reduz estritamente a complexidade sintática da fórmula tratada, dispensando qualquer mecanismo de bloqueio ou controle de ciclos.

Como exemplo de fórmula válida, considere-se a Lei de Peirce, ((p→q)→p)→p — válida na CPL, mas não na lógica intuicionista, o que a torna um teste clássico de distinção entre os dois sistemas: seu tableau fecha em todos os ramos, mostrando que nenhuma valoração bivalente pode torná-la falsa. Como exemplo de fórmula inválida, considere-se p→(q∧¬q): o tableau que testa sua validade abre um ramo contendo Tp e Fq simultaneamente satisfazíveis sem contradição, fornecendo o contramodelo v(p)=V, v(q)=F, que de fato torna o condicional falso — confirmando que a fórmula não é uma tautologia, embora seja satisfazível sob outras atribuições (por exemplo, v(p)=F).