Resolva pelo método de Tableaux
\exists x P b x, \forall x \forall y(P x y \rightarrow S y x) \vdash \exists x S x b

Passo 1

O enunciado nos dá as premissas \exists x\,P\,b\,x \forall x\forall y\bigl(P\,x\,y\rightarrow S\,y\,x\bigr)
e pede para mostrar \exists x\,S\,x\,b
usando método de Tableaux. Neste método assumimos as premissas e a negação da conclusão, expandimos quantificadores e conectivos e verificamos se todos os ramos se fecham.

Passo 2

Negamos a conclusão:
\neg\exists x\,S\,x\,b
que é equivalente a
\forall x\,\neg S\,x\,b.
Nosso conjunto inicial para o tableaux fica então
\exists x\,P\,b\,x,\quad \forall x\forall y\bigl(P\,x\,y\rightarrow S\,y\,x\bigr),\quad \forall x\,\neg S\,x\,b.

Passo 3

Expandimos \exists x\,P\,b\,x com uma constante nova c, obtendo
P\,b\,c.

Passo 4

Expandimos \forall x\forall y(P\,x\,y\rightarrow S\,y\,x) para x=b e y=c, obtendo
P\,b\,c \;\rightarrow\; S\,c\,b.

Passo 5

Expandimos \forall x\,\neg S\,x\,b para x=c, obtendo
\neg S\,c\,b.

Passo 6

Decompondo o condicional P\,b\,c \rightarrow S\,c\,b, criamos dois ramos:
ramo 1: \neg P\,b\,c
ramo 2: S\,c\,b

Passo 7

Analisando os ramos:
– Ramo 1 contém \neg P\,b\,c e P\,b\,c: contradição, fecha o ramo.
– Ramo 2 contém S\,c\,b e \neg S\,c\,b: contradição, fecha o ramo.
Como todos os ramos se fecham, o tableaux está fechado.

Resposta

O tableaux fecha em todos os ramos, logo
\exists x\,S\,x\,b
é consequência lógica das premissas.

Exercícios relacionados