Adapte os exercícios resolvidos à sua disciplina. Registe-se gratuitamente
Resolva os seguintes exercícios mediante o método de dedução natural proposto por Gentzen para lógica de proposições aplicando as regras derivadas de inferência expostas na teoria da demonstração:
NÍVEL 1
| [Exercício 7] | [Exercício 8] | ||
-1. ¬p → ¬q |
⊦p | -1. p → q ∧r | ⊦¬p |
| -2. q | -2. ¬q ∨ ¬r | ||
| 3. q → p | Contr 1 | ||
| 4. p | E→1 | ||
NÍVEL 2
| [Exercício 9] | [Exercício 10] | ||
-1. p ∨ q |
⊦¬t | -1. (p ∨ q) → r ∨ ¬(s → t) | ⊦¬p ∧¬q |
| -2. t → ¬p | -2. ¬(s ∨ t) ∧ ¬r | ||
| -3. ¬(q ∨ r) | 3. ¬(svt) | E^2 | |
| 4. ¬r | E^2 | ||
| 5. ¬s ∧ ¬t | DM v/^3 | ||
| 6. ¬s | E^5 | ||
| 7. ¬s ∨ t | Iv 6 | ||
| 8. s→t | Def v/→7 | ||
| 9. ¬r ∧ (s→t) | I^4, 8 | ||
| 10.¬(r ∨ ¬s→t) | Def ^/v 9 | ||
| 11. ¬(p ∨ q) | MT 1, 10 | ||
| 12. ¬p ∧¬q | DM ^/v 11 | ||
NÍVEL 3
| [Exercício 11] | [Exercício 12] | ||
-1. p ∨ q ↔ r ∨ s |
⊦¬p ∨ ¬q | ⊦(p ∧ q → r) ↔(p ∧ ¬r → ¬q) | |
| -2. ¬( m ∧¬n) | |||
| -3. w ∨ n | |||
| -4. ( r→ t) → u ∧ (w → m) | |||
| -5. ¬(n ∨ ¬t) | |||
| 6. ¬n ∧ t | DM ^/v 5 | ||
| 7. ¬n | E^6 | ||
| 8. ¬m ∨ n | DM v/^ 2 | ||
| 9. ¬m | SD 7,8 | ||
| 10. t | E^6 | ||
| 11. r→t | Crpr 10 | ||
| 12. u∧(w → m) | E→4, 11 | ||
13. w → m |
E^12 | ||
| 14. w | SD 3, 7 | ||
| 15. m | E→13, 14 | ||
| 16. m ∧¬m | I^ 9, 15 | ||
| 17. ¬p ∨ ¬q | EXQ 16 | ||