Lógica de Predicados

A lógica proposicional não consegue expressar "todo elemento da lista é positivo" — ela trata cada proposição como um átomo sem estrutura interna. A lógica de predicados (ou de primeira ordem) acrescenta o que falta: variáveis, predicados e quantificadores.

É a linguagem em que se escrevem especificações de programas, invariantes de laço e restrições de banco de dados.

Predicados

Um predicado é uma afirmação com variáveis livres, que só vira proposição quando as variáveis recebem valores. $P(x)$: "$x$ é primo" não tem valor de verdade; $P(7)$ tem.

Predicados podem ter várias variáveis: $D(x, y)$ para "$x$ divide $y$".

Quantificadores

O quantificador sempre percorre um domínio. "$\forall x, (x^2 \ge 0)$" é verdadeiro nos reais e falso nos complexos. Omitir o domínio é a fonte mais comum de ambiguidade numa especificação.

Dois casos-limite valem memorizar: sobre o domínio vazio, todo enunciado universal é verdadeiro e todo existencial é falso. Isso explica all([]) == True e any([]) == False.

Negação de quantificadores

As regras são o análogo direto de De Morgan, e são as mais usadas na prática:

Em português: negar "todos são pares" dá "existe um ímpar" — e não "todos são ímpares". A negação de uma propriedade universal é a existência de um contraexemplo, o que é a base de toda refutação matemática e de todo teste que encontra um defeito.

A ordem dos quantificadores importa

Este é o ponto que mais gera confusão, e vale um exemplo concreto. Seja $A(x, y)$ o predicado "$y$ é maior que $x$" sobre os inteiros:

• $\forall x, \exists y, A(x, y)$ — "para todo $x$ existe algum $y$ maior". Verdadeiro: basta tomar $y = x + 1$, e o $y$ pode depender de $x$.
• $\exists y, \forall x, A(x, y)$ — "existe um $y$ maior que todos os $x$". Falso: exigiria um inteiro maior que qualquer outro.

Trocar a ordem mudou o valor de verdade. A regra prática: no primeiro caso a escolha de $y$ pode depender de $x$; no segundo, o mesmo $y$ tem de servir para todos.

Essa distinção aparece direto em engenharia. "Toda requisição tem um servidor que a atende" é bem diferente de "existe um servidor que atende todas as requisições" — a primeira descreve um balanceador, a segunda um ponto único de falha.

Escopo e variáveis livres

Uma variável é ligada quando está sob o alcance de um quantificador, e livre caso contrário. Em

$$\forall x, (P(x) \wedge Q(y))$$

$x$ é ligada e $y$ é livre. Uma fórmula sem variáveis livres é uma sentença e tem valor de verdade definido; com variáveis livres, ela é um predicado.

A analogia com programação é exata: quantificador está para variável ligada assim como declaração de parâmetro está para variável local. Renomear a variável ligada não muda o significado, como renomear um parâmetro não muda a função.

Exemplo trabalhado: especificando uma busca

Especificar indice = busca(lista, alvo):

$$\text{Se } \exists i, (0 \le i < n \wedge L[i] = alvo), \text{ então } L[\mathit{indice}] = alvo$$ $$\text{Se } \neg\exists i, (0 \le i < n \wedge L[i] = alvo), \text{ então } \mathit{indice} = -1$$

Aplicando a negação do existencial, a segunda condição vira $\forall i, (0 \le i < n \to L[i] \ne alvo)$ — que é exatamente o invariante que o laço da busca linear mantém a cada iteração.

Aplicações em computação

Invariantes de laço. A prova de correção de um laço consiste em mostrar que um predicado vale antes da primeira iteração, é preservado por cada iteração e, junto com a negação da condição de parada, implica a pós-condição.

Contratos. Pré e pós-condições em ferramentas de verificação (Dafny, JML, Frama-C) são fórmulas de primeira ordem sobre o estado do programa.

SQL. EXISTS e NOT EXISTS são quantificadores literais; WHERE NOT EXISTS (...) é a tradução direta de $\neg\exists$. A divisão relacional — "clientes que compraram todos os produtos" — é um $\forall$ implementado como dupla negação.

Prolog e programação lógica. Um programa é um conjunto de cláusulas de primeira ordem, e a execução é busca por prova.

Resolvedores SMT. Ferramentas como Z3 decidem satisfatibilidade de fórmulas de primeira ordem sobre teorias (inteiros, vetores de bits, arranjos) e são o motor de muitos verificadores modernos^[ref] .

Erros comuns

• Trocar a ordem dos quantificadores e supor que o significado se mantém.
• Esquecer o domínio. "$\forall x, (x > 0 \to \sqrt{x} \text{ está definido})$" depende de estarmos nos reais.
• Negar só o predicado. A negação de $\forall x, P(x)$ não é $\forall x, \neg P(x)$.
• Usar $\wedge$ com $\forall$ em vez de $\to$. "Todo primo maior que 2 é ímpar" é $\forall x,(P(x) \wedge x>2 \to I(x))$; escrever $\forall x,(P(x) \wedge x>2 \wedge I(x))$ afirma que todo objeto do domínio é um primo ímpar maior que 2.
• Supor que primeira ordem decide tudo. Validade em lógica de primeira ordem é indecidível — resolvedores são incompletos ou podem não terminar.

Herbert B. Enderton (2001). A Mathematical Introduction to Logic. Academic Press. DOI: 10.1016/c2009-0-22107-6. Michael Huth and Mark Ryan (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press. DOI: 10.1017/cbo9780511810275.

Referências

1. Herbert B. Enderton (2001). A Mathematical Introduction to Logic. Academic Press.
2. Michael Huth; Mark Ryan (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.