Verifique a validade dos argumentos, usando tableaux semânticos ou resolução
Passo 1
Enunciado: Verificar a validade do argumento com as premissas
,
,
e conclusão
. O conteúdo é lógica proposicional e vamos usar o método de tableaux semântico, que consiste em assumir as premissas verdadeiras e a negação da conclusão e ver se todas as ramificações levam a contradição.
Passo 2
Montamos o tableau com as fórmulas abaixo, todas assumidas como verdadeiras exceto a conclusão que aparece negada:
Passo 3
Decompomos
usando a regra de negação de disjunção, que gera simultaneamente:
Passo 4
Decompomos a implicação
usando a regra
equivale a
. No tableau, isso gera uma ramificação com:
ramo 1:
ramo 2:
ramo 1:
ramo 2:
Passo 5
Decompomos a disjunção
usando a regra de disjunção, que gera duas ramificações em cada nó em que ela aparece:
ramo 1a (do ramo 1):
ramo 1b (do ramo 1):
ramo 1a (do ramo 1):
ramo 1b (do ramo 1):
Passo 6
Analisamos cada ramo:
No ramo 1a temos que se decompõe em
e
. Mas também temos
como premissa, logo
e
geram uma contradição e o ramo fecha.
No ramo 1b temos gerando
e
. Mas o ramo 1b traz
como hipótese, gerando
e
, contradição, então fecha.
No ramo 2 temos e também
(da negação da conclusão), o que é contradição, então esse ramo também fecha.
No ramo 1a temos
No ramo 1b temos
No ramo 2 temos
Resposta
Todas as ramificações do tableau fecham, logo o argumento é válido.