Adapt the solved exercises to your subject. Register for free
Solve the following exercises using Gentzen's natural deduction method for propositional logic, applying the derived inference rules presented in proof theory:
LEVEL 1
| [Exercise 7] | [Exercise 8] | ||
-1. ¬p → ¬q |
⊦p | -1. p → q ∧r | ⊦¬p |
| -2. q | -2. ¬q ∨ ¬r | ||
| 3. q → p | Contr 1 | ||
| 4. p | E→1 | ||
LEVEL 2
| [Exercise 9] | [Exercise 10] | ||
-1. p ∨ q |
⊦¬t | -1. (p ∨ q) → r ∨ ¬(s → t) | ⊦¬p ∧¬q |
| -2. t → ¬p | -2. ¬(s ∨ t) ∧ ¬r | ||
| -3. ¬(q ∨ r) | 3. ¬(s∨t) | E∧2 | |
| 4. ¬r | E∧2 | ||
| 5. ¬s ∧ ¬t | DM ∨/∧3 | ||
| 6. ¬s | E∧5 | ||
| 7. ¬s ∨ t | I∨ 6 | ||
| 8. s→t | Def ∨/→7 | ||
| 9. ¬r ∧ (s→t) | I∧4, 8 | ||
| 10.¬(r ∨ ¬s→t) | Def ∧/∨ 9 | ||
| 11. ¬(p ∨ q) | MT 1, 10 | ||
| 12. ¬p ∧¬q | DM ∧/∨ 11 | ||
LEVEL 3
| [Exercise 11] | [Exercise 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 ∧/∨ 5 | ||
| 7. ¬n | E∧6 | ||
| 8. ¬m ∨ n | DM ∨/∧ 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 | ||