Resolva pelo método de Tableaux
Passo 1
O enunciado pede para verificar, pelo método de Tableaux, se
Em Tableaux de proposições, assumimos as premissas verdadeiras e a conclusão falsa, e aplicamos as regras de decomposição para
,
e
.
Passo 2
Montamos a raiz do Tableaux com as fórmulas marcadas como verdadeiras (T) ou falsas (F):
T:
T:
F: A regra para F
gera:
T:
F: Portanto, no nível 0 temos:
T: , T:
, T:
, F:
.
T:
T:
F:
T:
F:
T:
Passo 3
Aplicamos T
em T:
. A regra T
gera dois ramos:
- F:
- T:
Passo 4
No ramo 1) aparece F:
junto com T:
(vindo de F:
), o que fecha esse ramo por contradição.
Passo 5
No ramo 2) temos agora as fórmulas:
T: , T:
, T:
, F:
.
T:
Expandimos T:
(regra T
) em dois subramos:
2.1) T:
2.2) T:
2.1) T:
2.2) T:
Passo 6
Considere o subramo 2.1) com T:
. Expandimos então T:
(regra T
) em:
2.1.a) F:
2.1.b) T: - No 2.1.b) temos T:
contra F:
, o que fecha esse subramo.
2.1.a) F:
2.1.b) T:
- No 2.1.a) F:
se decompõe (regra F ) em dois ramos: - 2.1.a.i) F:
, que fecha com T: . - 2.1.a.ii) F:
, que não gera mais contradições nem abre novas regras.
Logo, o subramo 2.1.a.ii) permanece aberto.
Passo 7
O ramo aberto corresponde à atribuição
que satisfaz T:
e T:
, mas falsifica
. Portanto o Tableaux não fecha completamente.
Resposta
O sequent não é válido. Um contraexemplo é
pois então