Lista2 Pred 2016 1gabarito

Prévia do material em texto

CIC 117366 Lo´gica Computacional 1 - Turmas A e D - 2016/1
27 de junho de 2016
Lista: Lo´gica de Predicados (Gabarito)
Derivac¸o˜es em Deduc¸a˜o Natural e Ca´lculo de Gentzen
Estagia´rio de doceˆncia: Thiago Ramos (thiagomendoncaferreiraramos@yahoo.com.br)
Monitora: Luiza Hansen (luizaahansen@gmail.com)
Em adic¸a˜o aos exerc´ıcios que aparecem nas notas de aula, fac¸a os listados a seguir. Nas suas
derivac¸o˜es, sempre indique qual regra dedutiva e´ utilizada em cada um dos passos.
1. Com derivac¸o˜es em Deduc¸a˜o Natural, prove as sequintes equivaleˆncias.
(a) ¬∀xφ a` ∃x¬φ
[¬∃x¬φ]u
[¬φ(a)]v
∃x¬φ ∃i
⊥ ¬e
φ(a)
PPC, v
∀xφ ∀i ¬∀xφ
⊥ ¬e
∃x¬φ PPC, u
∃x¬φ
[¬φ(a)]u
[∀xφ]v
φ(a)
∀e
⊥ (¬e)
⊥ (∃e), u
¬∀xφ (¬i), v
(b) ∀xφ a` ¬∃x¬φ
¬∃x¬φ
[¬φ(a)]u
∃x¬φ ∃i
⊥ ¬e
φ(a)
PPC, u
∀xφ ∀i
1
[∃x¬φ]v
[¬φ(a)]u
∀xφ
φ(a)
∀e
⊥ (¬e)
⊥ (∃e), u
¬∃x¬φ (¬i), v
(c) ∃xφ ` ¬∀x¬φ
∃xφ
[φ(a)]u
[∀x¬φ]v
¬φ(a) ∀e
⊥ (¬e)
⊥ (∃e), u
¬∀x¬φ (¬i), v
2. Apresente derivac¸o˜es em Deduc¸a˜o Natural, para os sequentes a seguir assumindo que
x na˜o ocorre livre em ψ:
(a) (∀xφ) ∧ ψ ` ∀x (φ ∧ ψ)
(∀xφ) ∧ ψ
∀xφ ∧e
φ(a)
∀e (∀xφ) ∧ ψψ ∧e
φ(a) ∧ ψ ∧i
∀x (φ ∧ ψ) ∀i
(b) (∃xφ) ∧ ψ ` ∃x (φ ∧ ψ)
(∃xφ) ∧ ψ
∃xφ ∧e
[φ(a)]u
(∃xφ) ∧ ψ
ψ
∧e
φ(a) ∧ ψ ∧i
∃x (φ ∧ ψ) ∃i
∃x (φ ∧ ψ) ∃e, u
(c) ∀x (ψ → φ) ` ψ → ∀xφ
[ψ]u
∀x (ψ → φ)
ψ → φ(a) ∀e
φ(a)
→e
∀xφ ∀i
ψ → ∀xφ →i, u
2
(d) ∀x (φ→ ψ) ` (∃xφ) → ψ
[∃xφ]u
[φ(a)]v
∀x (φ→ ψ)
φ(a) → ψ ∀e
ψ
→e
ψ
∃e, v
(∃xφ) → ψ →i, u
3. Prove os sequentes a seguir utilizando o Ca´lculo de Gentzen e indique se foi utilizada
a lo´gica intuicionista ou cla´ssica::
(a) φ ∧ ψ ` φ. Intucionista
φ⇒ φ
φ ∧ ψ ⇒ φ (L∧)
(b) ¬(φ ∨ ψ) ` (¬φ ∧ ¬ψ). Cla´ssica
φ⇒ φ
φ⇒ φ ∨ ψ (R∨)
⇒ ¬φ, φ ∨ ψ (R→)
ψ ⇒ ψ
ψ ⇒ φ ∨ ψ (R∨)
⇒ ¬ψ, φ ∨ ψ (R→)
⇒ (¬φ ∧ ¬ψ), φ ∨ ψ (R∧) ⊥ ⇒ (¬φ ∧ ¬ψ)
¬(φ ∨ ψ) ⇒ (¬φ ∧ ¬ψ) (L→)
(c) ¬¬(φ ∧ ψ) ` ¬¬φ ∧ ¬¬ψ. Cla´ssica
φ⇒ φ
φ ∧ ψ,⇒ φ (L∧) φ ∧ ψ,⊥ ⇒
φ ∧ ψ,¬φ⇒ L→
φ ∧ ψ ⇒ ¬¬φ (L→)
ψ ⇒ ψ
φ ∧ ψ,⇒ ψ (L∧) φ ∧ ψ,⊥ ⇒
φ ∧ ψ,¬ψ ⇒ (L→)
φ ∧ ψ ⇒ ¬¬ψH (R→)
φ ∧ ψ ⇒ ¬¬φ ∧ ¬¬ψ (R∧)
⇒ ¬(φ ∧ ψ),¬¬φ ∧ ¬¬ψ (R→) ⊥ ⇒ ¬¬φ ∧ ¬¬ψ
¬¬(φ ∧ ψ) ⇒ ¬¬φ ∧ ¬¬ψ (L→)
(d) ¬(φ ∨ ψ) a` ¬φ ∧ ¬ψ. Cla´ssica
φ⇒ φ
φ⇒ φ ∨ ψ (R∨)
⇒ φ ∨ ψ,¬φ (R→)
ψ ⇒ ψ
ψ ⇒ φ ∨ ψ (R∨)
⇒ φ ∨ ψ,¬ψ (R→)
⇒ φ ∨ ψ,¬φ ∧ ¬ψ (R∧) ⊥ ⇒ ¬φ ∧ ¬ψ
¬(φ ∨ ψ) ⇒ ¬φ ∧ ¬ψ (R→)
3
Intucionista
φ⇒ φ ⊥, φ⇒
¬φ, φ⇒ (L→)
¬φ ∧ ¬ψ, φ⇒ (L∧)
ψ ⇒ ψ ⊥, ψ ⇒
¬ψ, ψ ⇒ (L→)
¬φ ∧ ¬ψ, ψ ⇒ (R∧)
¬φ ∧ ¬ψ, φ ∨ ψ ⇒ (L∨)
¬φ ∧ ¬ψ ⇒ ¬(φ ∨ ψ) (R→)
(e) (φ→ ψ) ∧ (δ → ψ) ` (φ ∧ δ) → ψ. Cla´ssica
φ⇒ ψ, φ ψ, φ⇒ ψ
φ→ ψ, φ⇒ ψ (L→)
φ→ ψ, φ ∧ δ ⇒ ψ (L∧)
(φ→ ψ) ∧ (δ → ψ), φ ∧ δ ⇒ ψ (L∧)
(φ→ ψ) ∧ (δ → ψ) ⇒ (φ ∧ δ) → ψ (R→)
(f) (φ→ ψ) ` (¬ψ → ¬φ). Cla´ssica
φ⇒ ψ, φ ψ, φ⇒ ψ
φ→ ψ, φ⇒ ψ (L→) φ→ ψ,⊥, φ⇒
φ→ ψ,¬ψ, φ⇒ (L→)
φ→ ψ,¬ψ ⇒ ¬φ (R→)
φ→ ψ ⇒ ¬ψ → ¬φ (R→)
(g) ` (φ ∨ ψ) ↔ ¬(¬φ ∧ ¬ψ). Cla´ssica
φ⇒ φ φ,⊥ ⇒
φ,¬φ⇒ (R→)
φ,¬φ ∧ ¬ψ ⇒ (L∧)
ψ ⇒ ψ ψ,⊥ ⇒
ψ,¬ψ ⇒ (R→)
ψ,¬φ ∧ ¬ψ ⇒ (L∧)
φ ∨ ψ,¬φ ∧ ¬ψ ⇒ (L∨)
φ ∨ ψ ⇒ ¬(¬φ ∧ ¬ψ) (R→)
⇒ (φ ∨ ψ) → ¬(¬φ ∧ ¬ψ) (R→)
φ⇒ φ
φ⇒ φ ∨ ψ (R∨)
⇒ ¬φ, φ ∨ ψ (R→)
ψ ⇒ ψ
ψ ⇒ φ ∨ ψ (R∨)
⇒ ¬ψ, φ ∨ ψ (R→)
⇒ ¬φ ∧ ¬ψ, φ ∨ ψ (R∧) ⊥ ⇒ φ ∨ ψ
¬(¬φ ∧ ¬ψ) ⇒ φ ∨ ψ (L→)
⇒ ¬(¬φ ∧ ¬ψ) → (φ ∨ ψ) (R→)
⇒ (φ ∨ ψ) ↔ ¬(¬φ ∧ ¬ψ) (R∧)
(h) ` (¬¬φ→ ¬¬ψ) → ¬¬(φ→ ψ). Intucionista
4
ψ, φ⇒ ψ
ψ ⇒ φ→ ψ (R→) ⊥, ψ ⇒
¬(φ→ ψ), ψ ⇒ (L→)
¬(φ→ ψ) ⇒ ¬ψ (R→) ⊥,¬(φ→ ψ) ⇒
¬¬ψ,¬(φ→ ψ) ⇒ (L→)
φ⇒ φ ⊥, φ⇒
¬φ, φ⇒ (L→)
¬φ, φ⇒ ψ (Rw)
¬φ⇒ φ→ ψ (R→) ⊥,¬φ⇒
¬(φ→ ψ),¬φ⇒ (L→)
¬(φ→ ψ) ⇒ ¬¬φ (R→)
¬¬φ→ ¬¬ψ,¬(φ→ ψ) ⇒ (L→)
¬¬φ→ ¬¬ψ ⇒ ¬¬(φ→ ψ) (R→)
⇒ (¬¬φ→ ¬¬ψ) → ¬¬(φ→ ψ) (R→)
(i) (φ ∧ (ψ ∨ δ)) ` ((φ ∧ ψ) ∨ (φ ∧ δ)). Cla´ssica
φ, ψ ⇒ φ, φ ∧ δ φ, ψ ⇒ ψ, φ ∧ δ
φ, ψ ⇒ φ ∧ ψ, φ ∧ δ (R∧)
φ, δ ⇒ φ ∧ ψ, φ φ, δ ⇒ φ ∧ ψ, δ
φ, δ ⇒ φ ∧ ψ, φ ∧ δ (R∧)
φ, ψ ∨ δ ⇒ φ ∧ ψ, φ ∧ δ (L∨)
φ, φ ∧ (ψ ∨ δ) ⇒ φ ∧ ψ, φ ∧ δ (L∧)
φ ∧ (ψ ∨ δ), φ ∧ (ψ ∨ δ) ⇒ φ ∧ ψ, φ ∧ δ (L∧)
φ ∧ (ψ ∨ δ) ⇒ φ ∧ ψ, φ ∧ δ (LC)
φ ∧ (ψ ∨ δ) ⇒ φ ∧ ψ, (φ ∧ ψ) ∨ (φ ∧ δ) (R∨)
φ ∧ (ψ ∨ δ) ⇒ (φ ∧ ψ) ∨ (φ ∧ δ), (φ ∧ ψ) ∨ (φ ∧ δ) (R∨)
φ ∧ (ψ ∨ δ) ⇒ (φ ∧ ψ) ∨ (φ ∧ δ) (RC)
(j) p ∨ q ` ¬(¬p ∧ ¬q) Intucionista
p,⊥,¬q ⇒ p,¬q ⇒ p
p,¬p,¬q ⇒ (L→)
q,¬p,⊥ ⇒ q,¬p⇒ q
q,¬p,¬q ⇒ (R→)
p ∨ q,¬p,¬q ⇒ (L∨)
p ∨ q,¬p,¬p ∧ ¬q ⇒ (L∧)
p ∨ q,¬p ∧ ¬q,¬p ∧ ¬q ⇒ (L∧)
p ∨ q,¬p ∧ ¬q ⇒ (LC)
p ∨ q ⇒ ¬(¬p ∧ ¬q) (R→)
(k) ¬(¬p ∧ ¬q) ` p ∨ q Cla´ssica
5
p⇒ p, q
⇒ p, q,¬p (R→)
q ⇒ p, q
⇒ p, q,¬q (R→)
⇒ p, q,¬p ∧ ¬q (L∧) ⊥ ⇒ p, q
¬(¬p ∧ ¬q) ⇒ p, q (L→)
¬(¬p ∧ ¬q) ⇒ p, p ∨ q (R∨)
¬(¬p ∧ ¬q) ⇒ p ∨ q, p ∨ q (R∨)
¬(¬p ∧ ¬q) ⇒ p ∨ q (RC)
4. Com derivac¸o˜es no Ca´lculo de Gentzen, prove as seguintes equivaleˆncias entre os quan-
tificadores universal e existencial:
(a) ¬∀xφ a` ∃x¬φ
φ[x/t] ⇒ φ[x/t]
⇒ ¬φ[x/t], φ[x/t] (R→)
⇒ ∃x¬φ, φ[x/t] (R∃)
⇒ ∃x¬φ,∀xφ (R∀) ⊥ ⇒ ∃x¬φ
¬∀xφ ⇒ ∃x¬φ (L→)
φ[x/t] ⇒ φ[x/t] ⊥, φ[x/t] ⇒
¬φ[x/t], φ[x/t] ⇒ (R→)
¬φ[x/t],∀xφ ⇒ L∀
∃x¬φ, ∀xφ ⇒ (L∃)
∃x¬φ ⇒ ¬∀xφ (R→)
(b) ¬∃xφ a` ∀x¬φ
φ[x/t] ⇒ φ[x/t]
⇒ φ[x/t],¬φ[x/t] R→
⇒ ∃xφ,¬φ[x/t] (R∃)
⇒ ∃xφ,∀x¬φ (R∀) ⊥ ⇒ ∀x¬φ
¬∃xφ ⇒ ∀x¬φ (L→)
φ[x/t] ⇒ φ[x/t] ⊥, φ[x/t] ⇒
¬φ[x/t], φ[x/t] ⇒ (L→)
∀x¬φ, φ[x/t] ⇒ (L∀)
∀x¬φ,∃xφ ⇒ (L∃)
∀x¬φ ⇒ ¬∃xφ (R→)
6
(c) ∀xφ a` ¬∃x¬φ
φ[x/t] ⇒ φ[x/t] φ[x/t], ⊥ ⇒
φ[x/t], ¬φ[x/t] ⇒ (L→)
∀xφ, ¬φ[x/t] ⇒ (L∀)
∀xφ,∃x¬φ⇒ (L∃)
∀xφ ⇒ ¬∃x¬φ (R→)
φ[x/t] ⇒ φ[x/t]
⇒ φ[x/t],¬φ[x/t] (R→)
⇒ φ[x/t],∃x¬φ (R∃)
⇒ ∀xφ,∃x¬φ (R∀) ⊥ ⇒ ∀xφ
¬∃x¬φ ⇒ ∀xφ (L→)
(d) ∃xφ ` ¬∀x¬φ
φ[x/t] ⇒ φ[x/t] φ[x/t],⊥ ⇒
φ[x/t],¬φ[x/t] ⇒ (L→)
φ[x/t],∀x¬φ ⇒ (L∀)
∃xφ,∀x¬φ ⇒ (L∃)
∃xφ ⇒ ¬∀x¬φ (R→)
5. Apresente derivac¸o˜es no Ca´lculo de Gentzen para os sequentes a seguir assumindo que
x na˜o ocorre livre em ψ nos itens (a), (b), (c) e (d). Para o item (g), assuma que x
na˜o ocorre livre em φ.
(a) (∀xφ) ∨ ψ ` ∀x (φ ∨ ψ)
φ[x/x0] ⇒ φ[x/x0]
(Ax)
φ[x/x0] ⇒ φ[x/x0] ∨ ψ
(R∨)
∀xφ⇒ φ[x/x0] ∨ ψ
(L∀)
ψ ⇒ ψ (Ax)
ψ ⇒ φ[x/x0] ∨ ψ
(R∨)
(∀xφ) ∨ ψ ⇒ φ[x/x0] ∨ ψ
(L∨)
(∀xφ) ∨ ψ ⇒ ∀x(φ ∨ ψ) (R∀)
(b) (∃xφ) ∨ ψ ` ∃x (φ ∨ ψ) Considere a como sendo uma constante do tipo de x.
φ[x/x0] ⇒ φ[x/x0]
(Ax)
φ[x/x0] ⇒ φ[x/x0] ∨ ψ
(R∨)
φ[x/x0] ⇒ ∃x(φ ∨ ψ)
(R∃)
∃xφ⇒ ∃x(φ ∨ ψ) (L∃)
ψ ⇒ ψ (Ax)
ψ ⇒ φ[x/a] ∨ ψ (R∨)
ψ ⇒ ∃x(φ ∨ ψ) (R∃)
(∃xφ) ∨ ψ ⇒ ∃x(φ ∨ ψ) (L∨)
7
(c) ∃x (φ→ ψ) ` (∀xφ) → ψ
φ[x/x0] ⇒ ψ, φ[x/x0]
(Ax)
ψ, φ[x/x0] ⇒ ψ
(Ax)
φ[x/x0] → ψ, φ[x/x0] ⇒ ψ
(L→)
φ[x/x0] → ψ,∀xφ⇒ ψ
(L∀)
∃x(φ→ ψ),∀xφ⇒ ψ (L∃)
∃x(φ→ ψ) ⇒ (∀xφ) → ψ (R→)
(d) ∃x (ψ → φ) ` ψ → ∃xφ
ψ ⇒ φ[x/x0], ψ
(Ax)
φ[x/x0], ψ ⇒ φ[x/x0]
(Ax)
ψ → φ[x/x0], ψ ⇒ φ[x/x0]
(L→)
ψ → φ[x/x0], ψ ⇒ ∃xφ
(R∃)
ψ → φ[x/x0] ⇒ ψ → (∃xφ)
(R→)
∃x(ψ → φ) ⇒ ψ → (∃xφ) (L∃)
(e) (∀xφ) ∧ (∀xψ) a` ∀x(φ ∧ ψ)
φ[x/x0] ⇒ φ[x/x0]
(Ax)
∀xφ⇒ φ[x/x0]
(L∀)
∀xφ ∧ ∀xψ ⇒ φ[x/x0]
(L∧)
ψ[x/x0] ⇒ ψ[x/x0]
(Ax)
∀xψ ⇒ ψ[x/x0]
(L∀)
∀xφ ∧ ∀xψ ⇒ ψ[x/x0]
(L∧)
∀xφ ∧ ∀xψ ⇒ φ[x/x0] ∧ ψ[x/x0]
(R∧)
∀xφ ∧ ∀xψ ⇒ ∀x(φ ∧ ψ) (R∀)
φ[x/x0] ⇒ φ[x/x0] (Ax)
φ[x/x0] ∧ ψ[x/x0] ⇒ φ[x/x0] (L∧)
∀x(φ ∧ ψ) ⇒ φ[x/x0] (L∀)
∀x(φ ∧ ψ) ⇒ ∀xφ (R∀)
ψ[x/x1] ⇒ ψ[x/x1] (Ax)
φ[x/x1] ∧ ψ[x/x1] ⇒ ψ[x/x1] (L∧)
∀x(φ ∧ ψ) ⇒ ψ[x/x1] (L∀)
∀x(φ ∧ ψ) ⇒ ∀xψ (R∀)
∀x(φ ∧ ψ) ⇒ ∀xφ ∧ ∀xψ (R∧)
8
(f) ∃xφ ∨ ∃xψ a` ∃x (φ ∨ ψ)
φ[x/x0] ⇒ φ[x/x0]
(Ax)
φ[x/x0] ⇒ φ[x/x0] ∨ ψ[x/x0]
(R∨)
φ[x/x0] ⇒ ∃x(φ ∨ ψ)
(R∃)
∃xφ⇒ ∃x(φ ∨ ψ) (L∃)
ψ[x/x0] ⇒ ψ[x/x0]
(Ax)
ψ[x/x0] ⇒ φ[x/x0] ∨ ψ[x/x0]
(R∨)
ψ[x/x0] ⇒ ∃x(φ ∨ ψ)
(R∃)
∃xψ ⇒ ∃x(φ ∨ ψ) (L∃)
∃xφ ∨ ∃xψ ⇒ ∃x(φ ∨ ψ) (L∨)
φ[x/x0] ⇒ φ[x/x0] (Ax)
φ[x/x0] ⇒ ∃xφ (R∃)
φ[x/x0] ⇒ ∃xφ ∨ ∃xψ (R∨)
ψ[x/x0] ⇒ ψ[x/x0] (Ax)
ψ[x/x0] ⇒ ∃xψ (R∃)
ψ[x/x0] ⇒ ∃xφ ∨ ∃xψ (R∨)
φ[x/x0] ∨ ψ[x/x0] ⇒ ∃xφ ∨ ∃xψ (L∨)
∃x (φ ∨ ψ) ⇒ ∃xφ ∨ ∃xψ (L∃)
(g) ∃x (φ→ q(x)) a` φ→ ∃x q(x)
φ⇒ q(x0), φ
(Ax)
q(x0), φ⇒ q(x0)
(Ax)
φ→ q(x0), φ⇒ q(x0)
(L→)
φ→ q(x0), φ⇒ ∃xφ
(R∃)
φ→ q(x0) ⇒ φ→ (∃xφ)
(R→)
∃x(φ→ q(x)) ⇒ φ→ (∃x q(x)) (L∃)
Considere a como sendo uma constante do tipo de x.
φ⇒ q(a), φ (Ax)⇒ φ→ q(a), φ (R→)
⇒ ∃x(φ→ q(x)), φ (R∃)
q(x0), φ⇒ q(x0)
(Ax)
q(x0) ⇒ φ→ q(x0)
(R→)
q(x0) ⇒ ∃x(φ→ q(x))
(R∃)
∃x q(x) ⇒ ∃x(φ→ q(x)) (L∃)
φ→ ∃x q(x) ⇒ ∃x(φ→ q(x)) (L→)
(h) ∃x (¬p(x) ∧ ¬q(x)) ` ∃x (¬(p(x) ∧ q(x)))
9
p(x0) ⇒ p(x0)
(Ax) ⊥, p(x0) ⇒
(L⊥)
p(x0) →⊥, p(x0) ⇒
p(x0) →⊥, p(x0) ⇒⊥
(RW )
p(x0) →⊥, p(x0) ∧ q(x0) ⇒⊥
(L∧)
p(x0) →⊥⇒ (p(x0) ∧ q(x0)) →⊥
(R→)
(p(x0) →⊥) ∧ (q(x0) →⊥) ⇒ (p(x0) ∧ q(x0)) →⊥
(L∧)
(p(x0) →⊥) ∧ (q(x0) →⊥) ⇒ ∃x((p(x) ∧ q(x)) →⊥)
(R∃)
∃x((p(x) →⊥) ∧ (q(x) →⊥)) ⇒ ∃x((p(x) ∧ q(x)) →⊥) (L∃)
(i) ∃x (¬p(x) ∨ q(x)) ` ∃x (¬(p(x) ∧ ¬q(x)))
p(x0) ⇒ p(x0)
(Ax) ⊥, p(x0) ⇒
(L⊥)
p(x0) →⊥, p(x0) ⇒
(L→)
p(x0) →⊥, p(x0) ∧ (q(x0) →⊥) ⇒
(L∧)
q(x0) ⇒ q(x0)
(Ax) ⊥, q(x0) ⇒
(L⊥)
q(x0), q(x0) →⊥⇒
(L→)
q(x0), p(x0) ∧ (q(x0) →⊥) ⇒
(L∧)
(p(x0) →⊥) ∨ q(x0), p(x0) ∧ (q(x0) →⊥) ⇒
(L∨)
(p(x0) →⊥) ∨ q(x0), p(x0) ∧ (q(x0) →⊥) ⇒⊥
(RW )
(p(x0) →⊥) ∨ q(x0) ⇒ (p(x0) ∧ (q(x0) →⊥)) →⊥
(R→)
(p(x0) →⊥) ∨ q(x0) ⇒ ∃x((p(x) ∧ (q(x) →⊥)) →⊥)
(R∃)
∃x((p(x) →⊥) ∨ q(x)) ⇒ ∃x((p(x) ∧ (q(x) →⊥)) →⊥) (L∃)
(j) ∀x (p(x) ∧ q(x)) ` (∀x p(x)) ∧ (∀x q(x))
p(x0) ⇒ p(x0)
(Ax)
p(x0) ∧ q(x0) ⇒ p(x0)
(L∧)
∀x(p(x) ∧ q(x)) ⇒ p(x0)
(L∀)
∀x(p(x) ∧ q(x)) ⇒ ∀x p(x) (R∀)
q(x0) ⇒ q(x0)
(Ax)
p(x0) ∧ q(x0) ⇒ q(x0)
(L∧)
∀x(p(x) ∧ q(x)) ⇒ q(x0)
(L∀)
∀x(p(x) ∧ q(x)) ⇒ ∀x q(x) (R∀)
∀x(p(x) ∧ q(x)) ⇒ (∀x p(x)) ∧ (∀x q(x)) (R∧)
(k) (∀x p(x)) ∨ (∀x q(x)) ` ∀x (p(x) ∨ q(x))
p(x0) ⇒ p(x0)
(Ax)
∀x p(x) ⇒ p(x0)
(L∀)
∀x p(x) ⇒ p(x0) ∨ q(x0)
(R∨)
q(x0) ⇒ q(x0)
(Ax)
∀x q(x) ⇒ q(x0)
(L∀)
∀x q(x) ⇒ p(x0) ∨ q(x0)
(R∨)
(∀x p(x)) ∨ (∀x q(x)) ⇒ p(x0) ∨ q(x0)
(L∨)
(∀x p(x)) ∨ (∀x q(x)) ⇒ ∀x(p(x) ∨ q(x)) (R∀)
10
(l) ∃x (p(x) ∧ q(x)) ` ∃x p(x) ∧ ∃x q(x)
p(x0) ⇒ p(x0)
(Ax)
p(x0) ∧ q(x0) ⇒ p(x0)
(L∧)
p(x0) ∧ q(x0) ⇒ ∃x p(x)
(R∃)
q(x0) ⇒ q(x0)
(Ax)
p(x0) ∧ q(x0) ⇒ q(x0)
(L∧)
p(x0) ∧ q(x0) ⇒ ∃x q(x)
(R∃)
p(x0) ∧ q(x0) ⇒ ∃x p(x) ∧ ∃x q(x)
(R∧)
∃x(p(x) ∧ q(x)) ⇒ ∃x p(x) ∧ ∃x q(x) (L∃)
(m) ∃x p(x) ∨ ∃x q(x) ` ∃x (p(x) ∨ q(x))
p(x0) ⇒ p(x0)
(Ax)
p(x0) ⇒ p(x0) ∨ q(x0)
(R∨)
p(x0) ⇒ ∃x(p(x) ∨ q(x))
(R∃)
∃x p(x) ⇒ ∃x(p(x) ∨ q(x)) (L∃)
q(x0) ⇒ q(x0)
(Ax)
q(x0) ⇒ p(x0) ∨ q(x0)
(R∨)
q(x0) ⇒ ∃x(p(x) ∨ q(x))
(R∃)
∃x q(x) ⇒ ∃x(p(x) ∨ q(x))
∃x p(x) ∨ ∃x q(x) ⇒ ∃x(p(x) ∨ q(x)) (L∨)
(n) ∀x∀y (p(y) → q(x)) ` ∃y p(y) → ∀x q(x)
p(y0) ⇒ q(x0), p(y0)
(Ax)
q(x0), p(y0) ⇒ q(x0)
(Ax)
p(y0) → q(x0), p(y0) ⇒ q(x0)
(L→)
∀y(p(y) → q(x0)), p(y0) ⇒ q(x0)
(L∀)
∀y(p(y) → q(x0)),∃y p(y) ⇒ q(x0)
(L∃)
∀x∀y(p(y) → q(x)),∃y p(y) ⇒ q(x0)
(L∀)
∀x∀y(p(y) → q(x)),∃y p(y) ⇒ ∀x q(x) (R∀)
∀x∀y(p(y) → q(x)) ⇒ ∃y p(y) → ∀x q(x) (R→)
6. Conforme os teoremas de equivaleˆncia entre o Ca´lculo de Deduc¸a˜o Natural (CDN) e o
de Gentzen (CG), relacione as regras de cada um destes ca´lculos com as do outro.
Note que as questo˜es dif´ıceis esta˜o relacionadas com como relacionar as regras estri-
tamente cla´ssicas de DN ((PBC), (¬¬e)) e (LEM)) com elementos do CG, e como
relacionar regras estruturais e (Cut) do CG com elementos do CDN.
A derivac¸a˜o:
11
∇
ψ,Γ ⇒ φ
ψ ∧ δ,Γ ⇒ φ (L∧)
Se relaciona com:
[ψ ∧ δ]u
ψ
∧e
Γ
∇′
φ
Onde
ψ Γ
∇′
φ
e´ uma derivac¸a˜o em deduc¸a˜o natural, que existe por hipo´tese de induc¸a˜o, para a prova
em ca´lculo de Gentzen∇.
A derivac¸a˜o:
∇1
Γ ⇒ δ
∇2
Γ ⇒ ψ
Γ ⇒ δ ∧ ψ (R∧)
Se relaciona com:
Γ
∇′1
δ
Γ
∇′2
ψ
δ ∧ ψ ∧i
Onde
Γ
∇′1
δ
Γ
∇′2
ψ
sa˜o derivac¸o˜es em deduc¸a˜o natural, que existem por hipo´tese de induc¸a˜o, para as provas
em ca´lculo de Gentzen∇1 e∇2, respectivamente.
A derivac¸a˜o:
12
∇1
δ,Γ ⇒ φ
∇2
ψ,Γ ⇒ φ
δ ∨ ψ,Γ ⇒ φ (L∨)
Se relaciona com:
[δ ∨ ψ]q
[δ]u Γ
∇′1
φ
[ψ]v Γ
∇′2
φ
φ
∨e, u, v
Onde
[δ]u Γ
∇′1
φ
[ψ]v Γ
∇′2
φ
sa˜o derivac¸o˜es em deduc¸a˜o natural, que existem por hipo´tese de induc¸a˜o, para as provas
em ca´lculo de Gentzen∇1 e∇2, respectivamente.
A derivac¸a˜o: ∇
Γ ⇒ δ
Γ ⇒ δ ∨ ψ (R∨)
Se relaciona com:
Γ
∇′
δ
δ ∨ ψ ∨i
Onde
Γ
∇′
δ
e´ uma derivac¸a˜o em deduc¸a˜o natural, que existe por hipo´tese de induc¸a˜o, para a prova
em ca´lculo de Gentzen∇.
13
A derivac¸a˜o ∇1
Γ ⇒ δ
∇2
ψ,Γ ⇒ φ
δ → ψ,Γ ⇒ φ (L→)
Se relaciona com:
Γ
∇′1
δ δ → ψ
ψ
→e
Γ
∇′2
φ
Onde
Γ
∇′1
δ
ψ Γ
∇′2
φ
sa˜o derivac¸o˜es em deduc¸a˜o natural, que existem por hipo´tese de induc¸a˜o, para as provas
em ca´lculo de Gentzen∇1 e∇2, respectivamente.
A derivac¸a˜o:
∇
δ,Γ ⇒ ψ
Γ ⇒ δ → ψ (R→)
Se relaciona com:
[δ]u Γ
∇′
ψ
δ → ψ →i, u
Onde
[δ]u Γ
∇′
ψ
e´ uma derivac¸a˜o em deduc¸a˜o natural, que existe por hipo´tese de induc¸a˜o, para a prova
em ca´lculo de Gentzen∇.
14
A derivac¸a˜o: ∇
ψ[x/y] ⇒ φ
∀xψ ⇒ φ (L∀)
Se relaciona com:
∀xψ
ψ[x/y]
∀e Γ
∇′
φ
Onde
ψ[x/y] Γ
∇′
φ
e´ uma derivac¸a˜o em deduc¸a˜o natural, que existe por hipo´tese de induc¸a˜o, para a prova
em ca´lculo de Gentzen∇.
A derivac¸a˜o:
∇
ψ[x/y],Γ ⇒ φ
∃xψ,Γ ⇒ φ (L∃)
Se relaciona com:
[∃xψ]v
[ψ[x/y]]u Γ
∇′
φ
φ
(∃e), u
Onde
[ψ[x/y]]u Γ
∇′
φ
e´ uma derivac¸a˜o em deduc¸a˜o natural, que existe por hipo´tese de induc¸a˜o, para a prova
em ca´lculo de Gentzen∇.
15
A derivac¸a˜o:
∇
Γ ⇒ ψ[x/y]
Γ ⇒ ∃xψ (R∃)
Se relaciona com:
∇′ Γ
ψ[x/y]
∃xψ ∃i
Onde ∇′ Γ
ψ[x/y]
e´ uma derivac¸a˜o em deduc¸a˜o natural, que existe por hipo´tese de induc¸a˜o, para a prova
em ca´lculo de Gentzen∇.
A derivac¸a˜o
∇1
Γ ⇒ ψ
∇2
ψ,Γ ⇒ φ
Γ ⇒ φ (Cut)
Se relaciona com
Γ
∇′1
ψ Γ
∇′2
φ
Onde
Γ
∇′1
ψ
ψ Γ
∇′2
φ
sa˜o derivac¸o˜es em deduc¸a˜o natural, que existem por hipo´tese de induc¸a˜o, para as provas
em ca´lculo de Gentzen∇1 e∇2, respectivamente.
16
Outras derivac¸o˜es de regras como PBC, ¬¬e e LEM sa˜o relacionados com o CG da
seguinte forma:
∇′
Γ,¬φ⇒ ⊥ Γ,⊥ ⇒ φ
Γ ⇒ φ (Cut)
Se relaciona com PBC:
[¬φ]u
∇
⊥
φ
PBC, u
A derivac¸a˜o
∇′
Γ ⇒ ¬¬φ
φ,Γ ⇒ φ
Γ ⇒ φ,¬φ (R→) ⊥,Γ ⇒ φ
¬¬φ,Γ ⇒ φ (L→)
Γ ⇒ φ (Cut)
Se relaciona com
∇
¬¬φ
φ
¬¬e
Ja´ a lei do terceiro exclu´ıdo:
φ⇒ φ
⇒ φ,¬φ (R→)
⇒ φ, φ ∨ ¬φ (R∨)
⇒ φ ∨ ¬φ, φ ∨ ¬φ (R∨)
⇒ φ ∨ ¬φ (RC)
7. Conforme experieˆncia no desenvolvimento do projeto construa uma tabela que rela-
cione as regras do CG com os comandos de prova (split), (flatten), (inst),
(Skolem), (lemma), (case), (copy), (hide) do assistente de demonstrac¸a˜o PVS.
Note que sera´ preciso discriminar a ac¸a˜o destas regras sobre fo´rmulas no antecedente
e no sucedente de cada sequente.
17
Comando de Prova Ca´lculo de Gentzen Efeito
(flatten) (R∨), (L∧), (R→)
Γ, α1, α2, γ1 ⇒ β1, β2, γ2,∆
Γ, α1, α2 ⇒ β1, β2, γ1 → γ2,∆ (R→)
Γ, α1, α2 ⇒ β1, β1 ∨ β2, γ1 → γ2,∆ (R∨)
Γ, α1, α2 ⇒ β1 ∨ β2, β1 ∨ β2, γ1 → γ2,∆ (L∧)
Γ, α1 ∧ α2, α1 ∧ α2 ⇒ β1 ∨ β2, β1 ∨ β2, γ1 → γ2,∆ (L∧)
Γ, α1 ∧ α2, α1 ∧ α2 ⇒ β1 ∨ β2, γ1 → γ2,∆ (RC)
Γ, α1 ∧ α2 ⇒ β1 ∨ β2, γ1 → γ2,∆ (LC)
(split) (L∨), (R∧), (L→)
Γ, φ1 ⇒ ∆ Γ, φ2 ⇒ ∆
Γ, φ1 ∨ φ2 ⇒ ∆ (L∨)
Γ ⇒ ∆, φ1 Γ ⇒ ∆, φ2
Γ ⇒ ∆, φ1 ∧ φ2 (R∧)
Γ, φ2 ⇒ ∆ Γ ⇒ ∆, φ1
Γ ⇒ φ1 → φ2,∆ (L→)
(inst) (R∀), (L∃)
Γ ⇒ ∆, φ[x/t]
Γ ⇒ ∆,∀xφ (R∀)
Γ, φ[x/t] ⇒ ∆
Γ,∃xφ⇒ ∆ (R∃)
(skolem) (L∀), (R∃)
Γ ⇒ ∆, φ[x/t]
Γ ⇒ ∆,∃xφ (R∃)
Γ, φ[x/t] ⇒ ∆
Γ,∀xφ⇒ ∆ (R∀)
(case) (Cut)
Γ ⇒ ∆, φ Γ, φ⇒ ∆
Γ ⇒ ∆ (Cut)
(copy) (RC), (LC)
Γ, φ⇒ ∆
Γ, φ, φ⇒ ∆ (LC)
Γ ⇒ ∆, φ
Γ ⇒ ∆, φ, φ (RC)
(lemma)
Γ, φ⇒ ∆
Γ ⇒ ∆ (lemma) Onde φ ja´ foi provado.
(hide) (RW ), (LW )
Γ ⇒ ∆
Γ, φ⇒ ∆ (LW )
Γ ⇒ ∆
Γ ⇒ ∆, φ (RW )
8. Explique a semaˆntica lo´gica do comando de especificac¸a˜o condicional IF THEN
ELSE ENDIF. Devera´ explicar qual a maneira como fo´rmulas do estilo IF "C"THEN
"T"ELSE "E"ENDIF sa˜o interpretadas tanto no sucedente quanto no antecedente de
sequentes no provador de PVS: qualo comando a aplicar, e qual o seu efeito, a uma
fo´rmula IF "C"THEN "T"ELSE "E"ENDIF no antecedente e no sucedente?
Fo´rmulas no estilo IF "C"THEN "T"ELSE "E"ENDIF possuem a mesma semaˆntica que
(′′C′′ → ′′T′′)∧ (¬′′C′′ → ′′E′′) e sa˜o interpreadas dessa forma tanto no sucedente quanto
no antecedente. Esse tipo de fo´rmula deve ser tratado com (split), tanto no sucedente
quanto no antecedente. Em cada caso o efeito sera˜o os seguintes:
∆ ⇒ (′′C′′ → ′′T′′) ∆ ⇒ (¬′′C′′ → ′′E′′)
∆ ⇒ IF”C”THEN”T”ELSE”E”ENDIF (split)
18
′′C′′ ∧ ′′T′′ ⇒ ∆ ¬′′C′′ ∧ ′′E′′ ⇒ ∆
IF”C”THEN”T”ELSE”E”ENDIF⇒ ∆ (split)
19