Verifique a propriedade indicada das seguintes fórmulas através de Tableaux:
, satisfatibilidade, mostrando, caso seja, o modelo para a fórmula.
Passo 1
O enunciado pede verificar, via método de Tableaux, a satisfatibilidade da fórmula
O conteúdo é lógica proposicional e o que precisamos é montar um Tableau semântico assumindo a fórmula verdadeira, aplicar as regras de conjunção (não ramifica) e disjunção (ramifica) e identificar se existe algum ramo aberto. Se houver ramo aberto, a fórmula é satisfatível e podemos extrair um modelo atribuindo aos átomos os valores indicados pelos literais do ramo.
Passo 2
Assumimos a fórmula inteira como verdadeira e aplicamos a regra de conjunção em cascata. De
extraímos na mesma ramificação os três componentes:
Em particular, de
tiramos
e
no ramo. Até agora não há contradição.
Passo 3
Explicação das regras aplicadas até agora:
- Regra
(conjunção): de colocamos e no mesmo ramo. - Regra
(disjunção): de criamos dois ramos, um com e outro com .
No nosso caso, já temos sem ramificação direta as fórmulas
,
,
e
no único ramo.
Passo 4
Agora aplicamos a regra
em
. Isso gera dois ramos:
Ramo 1: verdadeiro.
Ramo 2: verdadeiro.
Ramo 1:
Ramo 2:
Passo 5
No Ramo 1 temos
, aplicamos outra regra
e bifurcamos:
- Subramo 1.1:
. Mas no ramo principal já tínhamos . Assim e fecham esse subramo. - Subramo 1.2:
. Aqui temos apenas e . Não há mais fórmulas para decompor (em e basta que seja verdadeiro) e não aparece contradição. Este subramo permanece aberto.
No Ramo 2 temos
junto com
. As disjunções
e
já estão satisfeitas por
, não há mais expansões nem contradições, então este ramo também fica aberto.
Passo 6
Como existe pelo menos um ramo aberto, a fórmula é satisfatível. Do Subramo 1.2 (ou do Ramo 2) extraímos um modelo:
-
deve ser verdadeiro. -
indica falso. -
não foi fixado em Subramo 1.2, então podemos escolher falso (ou verdadeiro) — no Ramo 2 poderíamos escolher arbitrariamente.
Uma atribuição funciona, por exemplo:
Resposta
A fórmula é satisfatível. Um modelo é