Árvores de Refutação

P Q R    x y    a b    ∀ ∃    □ ◇ ¬ ∧ ∨ → ↔    ( ) , ⊢ Formato: premissa1, premissa2, ... ⊢ conclusão. -- Selecione um exemplo -- MP: P→Q, P ⊢ Q MT: P→Q, ¬Q ⊢ ¬P SD: P∨Q, ¬P ⊢ Q SH: P→Q, Q→R ⊢ P→R ¬¬: ¬¬P ⊢ P Contrapos: P→Q ⊢ ¬Q→¬P De Morgan: ¬(P∧Q) ⊢ ¬P∨¬Q De Morgan: ¬(P∨Q) ⊢ ¬P∧¬Q Impl Mat: P→Q ⊢ ¬P∨Q ∀ Inst: ∀x P(x) ⊢ P(a) ∃ Gen: P(a) ⊢ ∃x P(x) Barbara Sil. Exist Subst ∃ Igual Ax T: □P ⊢ P Ax 4: □P ⊢ □□P Ax 5: ◇P ⊢ □◇P Dist □ □→◇ Intro ◇ Colap □ Colap ◇ Permut S5 □∀→∀□ ∀□→□∀ ◇∃→∃◇ ∃◇→◇∃ Básico S5 Leibniz □ a=b, □P(a) ❌ Conversão ❌ Afirm Conseq ❌ Neg Antec 🚀 Construir árvore Limpar 📖 Regras 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