Regras das Árvores de Refutação
═══════════════════════════════════════════
LÓGICA PROPOSICIONAL
═══════════════════════════════════════════
REGRAS NÃO RAMIFICANTES:
1. Dupla Negação 2. Conjunção 3. Neg. Disj.
¬¬φ φ∧ψ ¬(φ∨ψ)
| | |
φ φ ¬φ
ψ ¬ψ
4. Negação da Implicação
¬(φ→ψ)
|
φ
¬ψ
REGRAS RAMIFICANTES:
5. Disjunção 6. Implicação 7. Neg. Conj.
φ∨ψ φ→ψ ¬(φ∧ψ)
/\ /\ /\
φ ψ ¬φ ψ ¬φ ¬ψ
8. Bicondicional 9. Neg. Bicondicional
φ↔ψ ¬(φ↔ψ)
/\ /\
φ ¬φ φ ¬φ
ψ ¬ψ ¬ψ ψ
═══════════════════════════════════════════
LÓGICA DE PREDICADOS
═══════════════════════════════════════════
10. Universal (∀) 11. Neg. Exist. (¬∃)
∀x φ(x) ¬∃x φ(x)
| |
φ(t) ∀x ¬φ(x) (passo 1)
(termo t) |
¬φ(t) (passo 2)
12. Existencial (∃) 13. Neg. Univ. (¬∀)
∃x φ(x) ¬∀x φ(x)
| |
φ(c) ∃x ¬φ(x) (passo 1)
(novo c) |
¬φ(c) (passo 2)
NOTA: ∀ multi-instanciação; ∃ uma vez
═══════════════════════════════════════════
LÓGICA MODAL S5
═══════════════════════════════════════════
14. Necessidade (□) 15. Neg. Poss. (¬◇)
w: □φ w: ¬◇φ
| |
w: φ (wRw) w: □¬φ
v: φ (∀v) v: ¬φ (∀v)
16. Possibilidade (◇) 17. Neg. Nec. (¬□)
w: ◇φ w: ¬□φ
| |
v: φ (novo v) w: ◇¬φ
|
v: ¬φ (novo v)
PROPAGAÇÃO S5 (DOMÍNIO CONSTANTE):
• □φ → propaga φ para TODOS os mundos
• □φ → propaga □φ para TODOS (axioma 4)
• ∀x φ(x) → propaga para TODOS os mundos
• ◇φ → cria novo mundo com φ
═══════════════════════════════════════════
FECHAMENTO
═══════════════════════════════════════════
• Ramo fecha (×): φ e ¬φ no MESMO mundo
• TODOS fecham → VÁLIDO
• UM aberto (○) → INVÁLIDO
