🌲 árvores de refutação · tableaux semânticos

O método de tableaux semânticos (ou árvores de refutação) é um procedimento de prova utilizado para verificar a validade de argumentos lógicos e a satisfabilidade de fórmulas. Ele funciona por refutação: para provar que uma fórmula é válida, mostramos que sua negação leva a uma contradição em todos os ramos da árvore. É um método intuitivo e mecânico, aplicável tanto à lógica proposicional quanto à de primeira ordem.

🔍 princípio do método

Dada uma fórmula \(\varphi\), queremos saber se ela é uma tautologia (sempre verdadeira). Construímos um tableau para \(\neg\varphi\). Se todas as ramificações fecharem (contiverem uma contradição como \(P\) e \(\neg P\)), então \(\neg\varphi\) é insatisfatível, logo \(\varphi\) é válida. Se algum ramo permanecer aberto, temos um contraexemplo.

\(\text{Para provar } \vDash \varphi,\text{ mostramos que } \neg\varphi \text{ leva à contradição em todos os ramos.}\)

📐 regras de expansão (lógica proposicional)

Cada conectivo tem regras que expandem a árvore. As fórmulas são marcadas como verdadeiras (\(T\)) ou falsas (\(F\)), mas normalmente usamos a própria fórmula para indicar que queremos torná-la verdadeira, e sua negação para falsa. Abaixo, as regras no estilo tableaux:

Conjunção (\(T\alpha\))

\(T(P \land Q)\)
↓
\(T P\)
\(T Q\)

(ambos devem ser verdadeiros)

Disjunção (\(T\beta\))

\(T(P \lor Q)\)
↙ ↘
\(T P\) \(T Q\)

(bifurcação)

Condicional (\(T(P \rightarrow Q)\))

equivale a \(T(\neg P \lor Q)\)
↙ ↘
\(F P\) \(T Q\)

Bicondicional (\(T(P \leftrightarrow Q)\))

↙ ↘
\(T P, T Q\) \(F P, F Q\)

Negação (\(F \neg P\))

\(F \neg P\) → \(T P\)

Para fórmulas falsas (\(F\)), aplicamos regras análogas (ex.: \(F(P \land Q)\) bifurca em \(F P\) e \(F Q\)).

🧩 exemplo: validade de \((P \rightarrow Q) \rightarrow (\neg Q \rightarrow \neg P)\)

Vamos provar que esta fórmula é uma tautologia. Começamos negando-a e construindo o tableau.

1. \(F((P \rightarrow Q) \rightarrow (\neg Q \rightarrow \neg P))\) (hipótese)

2. \(T(P \rightarrow Q)\) (de 1, regra para \(F(\alpha \rightarrow \beta)\): \(T\alpha\) e \(F\beta\))

3. \(F(\neg Q \rightarrow \neg P)\) (de 1)

4. \(T \neg Q\) (de 3: \(F(\alpha \rightarrow \beta)\) ⇒ \(T\alpha\) e \(F\beta\))

5. \(F \neg P\) (de 3)

6. \(F Q\) (de 4: \(T \neg Q\) ⇒ \(F Q\))

7. \(T P\) (de 5: \(F \neg P\) ⇒ \(T P\))

8. Agora, de 2 (\(T(P \rightarrow Q)\)), temos bifurcação:

Ramo esquerdo: \(F P\) (contradiz 7: \(T P\) e \(F P\)) → fechado.
Ramo direito: \(T Q\) (contradiz 6: \(F Q\) e \(T Q\)) → fechado.

Ambos os ramos fecham. Logo, a fórmula original é válida.

🌐 extensão para primeira ordem

Para quantificadores, acrescentam-se regras com instanciação:

• \(T \forall x P(x)\): instancie com um termo ainda não usado no ramo (constante nova).
• \(F \forall x P(x)\): introduza uma constante (ou termo) e escreva \(F P(c)\).
• \(T \exists x P(x)\): introduza uma constante nova \(c\) e escreva \(T P(c)\).
• \(F \exists x P(x)\): para qualquer termo, escreva \(F P(t)\) (mas cuidado com a ordem).

O método pode gerar ramos infinitos em alguns casos, mas é completo para lógica de primeira ordem.

🔬 exemplo: validade de \(\forall x P(x) \rightarrow \exists x P(x)\)

Negamos: \(T \forall x P(x)\) e \(F \exists x P(x)\).

1. \(F(\forall x P(x) \rightarrow \exists x P(x))\)

2. \(T \forall x P(x)\) (de 1)

3. \(F \exists x P(x)\) (de 1)

4. De 2, instancie com uma constante \(a\): \(T P(a)\)

5. De 3, instancie com \(a\): \(F P(a)\) (pois \(F \exists x P(x)\) significa \(\forall x \neg P(x)\)).

Contradição entre 4 e 5. Ramo fechado. Logo, a fórmula é válida.

⚡ vantagens e aplicações

• Intuitivo: simula a busca por um contraexemplo.
• Decisivo para lógica proposicional: sempre termina.
• Completo para primeira ordem: se a fórmula é válida, o tableau fecha (teorema da completude).
• Útil em ensino: fácil de entender e aplicar manualmente.
• Base para provadores automáticos: implementações como tableaux com backjumping.

⚠️ limitações

Em lógica de primeira ordem, o tableau pode não terminar para fórmulas inválidas (o método é apenas semidecidível). Estratégias de instanciação precisam ser escolhidas com cuidado para evitar loops infinitos.

🔄 tableaux vs. dedução natural

Enquanto a dedução natural constrói a prova a partir das premissas, o tableau prova por refutação. Ambos são equivalentes em poder expressivo, mas o tableau é muitas vezes mais mecânico e adequado para implementação computacional.

\(\displaystyle \text{Tableaux fechado} \iff \text{fórmula é válida}\)

✦ “A refutação é o caminho para a verdade.” ✦