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, por meio de Tableaux semântico, se a fórmula
é válida (isto é, tautologia) e, caso não fosse, encontrar um contraexemplo. Para mostrar validade via tableaux, testamos a insatisfatibilidade da negação da fórmula.
Passo 2
Escrevemos a negação da fórmula principal como fórmula inicial no tableau:
e vamos decompor passo a passo.
Passo 3
Aplicamos a regra de negação de implicação:
Aqui
é
e
é
. Logo obtemos duas fórmulas conjuntas:
Passo 4
Decompomos a negação de disjunção em conjunção de negações:
Isto gera:
Em seguida simplificamos duplas negações:
Passo 5
Agora restou a fórmula
. A negação de conjunção se decompõe em disjunção de negações:
Isto gera duas ramificações no tableau:
Ramo 1:
Ramo 2:
Em ambas as ramificações mantemos também as fórmulas
(6) e
(7).
Passo 6
Verificamos cada ramo:
- Ramo 1 contém
e (contradição). - Ramo 2 contém
e (contradição).
Ambos os ramos fecham. Como não há ramo aberto, a negação da fórmula é insatisfatível.
Resposta
A fórmula
é válida (tautologia).