Resolva pelo método de Tableaux
Passo 1
Vamos mostrar que
é válido pelo método de Tableaux, isto é, assumimos sua negação e provamos que todo ramo fecha.
Passo 2
Negamos a fórmula e aplicamos a regra de
:
Gera as fórmulas
Em seguida aplicamos de novo
na segunda:
Passo 3
Agora expandimos cada existencial usando a mesma constante nova
:
Passo 4
Expandimos a implicação
criando dois ramos:
- Ramo 1:
- Ramo 2:
No ramo 1 há
e
, contradição.
No ramo 2 há e
, contradição.
No ramo 2 há
Todos os ramos fecham, portanto a negação leva a contradição.
Resposta
A fórmula
é válida.