Verifique a propriedade indicada das seguintes fórmulas através de Tableaux:
(
)
(
), validade, mostrando, caso não seja, um contraexemplo.
(
Passo 1
O enunciado pede para verificar se a fórmula
é válida, usando o método de tableaux semântico. Para mostrar validade, constrói-se o tableau para a negação da fórmula e prova-se que todas as ramificações fecham (logo, a negação é insatisfatível).
Passo 2
Começamos com a negação da fórmula alvo:
Aplicando a regra de negação de implicação
, obtemos os ramos simultâneos
Passo 3
Agora expandimos 2) de novo como negação de implicação, com
e
:
Isto gera as fórmulas literais
3.1)
3.2) , que por dupla negação dá
.
No ramo temos então o conjunto
3.1)
3.2)
No ramo temos então o conjunto
Passo 4
Expandimos
usando a regra de implicação
, o que gera duas sub-ramificações:
• Ramo 1 com . Atribuindo ao conjunto:
, há
e
juntos → contradição → ramo fecha.
• Ramo 2 com . Atribuindo ao conjunto:
, há
e
juntos → contradição → ramo fecha.
• Ramo 1 com
• Ramo 2 com
Passo 5
Como ambas as ramificações fecharam, o tableau para
está completamente fechado. Isso mostra que a negação da fórmula é insatisfatível, logo a fórmula original é válida (tautologia).
Resposta
A fórmula
é válida.