Lógica Proposicional
compiladores, verificacao-formal, algoritmos basico matematica-discreta, logicaLógica Proposicional
A lógica proposicional é o sistema formal mais simples capaz de expressar raciocínio. Para quem programa, ela não é um tópico abstrato: é a semântica exata do if. Toda condição de desvio, toda cláusula WHERE de SQL, todo circuito combinacional é uma fórmula proposicional.
Proposições e conectivos
Uma proposição é uma sentença à qual se pode atribuir um único valor de verdade: verdadeiro ($V$) ou falso ($F$). "$2 + 2 = 4$" é proposição; "feche a porta" não é.
Proposições se combinam por conectivos:
| Conectivo | Símbolo | Leitura | Em código |
|---|---|---|---|
| Negação | $\neg p$ | não $p$ | !p |
| Conjunção | $p \wedge q$ | $p$ e $q$ | p && q |
| Disjunção | $p \vee q$ | $p$ ou $q$ | p || q |
| Condicional | $p \to q$ | se $p$, então $q$ | !p || q |
| Bicondicional | $p \leftrightarrow q$ | $p$ se e somente se $q$ | p == q |
Tabelas-verdade
A semântica de cada conectivo é dada exaustivamente:
| $p$ | $q$ | $\neg p$ | $p \wedge q$ | $p \vee q$ | $p \to q$ | $p \leftrightarrow q$ |
|---|---|---|---|---|---|---|
| V | V | F | V | V | V | V |
| V | F | F | F | V | F | F |
| F | V | V | F | V | V | F |
| F | F | V | F | F | V | V |
A coluna do condicional é a que causa mais estranheza. $p \to q$ só é falso quando a premissa é verdadeira e a conclusão falsa. Se a premissa é falsa, a implicação é verdadeira por vacuidade — "se a lista for vazia, todos os seus elementos são positivos" é uma afirmação verdadeira.
Isso não é um capricho: é o que faz all([]) retornar True em Python e o que torna um laço for sobre coleção vazia consistente com sua pós-condição.
Tautologias, contradições e satisfatibilidade
Uma fórmula é tautologia se é verdadeira sob toda atribuição, contradição se é falsa sob todas, e satisfatível se existe ao menos uma atribuição que a torna verdadeira.
$$p \vee \neg p \quad \text{(tautologia)} \qquad p \wedge \neg p \quad \text{(contradição)}$$
Decidir se uma fórmula proposicional é satisfatível é o problema SAT — o primeiro problema demonstrado NP-completo, e o motor por trás de verificadores de modelo, resolvedores de restrições e otimizadores de compilador.
Equivalências fundamentais
Duas fórmulas são equivalentes ($\equiv$) quando têm a mesma tabela-verdade.
| Nome | Equivalência |
|---|---|
| Dupla negação | $\neg\neg p \equiv p$ |
| De Morgan | $\neg(p \wedge q) \equiv \neg p \vee \neg q$ |
| De Morgan | $\neg(p \vee q) \equiv \neg p \wedge \neg q$ |
| Distributiva | $p \wedge (q \vee r) \equiv (p \wedge q) \vee (p \wedge r)$ |
| Contrapositiva | $p \to q \equiv \neg q \to \neg p$ |
| Definição de $\to$ | $p \to q \equiv \neg p \vee q$ |
| Absorção | $p \vee (p \wedge q) \equiv p$ |
De Morgan é a mais usada na prática. Negar uma condição composta troca o conectivo e nega cada parte:
# estas duas condições são a mesma coisa
if not (idade >= 18 and tem_documento):
if idade < 18 or not tem_documento:A contrapositiva também aparece o tempo todo: "se o cache está válido, o dado está atualizado" equivale a "se o dado está desatualizado, o cache não está válido". Trocar a implicação pela contrapositiva costuma ser a forma mais simples de reescrever uma pré-condição difícil de testar.
Note o segundo símbolo: a recíproca $q \to p$ não é equivalente. Confundir as duas é a falácia lógica mais comum que existe.
Formas normais
Toda fórmula pode ser reescrita em duas formas canônicas:
- FNC (forma normal conjuntiva): conjunção de cláusulas, cada uma uma disjunção de literais — $(p \vee \neg q) \wedge (r \vee q)$.
- FND (forma normal disjuntiva): disjunção de termos conjuntivos — $(p \wedge r) \vee (\neg q \wedge r)$.
A FNC é o formato de entrada padrão dos resolvedores SAT. A conversão direta pode explodir exponencialmente em tamanho; na prática usa-se a transformação de Tseitin, que introduz variáveis auxiliares e mantém o crescimento linear preservando satisfatibilidade.
Exemplo trabalhado
Verificar se $(p \to q) \wedge (q \to r) \to (p \to r)$ é tautologia — a regra do silogismo hipotético.
Em vez da tabela de 8 linhas, use a estratégia de refutação: suponha que a fórmula seja falsa. Então o antecedente é verdadeiro e $p \to r$ é falso. De $p \to r$ falso vem $p = V$ e $r = F$. De $p \to q$ verdadeiro com $p = V$ vem $q = V$. Mas então $q \to r$ é $V \to F$, ou seja, falso — contradizendo a hipótese de que o antecedente inteiro era verdadeiro.
Não há atribuição que falsifique a fórmula, logo ela é tautologia. Esse raciocínio por refutação é exatamente o que um resolvedor SAT automatiza.
Aplicações em computação
Otimização de código. Compiladores simplificam condições usando as equivalências acima. if (!(a && b)) vira if (!a || !b), e ramos cuja condição se reduz a contradição são eliminados como código morto.
Avaliação em curto-circuito. && e || na maioria das linguagens não avaliam o segundo operando quando o primeiro já decide o resultado. Isso preserva a semântica lógica, mas não preserva efeitos colaterais — é por isso que if (init() && check()) pode não chamar check().
Circuitos digitais. Uma porta lógica é a realização física de um conectivo. Minimizar uma expressão booleana com mapas de Karnaugh ou o algoritmo de Quine-McCluskey é reduzir literalmente a contagem de transistores.
Verificação formal. Model checkers traduzem propriedades de programas em fórmulas cuja insatisfatibilidade prova a ausência de um defeito[ref] .
Bancos de dados. O otimizador de consultas reescreve predicados WHERE com as mesmas leis, empurrando filtros para perto da leitura dos dados.
Erros comuns
- Confundir recíproca com contrapositiva. De "se chove, a rua molha" não se conclui "se a rua molha, choveu".
- Negar mal uma conjunção. A negação de "$a$ e $b$" é "não $a$ ou não $b$", não "não $a$ e não $b$".
- Ler o "ou" como exclusivo. Em lógica, $p \vee q$ é verdadeiro quando ambos são verdadeiros. O ou exclusivo é outro conectivo, $p \oplus q$.
- Achar que implicação é causalidade. $p \to q$ é uma relação entre valores de verdade, não uma afirmação de que $p$ causa $q$.
Michael Huth and Mark Ryan (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press. DOI: 10.1017/cbo9780511810275. Kenneth H. Rosen (2019). Discrete Mathematics and Its Applications. McGraw-Hill. ISBN 9781259676512.
Referências
- Michael Huth; Mark Ryan (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
- Kenneth H. Rosen (2019). Discrete Mathematics and Its Applications. McGraw-Hill.