Regras de Dedução Natural

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Instituto Federal do Esp´ırito Santo — Campus Serra
Regras para o Sistema de Deduc¸a˜o Natural – Prof. Jefferson O. Andrade – 7 de Junho de 2011
Lo´gica Proposicional
Regras de Equivaleˆncia
1. Bicondicional (bicond)
α↔ β ≡ (α→ β) ∧ (β → α)
2. Ou-exclusivo (ouex)
(a) α Y β ≡ (α ∨ ¬β) ∧ (¬α ∧ β)
(b) α Y β ≡ (α ∨ β) ∧ ¬(α ∧ β)
3. Dupla negac¸a˜o (dn)
¬¬α ≡ α
4. Comutatividade (com)
(a) α ∧ β ≡ β ∧ α
(b) α ∨ β ≡ β ∨ α
5. Associatividade (ass)
(a) α ∧ (β ∧ γ) ≡ (α ∧ β) ∧ γ
(b) α ∨ (β ∨ γ) ≡ (α ∨ β) ∨ γ
6. Distributividade (dist)
(a) α ∧ (β ∨ γ) ≡ (α ∧ β) ∨ (α ∧ γ)
(b) α ∨ (β ∧ γ) ≡ (α ∨ β) ∧ (α ∨ γ)
7. Condicional (cond)
α→ β ≡ ¬α ∨ β
8. De Morgan (dm)
(a) ¬(α ∧ β) ≡ ¬α ∨ ¬β
(b) ¬(α ∨ β) ≡ ¬α ∧ ¬β
9. Idempoteˆncia (id)
(a) α ∧ α ≡ α
(b) α ∨ α ≡ α
10. Complemento (comp)
(a) α ∧ ¬α ≡ 0
(b) α ∨ ¬α ≡ 1
11. Elemento neutro (en)
(a) α ∧ 1 ≡ α
(b) α ∨ 0 ≡ α
12. Elemento absorvente (ea)
(a) α ∧ 0 ≡ 0
(b) α ∨ 1 ≡ 1
Regras de Infereˆncia Ba´sicas
1. Modus Ponens (mp)
α, α→ β
β
2. Modus Tolens (mt)
¬β, α→ β
¬α
3. Conjunc¸a˜o (conj)
α, β
α ∧ β
4. Simplificac¸a˜o (simp)
α ∧ β
α
ou
α ∧ β
β
5. Adic¸a˜o (ad)
α
α ∨ γ — para qualquer γ.
Regras de Infereˆncia Adicionais
1. Exportac¸a˜o (exp)
α→ (β → γ)
(α ∧ β)→ γ
2. Inconsisteˆncia (inc)
α,¬α
γ
— para qualquer γ.
3. Contraposic¸a˜o (cont)
α→ β
¬β → ¬α
4. Silogismo hipote´tico (sh)
α→ β, β → γ
α→ γ
5. Silogismo disjuntivo (sd)
α ∨ β, ¬α
β
ou
α ∨ β, ¬β
α
6. Dilema construtivo (dc)
α→ β, γ → δ, α ∨ γ
β ∨ δ
7. Dilema destrutivo (dd)
α→ β, γ → δ, ¬β ∨ ¬δ
¬α ∨ ¬γ
Lo´gica de Predicados
Regras de Equivaleˆncia
1. Dualidade dos quantificadores (dq)
(a) ¬∀x : P (x) ≡ ∃x : ¬P (x)
(b) ¬∃x : P (x) ≡ ∀x : ¬P (x)
Regras de Infereˆncia
1. Particularizac¸a˜o universal (pu)
∀x : P (x)
P (t)
2. Particularizac¸a˜o existencial (pe)
∃x : P (x)
P (t)
Restric¸a˜o: o s´ımbolo “t” na˜o pode
ter sido usado antes.
3. Generalizac¸a˜o universal (gu)
P (a)
∀x : P (x)
Restric¸a˜o: “a” na˜o pode ter sido
introduzido na demonstrac¸a˜o por
pe. Na˜o pode haver captura de
varia´veis.
4. Generalizac¸a˜o existencial (ge)
P (a)
∃x : P (x)
Na˜o pode haver captura de
varia´veis.