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

Prévia do material em texto

Souluc¸o˜es da Quarta 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) ¬∀xφ ` ∃x¬φ
[¬φ[x/x0] ]u
∃x¬φ ∃x i [¬∃x¬φ]v
⊥ ¬e
φ[x/x0]
PBC, u
∀xφ ∀x i ¬∀xφ
⊥ ¬e
∃x¬φ PBC, v
∃x¬φ ` ¬∀xφ
∃x¬φ
[¬φ[x/x0] ]u
[∀xφ]v
φ[x/x0]
∀x i
⊥ ¬e
¬∀xφ ¬i, v
¬∀xφ ∃x e, u
(b) ¬∃xφ ` ∀x¬φ
[φ[x/x0] ]
u
∃xφ ∃x i ¬∃xφ
⊥ ¬e
¬φ[x/x0] ¬i, u
∀x¬φ ∀x i
∀x¬φ ` ¬∃xφ
[∃xφ ]u
∀x¬φ
¬φ[x/x0] ∀x e [φ[x/x0] ]v
⊥ ¬e
⊥ ∃x e, v
¬∃xφ ¬i, u
2. Se assumirmos que x na˜o esta´ free em ψ sabemos que ψ[x/x0] ≡ ψ. Por outro lado, x esta´ free
em φ, enta˜o podemos dizer tambe´m que (φ ∧ ψ)[x/x0] ≡ φ[x/x0] ∧ ψ[x/x0] ≡ φ[x/x0] ∧ ψ
(a) (∀xφ) ∧ ψ ` ∀x (φ ∧ ψ)
(∀xφ) ∧ ψ
∀xφ ∧e1
φ[x/x0]
∀x e (∀xφ) ∧ ψ
φ
∧e2
φ[x/x0] ∧ ψ ∧i≡
(φ ∧ ψ)[x/x0]
∀x (φ ∧ ψ) ∀x i
∀x (φ ∧ ψ) ` (∀xφ) ∧ ψ
∀x (φ ∧ ψ)
(φ ∧ ψ)[x/x0] ∀x e≡
φ[x/x0] ∧ ψ
φ[x/x0]
∧e1
∀xφ ∀x i
∀x (φ ∧ ψ)
(φ ∧ ψ)[x/x1] ∀x e≡
φ[x/x1] ∧ ψ
ψ
∧e2
(∀xφ) ∧ ψ ∧i
1
(b) (∀xφ) ∨ ψ ` ∀x (φ ∨ ψ)
(∀xφ) ∨ ψ
[∀xφ]u
φ[x/x0]
∀x e
φ[x/x0] ∨ ψ ∨i
[ψ]v
φ[x/x0] ∨ ψ ∨i
φ[x/x0] ∨ ψ
∨e, u, v
≡
(φ ∨ ψ)[x/x0]
∀x (φ ∨ ψ) ∀x i
∀x (φ ∨ ψ) ` (∀xφ) ∨ ψ
∀x (φ ∨ ψ)
(φ ∨ ψ)[x/x0] ∀x e≡
φ[x/x0] ∨ ψ
[φ[x/x0] ]
u
(∀xφ) ∀x i
(∀xφ) ∨ ψ ∨i
[ψ]v
(∀xφ) ∨ ψ ∨i
(∀xφ) ∨ ψ ∨e, u, v
(c) (∃xφ) ∧ ψ ` ∃x (φ ∧ ψ)
(∃xφ) ∧ ψ
∃xφ ∧e1
[φ[x/x0] ]
u
(∃xφ) ∧ ψ
ψ
∧e2
(φ[x/x0]) ∧ ψ ∧i≡
(φ ∧ ψ)[x/x0]
∃x (φ ∧ ψ) ∃x i
∃x (φ ∧ ψ) ∃x e, u
∃x (φ ∧ ψ) ` (∃xφ) ∧ ψ
∃x (φ ∧ ψ)
[ (φ ∧ ψ)[x/x0] ]u≡
(φ[x/x0]) ∧ ψ
φ[x/x0]
∧e1
∃xφ ∃x i
[ (φ ∧ ψ)[x/x0] ]u≡
(φ[x/x0]) ∧ ψ
ψ
∧e2
(∃xφ) ∧ ψ ∧i
(∃xφ) ∧ ψ ∃x e, u
(d) (∃xφ) ∨ ψ ` ∃x (φ ∨ ψ)
(∃xφ) ∨ ψ
[∃xφ]u
[φ[x/x0] ]
a
φ[x/x0] ∨ ψ ∨i≡
(φ ∨ ψ)[x/x0]
∃x (φ ∨ ψ) ∃x i
∃x (φ ∨ ψ) ∃x e, a
[ψ]v
φ[x/x1] ∨ ψ ∨i≡
(φ ∨ ψ)[x/x1]
∃x (φ ∨ ψ) ∃x i
∃x (φ ∨ ψ) ∨e, u, v
∃x (φ ∨ ψ) ` (∃xφ) ∨ ψ
∃x (φ ∨ ψ)
[ (φ ∨ ψ)[x/x0] ]u≡
φ[x/x0] ∨ ψ
[φ[x/x0] ]
a
(∃xφ) ∃x i
(∃xφ) ∨ ψ ∨i
[ψ]b
(∃xφ) ∨ ψ ∨i
(∃xφ) ∨ ψ ∨e, a, b
(∃xφ) ∨ ψ ∃x e, u
2
(e) ∀x (ψ → φ) ` ψ → ∀xφ
∀x (ψ → φ)
(ψ → φ)[x/x0] ∀x e≡
ψ → φ[x/x0] [ψ]u
φ[x/x0]
→ e
∀xφ ∀x i
ψ → ∀xφ → i, u
ψ → ∀xφ ` ∀x (ψ → φ)
ψ → ∀xφ [ψ]u
∀xφ → e
φ[x/x0]
∀x e
ψ → φ[x/x0] → i, u≡
(ψ → φ)[x/x0]
∀x (ψ → φ) ∀x i
(f) ∃x (φ→ ψ) ` (∀xφ)→ ψ
∃x (φ→ ψ)
[ (φ→ ψ)[x/x0] ]u≡
φ[x/x0]→ ψ
[∀xφ]v
φ[x/x0]
∀x e
ψ
→ e
(∀xφ)→ ψ → i, v
(∀xφ)→ ψ ∃x e
(∀xφ)→ ψ ` ∃x (φ→ ψ)
ψ ∨ ¬ψ LEM [ψ]a
[¬ψ]b (∀xφ)→ ψ
¬∀xφ MT
∆∃x¬φ
[¬φ[x/x0]]v [φ[x/x0]]u
⊥ ¬e
ψ
⊥e
ψ
∃x e, v
ψ
∨e, a, b
φ[x/x0]→ ψ → i, u
≡
(φ→ ψ)[x/x0]
∃x (φ→ ψ) ∃x i
∆ :
[¬φ[x/x0] ]z
∃x¬φ ∃x i [¬∃x¬φ]w
⊥ ¬e
φ[x/x0]
PBC, z
∀xφ ∀x i ¬∀xφ
⊥ ¬e
∃x¬φ PBC,w
3
(g) ∀x (φ→ ψ) ` (∃xφ)→ ψ
[∃xφ]u
∀x (φ→ ψ)
(φ→ ψ)[x/x0] ∀x e≡
φ[x/x0]→ ψ [φ[x/x0] ]v
ψ
→ e
ψ
∃x e, v
(∃xφ)→ ψ → i, u
(∃xφ)→ ψ ` ∀x (φ→ ψ)
[φ[x/x0] ]
u
∃xφ ∃x i (∃xφ)→ ψ
ψ
→ e
φ[x/x0]→ ψ → i, u≡
(φ→ ψ)[x/x0]
∀x (φ→ ψ) ∀x i
(h) ∃x (ψ → φ) ` ψ → ∃xφ
∃x (ψ → φ)
(ψ → φ)[x/x0]≡
ψ → φ[x/x0] [ψ]a
φ[x/x0]
→ e
∃xφ ∃x i
ψ → ∃xφ → i, a
ψ → ∃xφ ∃x e, u
ψ → ∃xφ ` ∃x (ψ → φ)
ψ → ∃xφ [ψ]u
∃xφ → e
[φ[x/x0] ]
a
ψ → φ[x/x0] → i, u≡
(ψ → φ)[x/x0]
∃x (ψ → φ) ∃x i
∃x (ψ → φ) ∃x e, a
3.
(a) (∀xφ) ∧ (∀xψ) ` ∀(φ ∧ ψ)
(∀xφ) ∧ (∀xψ)
∀xφ ∧e1
φ[x/x0]
∀x e
(∀xφ) ∧ (∀xψ)
∀xψ ∧e2
ψ[x/x0]
∀x e
φ[x/x0] ∧ ψ[x/x0] ∧i≡
(φ ∧ ψ)[x/x0]
∀(φ ∧ ψ) ∀x i
∀(φ ∧ ψ) ` (∀xφ) ∧ (∀xψ)
∀(φ ∧ ψ)
(φ ∧ ψ)[x/x0] ∀x e≡
φ[x/x0] ∧ ψ[x/x0]
φ[x/x0]
∧e1
∀xφ ∀x i
∀(φ ∧ ψ)
(φ ∧ ψ)[x/x0] ∀x e≡
φ[x/x0] ∧ ψ[x/x0]
ψ[x/x0]
∧e2
∀xψ ∀x i
(∀xφ) ∧ (∀xψ) ∧i
(b) ∃xφ ∨ ∃xψ ` ∃x (φ ∨ ψ)
∃xφ ∨ ∃xψ
[∃xφ]a
[φ[x/x0] ]
u
φ[x/x0] ∨ ψ[x/x0] ∨i≡
(φ ∨ ψ)[x/x0]
∃x (φ ∨ ψ) ∃x i
∃x (φ ∨ ψ) ∃x e, u
[∃xψ]b
[ψ[x/x1] ]
v
φ[x/x1] ∨ ψ[x/x1] ∨i≡
(φ ∨ ψ)[x/x1]
∃x (φ ∨ ψ) ∃x i
∃x (φ ∨ ψ) ∃x e, v
∃x (φ ∨ ψ) ∨e, a, b
4
∃x (φ ∨ ψ) ` ∃xφ ∨ ∃xψ
∃x (φ ∨ ψ)
[ (φ ∨ ψ)[x/x0] ]x≡
φ[x/x0] ∨ ψ[x/x0]
[φ[x/x0] ]
u
∃xφ ∃x i
∃xφ ∨ ∃xψ ∨i
[ψ[x/x0] ]
v
∃xψ ∃x i
∃xφ ∨ ∃xψ ∨i
∃xφ ∨ ∃xψ ∨e, u, v
∃xφ ∨ ∃xψ ∃x e, x
4.
(a) φ→ (q1 ∧ q2) ` (φ→ q1) ∧ (φ→ q2)
φ→ (q1 ∧ q2) [φ]u
q1 ∧ q2 → e
q1
∧e1
φ→ q1 → i, u
φ→ (q1 ∧ q2) [φ]v
q1 ∧ q2 → e
q2
∧e2
φ→ q2 → i, v
(φ→ q1) ∧ (φ→ q2) ∧i
(b) φ→ ∀xQ(x) ` ∀x (φ→ Q(x)) , considerando que x na˜o esta´ free em φ temos que φ[x/t] ≡ φ
φ→ ∀xQ(x) [φ]u
∀xQ(x) → e
Q(x0)
∀x e
φ→ Q(x0) → i, u≡
(φ→ Q(x))[x/x0]
∀x (φ→ Q(x)) ∀x i
(c) (p1 → q1) ∧ (p2 → q2) ` (p1 ∧ p2)→ (q1 ∧ q2)
(p1 → q1) ∧ (p2 → q2)
p1 → q1 ∧e1
[p1 ∧ p2]u
p1
∧e1
q1
→ e
(p1 → q1) ∧ (p2 → q2)
p2 → q2 ∧e1
[p1 ∧ p2]u
p2
∧e2
q2
→ e
q1 ∧ q2 ∧i
(p1 ∧ p2)→ (q1 ∧ q2) → i, u
5