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 | ||