Lógica Computacional 1 - Quinta Lista de Exercícios Resolvida

Vista previa del material en texto

Souluc¸o˜es da Quinta Lista de Exerc´ıcios
Universidade de Bras´ılia - UnB
Instituto de Cieˆncias Exatas
Departamento de Ciencia da Computac¸a˜o - CIC
Andre´ Figueira Lourenc¸o
Mauricio Ayala Rinco´n
1.
(a) ∀xP (x) ` ∀y P (y)
∀xP (x)
P (y0)
∀x e
∀y P (y) ∀y i
(b) ∀x (P (x)→ Q(x)) ` (∀x¬Q(x))→ (∀x¬P (x))
∀x (P (x) → Q(x))
P (x0) → Q(x0) ∀x e
[∀x¬Q(x)]u
¬Q(x0) ∀x e
¬P (x0) MT
∀x¬P (x) ∀x i
(∀x¬Q(x)) → (∀x¬P (x)) → i, u
(c) ∀x (P (x) → ¬Q(x)) ` ¬(∃x (P (x) ∧Q(x)))
[∃x (P (x) ∧Q(x))]u
∀x (P (x) → ¬Q(x))
P (x0) → ¬Q(x0) ∀x e
[P (x0) ∧Q(x0)]v
P (x0)
∧e1
¬Q(x0) → e
[P (x0) ∧Q(x0)]v
Q(x0)
∧e2
⊥ ¬e
⊥ ∃x e, v
¬(∃x (P (x) ∧Q(x))) ¬i, u
2.
(a) ∃x (S → Q(x)) ` S → ∃xQ(x)
∃x (S → Q(x))
[S → Q(x0)]u [S]v
Q(x0)
→ e
∃xQ(x) ∃x i
S → ∃xQ(x) → i, v
S → ∃xQ(x) ∃x e, u
(b) S → ∃xQ(x) ` ∃x (S → Q(x))
S → ∃xQ(x) [S]u
∃xQ(x) → e
[Q(x0)]
v
S → Q(x0) → i, u
∃x (S → Q(x)) ∃x i
∃x (S → Q(x)) ∃x e, v
1
(c) (∃xP (x)) → S ` ∀x (P (x) → S)
(∃xP (x)) → S
[P (x0)]
u
∃xP (x) ∃x i
S
→ e
P (x0) → S → i, u
∀x (P (x) → S) ∀x i
(d) ∀x (¬P (x) ∧Q(x)) ` ∀x (P (x) → Q(x))
∀x (¬P (x) ∧Q(x))
¬P (x0) ∧Q(x0) ∀x e
¬P (x0) ∧e1 [P (x0)]u
⊥ ¬e
Q(x0)
⊥e
P (x0) → Q(x0) → i, u
∀x (P (x) → Q(x)) ∀x i
(e) ∀x (P (x) ∧Q(x)) ` ∀x (P (x) → Q(x))
∀x (P (x) ∧Q(x))
P (x0) ∧Q(x0) ∀x e
Q(x0)
∧e2
[P (x0)]
u
Q(x0) ∧ P (x0) ∧i
Q(x0)
∧e1
P (x0) → Q(x0) → i, u
∀x (P (x) → Q(x)) ∀x i
(f) ∃x (¬P (x) ∧ ¬Q(x)) ` ∃x (¬(P (x) ∧Q(x)))
∃x (¬P (x) ∧ ¬Q(x))
[¬P (x0) ∧ ¬Q(x0)]u
¬P (x0) ∧e1
[P (x0) ∧Q(x0)]v
P (x0)
∧e1
⊥ ¬e
¬(P (x0) ∧Q(x0)) ¬i, v
∃x (¬(P (x) ∧Q(x))) ∃x i
∃x (¬(P (x) ∧Q(x))) ∃x e, u
(g) ∃x (¬P (x) ∨Q(x)) ` ∃x (¬(P (x) ∧ ¬Q(x)))
∃x (¬P (x) ∨Q(x))
[¬P (x0) ∨Q(x0)]a
[P (x0) ∧ ¬Q(x0)]b
P (x0)
∧e1
[¬P (x0)]u
⊥ ¬e
¬(P (x0) ∧ ¬Q(x0) ¬i, b
∃x (¬(P (x) ∧ ¬Q(x))) ∃x i
[P (x0) ∧ ¬Q(x0)]c
¬Q(x0)
∧e2
[Q(x0)]
v
⊥ ¬e
¬(P (x0) ∧ ¬Q(x0) ¬i, c
∃x (¬(P (x) ∧ ¬Q(x))) ∃x i
∃x (¬(P (x) ∧ ¬Q(x))) ∨e, u, v
∃x (¬(P (x) ∧ ¬Q(x))) ∃x e, a
2
(h) ∀x (P (x) ∧Q(x)) ` (∀xP (x)) ∧ (∀xQ(x))
∀x (P (x) ∧Q(x))
P (x0) ∧Q(x0) ∀x e
P (x0)
∧e1
∀xP (x) ∀x i
∀x (P (x) ∧Q(x))
P (x1) ∧Q(x1) ∀x e
Q(x1)
∧e2
∀xQ(x) ∀x i
(∀xP (x)) ∧ (∀xQ(x)) ∧i
(i) (∀xP (x)) ∨ (∀xQ(x)) ` ∀x (P (x) ∨Q(x))
(∀xP (x)) ∨ (∀xQ(x))
[∀xP (x)]u
P (x0)
∀x e
P (x0) ∨Q(x0) ∨i
∀x (P (x) ∨Q(x)) ∀x i
[∀xQ(x)]v
Q(x1)
∀x e
P (x1) ∨Q(x1) ∨i
∀x (P (x) ∨Q(x)) ∀x i
∀x (P (x) ∨Q(x)) ∨e, u, v
(j) ∃x (P (x) ∧Q(x)) ` ∃xP (x) ∧ ∃xQ(x)
∃x (P (x) ∧Q(x))
[P (x0) ∧Q(x0)]u
P (x0)
∧e1
∃xP (x) ∃x i
[P (x0) ∧Q(x0)]u
Q(x0)
∧e2
∃xQ(x) ∃x i
∃xP (x) ∧ ∃xQ(x) ∧i
∃xP (x) ∧ ∃xQ(x) ∃x e, u
(k) ∃xF (x) ∨ ∃xG(x) ` ∃x (F (x) ∨G(x))
∃xF (x) ∨ ∃xG(x)
[∃xF (x)]u
[F (x0)]
a
F (x0) ∨G(x0) ∨i
∃x (F (x) ∨G(x)) ∃x i
∃x (F (x) ∨G(x)) ∃x e, a
[∃xG(x)]v
[G(x0)]
b
F (x0) ∨G(x0) ∨i
∃x (F (x) ∨G(x)) ∃x i
∃x (F (x) ∨G(x)) ∃x e, b
∃x (F (x) ∨G(x)) ∨e, u, v
(l) ∀x ∀y (S(y) → F (x)) ` ∃y S(y) → ∀xF (x)
[∃y S(y)]u
∀x ∀y (S(y) → F (x))
∀y (S(y) → F (x0)) ∀x e
S(y0) → F (x0) ∀y e [S(y0)]a
F (x0)
→ e
∀xF (x) ∀x i
∀xF (x) ∃y e, a
∃y S(y) → ∀xF (x) → i, u
3
(m) ¬∀x¬P (x) ` ∃xP (x)
[P (x0)]
u
∃xP (x) ∃x i [¬∃xP (x)]v
⊥ ¬e
¬P (x0) ¬i, u
∀x¬P (x) ∀x i ¬∀x¬P (x)
⊥ ¬e
∃xP (x) PBC, v
(n) ∀x¬P (x) ` ¬∃xP (x)
[∃xP (x)]a
∀x¬P (x)
¬P (x0) ∀x e [P (x0)]u
⊥ ¬e
⊥ ∃x e, u
¬∃xP (x) ¬i, a
(r) ¬∃xP (x) ` ∀x¬P (x)
[P (x0)]
u
∃xP (x) ∃x i ¬∃xP (x)
⊥ ¬e
¬P (x0) ¬i, u
∀x¬P (x) ∀x i
3.
(a) p ∨ q ` ¬(¬p ∧ ¬q)
p ∨ q
[¬p ∧ ¬q]a
¬p ∧e1 [p]u
⊥ ¬e
¬(¬p ∧ ¬q) ¬i, a
[¬p ∧ ¬q]b
¬q ∧e2 [q]v
⊥ ¬e
¬(¬p ∧ ¬q) ¬i, b
¬(¬p ∧ ¬q) ∨e, u, v
(b) ∃xP (x) ` ¬∀x¬P (x)
∃xP (x)
[P (x0)]
u
[∀x¬P (x)]v
¬P (x0) ∀x e
⊥ ¬e
¬∀x¬P (x) ¬i, v
¬∀x¬P (x) ∃x e, u
(c) ¬(¬p ∧ ¬q) ` p ∨ q (usando ¬¬e)
p ∨ ¬p LEM
[p]u
p ∨ q ∨i [¬(p ∨ q)]x
⊥ ¬e
¬¬(p ∨ q) ¬i, x
p ∨ q ¬¬e
[¬p]v [¬q]a
(¬p ∧ ¬q) ∧i ¬(¬p ∧ ¬q)
⊥ ¬e
q PBC, a
p ∨ q ∨i
p ∨ q ∨e, u, v
4