lista gentzen

Prévia do material em texto

Universidade de Bras´ılia
Instituto de Cieˆncias Exatas - Departamento de Cieˆncia da Computac¸a˜o
117366 Lo´gica Computacional 1 - 2016/1 Prof. Fla´vio L. C. de Moura
Lista de Exerc´ıcios: Ca´lculo de Sequentes (Gentzen)
1. Prove os sequentes a seguir:
• ((φ→⊥)→⊥)→⊥⇔ φ→⊥
• ((φ→ ψ)→⊥)→⊥⇔ ((φ→⊥) ⊥)→ ((ψ →⊥)→⊥)
• ((φ ∧ ψ)→⊥)→⊥⇔ ((φ→⊥)→⊥) ∧ ((ψ →⊥)→⊥)
• (φ ∨ ψ)→⊥⇔ (φ→⊥) ∧ (ψ →⊥)
• (φ ∧ ψ) ∧ ϕ ⇔ φ ∧ (ψ ∧ ϕ)
• (φ ∨ ψ) ∨ ϕ ⇔ φ ∨ (ψ ∨ ϕ)
• ⇒ φ ∨ (φ→⊥)
• (φ→⊥)→⊥⇒ φ
• φ ⇒ (φ→⊥)→⊥
• φ→ ψ, ψ →⊥⇒ φ→⊥
• (ψ →⊥)→ φ ⇔ (φ→⊥)→ ψ
• ψ → (φ→⊥) ⇔ φ→ (ψ →⊥)
• (p→ r) ∧ (q → r) ⇒ (p ∧ q)→ r
• q → r ⇒ (p→ q)→ (p→ r)
• p→ (q → r), p→ q ⇒ p→ r
• p→ q, r → s ⇒ p ∨ r → q ∨ s
• p ∨ q ⇒ r → (p ∨ q) ∧ r
• (p ∨ (q → p)) ∧ q ⇒ p
• p→ q, r → s ⇒ p ∧ r → q ∧ s
• p→ q ⇒ ((p ∧ q)→ p) ∧ (p→ (p ∧ q))
• ⇒ q → (p→ (p→ (q → p)))
• p→ (q ∧ r) ⇒ (p→ q) ∧ (p→ r)
• (p→ q) ∧ (p→ r) ⇒ p→ (q ∧ r)
• ⇒ (p→ q)→ ((r → s)→ (p ∧ r → q ∧ s))
1
• (p ∧ q) ∧ r, s ∧ t ⇒ q ∧ s
• p ∧ q ⇒ q ∧ p
• p→ (p→ q), p ⇒ q
• q → (p→ r), r →⊥, q ⇒ p→⊥
• ⇒ (p ∧ q)→ p
• p ⇒ q → (p ∧ q)
• p ⇒ (p→ q)→ q
• p→ q ⇒ (q →⊥)→ (p→⊥)
• p ∨ (p ∧ q) ⇒ p
• r, p→ (r → q) ⇒ p→ (q ∧ r)
• p→ (q ∨ r), q → s, r → s ⇒ p→ s
• (p ∧ q) ∨ (p ∧ r) ⇒ p ∧ (q ∨ r)
• φ ∨ ψ ⇔ ((φ→⊥) ∧ (ψ →⊥))→⊥
• Lei de Peirce: ⇒ ((φ→ ψ)→ φ)→ φ
2. 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¬φ
(b) ¬∃xφ a` ∀x¬φ
(c) ∀xφ a` ¬∃x¬φ
(d) ∃xφ ` ¬∀x¬φ
3. 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 (φ ∨ ψ)
(b) (∃xφ) ∨ ψ ` ∃x (φ ∨ ψ)
(c) ∃x (φ→ ψ) ` (∀xφ)→ ψ
(d) ∃x (ψ → φ) ` ψ → ∃xφ
(e) (∀xφ) ∧ (∀xψ) a` ∀x(φ ∧ ψ)
(f) ∃xφ ∨ ∃xψ a` ∃x (φ ∨ ψ)
(g) ∃x (φ→ q(x)) a` φ→ ∃x q(x)
(h) ∃x (¬p(x) ∧ ¬q(x)) ` ∃x (¬(p(x) ∧ q(x)))
(i) ∃x (¬p(x) ∨ q(x)) ` ∃x (¬(p(x) ∧ ¬q(x)))
2
(j) ∀x (p(x) ∧ q(x)) ` (∀x p(x)) ∧ (∀x q(x))
(k) (∀x p(x)) ∨ (∀x q(x)) ` ∀x (p(x) ∨ q(x))
(l) ∃x (p(x) ∧ q(x)) ` ∃x p(x) ∧ ∃x q(x)
(m) ∃x p(x) ∨ ∃x q(x) ` ∃x (p(x) ∨ q(x))
(n) ∀x∀y (p(y)→ q(x)) ` ∃y p(y)→ ∀x q(x)
3