Resolva pelo método de Tableaux
Passo 1
O enunciado pede para testar a validade da fórmula
usando o método semântico de tableaux em lógica de primeira ordem. Vamos precisar das regras de tableaux para a implicação, para negação de quantificador universal e para os quantificadores ∀ e ∃.
Passo 2
Para verificar se a fórmula é válida, começamos negando-a. Colocamos no ramo inicial:
Passo 3
Decompondo 2.:
- A regra para
gera . - Em seguida aplicamos a regra ∃, introduzindo uma constante nova
, e obtemos
-
.
- Finalmente usamos a regra α para
, que dá simultaneamente
Passo 4
Agora decompondo 1. que é uma implicação β:
- Ramo 4.1:
- Ramo 4.2:
Em ambos os ramos ficam as fórmulase .
Passo 5
Ramo 4.1
:
- Regra para
gera . - Instanciamos com constante nova
, obtendo
-
.
Não sobra mais regra aplicável e não há contradição entree a implicação original. Esse ramo fica aberto.
Ramo 4.2
:
- Regra ∀ dá
. - Com
e surge contradição, fechando esse ramo.
Passo 6
Como há um ramo aberto, o tableau não fecha, o que mostra que a negação da fórmula é satisfatível. Logo a fórmula original não é válida em lógica de primeira ordem.
Do ramo aberto extraímos um contra-modelo:
Do ramo aberto extraímos um contra-modelo:
Nesse modelo
é verdade (antecedente falso), mas
é falso em
.
Resposta
A fórmula
não é válida. Um contra-modelo é dado por