Lógica Para computação

Lógica para computação
Lógica de Predicados
Dedução Natural (continuação)

Luciana Foss [e-mail] Regras - Quantificador Existencial
Introdução existencial (IE): de uma FBF φ contendo uma letra nominal “a”, podemos inferir uma FBF da forma xφ{x/a}.
 Restrições






φ{x/a} é o resultado da substituição de uma ou mais ocorrências da letra nominal “a” em φ por uma variável “x”.
“x” que não pode ocorrer em φ.

Exemplo


Prove x(F(x)  G(x)) ⊦ x(F(x)  G(a))

Exemplo


Prove x(F(x)  G(x)) ⊦ x(F(x)  G(a))
1.
2.
3.

x(F(x)  G(x))
F(a)  G(a)
x(F(x)  G(a))

P
1 EU
3 IE

Regras - Quantificador Existencial




Eliminação existencial (EE): de uma FBF quantificada existencialmente xφ e uma derivação de ψ a partir de uma hipótese da forma φ{a/x}, podemos descartar a hipótese e inferir ψ.
Restrições






φ{a/x} é o resultado da substituição de todas as ocorrências da variável “x” em φ por letra nominal “a”.
“a” não pode ocorrer em φ
“a” não pode ocorrer em ψ
“a” não pode ocorrer nem em qualquer premissa e nem em uma hipótese vigente

Exemplo


Prove x(F(x)  G(x)), xF(x) ⊦ xG(x)

x(Fx  Gx)
xFx

P

| Fa

P
H

| Fa  Ga
| Ga

1 EU
3,4 MP

| xGx

xGx

5 IE
2,3-6 EE

Exemplo


Prove x(F(x)  G(x)), xF(x) ⊦ xG(x)

2.

x(F(x)  G(x))
xF(x)

3.

| F(a)

P
H (EE)

5.

| F(a)  G(a)
| G(a)

1 EU
3,4 MP

6.

| xG(x)

5 IE

7.

xG(x)

2,3-6 EE

1.

4.

P

Derivações inválidas
xyF(y,x) ⊬ xF(x,x)



xyF(y,x) P
yF(y,a) 1 EU
| F(a,a)
H (EE)
| xF(x,x) 3 IE
xF(x,x) 2,3-4 EE
1.

Derivações inválidas
xyF(y,x) ⊬ xF(x,x)



xyF(y,x) P
2.
yF(y,a)
1 EU
| F(a,a)
H (EE)
| xF(x,x) 3 IE
xF(x,x) 2,3-4 EE
1.

Derivações inválidas
xyF(y,x) ⊬ xF(x,x)



xyF(y,x) P
2.
yF(y,a)
1 EU
3. | F(a,a)
H (EE)
| xF(x,x) 3 IE
xF(x,x) 2,3-4 EE
1.