Defina se os argumentos abaixo são válidos com Tableaux. Caso não sejam, mostre o contraexemplo.
Passo 1
O enunciado pede para verificar, usando tableaux semânticos, se o seguinte argumento é válido:
.
O método de tableaux testa a validade mostrando que as fórmulas das premissas, junto com a negação da conclusão, formam um conjunto insatisfatível.
O método de tableaux testa a validade mostrando que as fórmulas das premissas, junto com a negação da conclusão, formam um conjunto insatisfatível.
Passo 2
Formulamos o conjunto para o tableau como
ou seja,
Se todo ramo do tableau fechar, concluímos que não há modelo para esse conjunto, logo o argumento é válido.
Passo 3
Iniciamos o tableau e aplicamos a regra de disjunção em
, gerando dois ramos:
- Ramo 1 assume
. - Ramo 2 assume
.
Em ambos os ramos também carregamos
,
e .
e
Passo 4
Expandimos cada ramo:
Ramo 1 (
é verdadeiro):
- De
e obtemos . - De
obtemos simultaneamente e . - Logo aparece
e : ramo fechado.
Ramo 2 (
é verdadeiro):
- De
e obtemos . - De
já tínhamos . - Logo aparece
e : ramo fechado.
Como todos os ramos fecharam, o tableau é completamente fechado.
Resposta
O argumento é válido.