Verifique a validade dos seguintes argumentos, utilizando o tableaux.
Passo 1
Resumindo, queremos verificar se o argumento
é válido. Pelo método do tableaux semântico, assumimos todas as premissas verdadeiras e a conclusão falsa e mostramos que isso leva a contradições em todas as ramificações.
Passo 2
Escrevemos as fórmulas assinadas:
T ,
T ,
T ,
F .
T
T
T
F
Passo 3
Expandimos T
(regra β:
gera duas ramificações):
- Ramificação 1: F
- Ramificação 2: T
Em cada uma mantemos também T , T e F .
Passo 4
Na Ramificação 1 aplicamos F
(regra α:
gera F
e F
):
- Obtemos F
e F . - Mas F
é α de negação, dá T .
Logo nesta ramificação temos as assinaturas:
T, T , F , F , T .
Passo 5
Ainda na Ramificação 1, expandimos T
(regra β):
- Subramo 1.1: F
Aqui Fe T se chocam → fechamento. - Subramo 1.2: T
Aqui Te T se chocam → fechamento.
Portanto toda a Ramificação 1 fecha.
Passo 6
Na Ramificação 2 tínhamos já T
e F
, o que é um choque imediato → fechamento.
Como todas as ramificações fecharam, o conjunto é insatisfatível e o argumento é válido.
Resposta
O argumento é válido.