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 basic inference rules presented in proof theory:

LEVEL 1

[Exercise 1] [Exercise 2]

-1. s → t

 ⊦r -1. p ∧ ¬¬q ⊦q
-2. t → r   2. ¬¬q E∧ 1
-3. s   3. q E¬2
       
       

LEVEL 2

[Exercise 3] [Exercise 4]

-1. t ∨ m

 ⊦s ∨ (w∧t) -1. p ∨ (r ∧ m) → s ⊦ p→ ( q→ s)
-2. t → p   -2. q ∧ s → t  
-3. p→ s   -3. s ∧ t → r  
-4. m→ q      
-5. q→ w ∧ t      
┌ 6. t      
| 7. p E→2,6    

┗

 8. s E→ 3,7    
┌ 9. m      
| 10. q E→ 4,9    
| 11. w ∧ t E→ 5,10    
| 12. t E∧11    
| 13. p E→ 2,12    
┗ 14. s E→ 3,13    
15.s E∨ 1,6-8,9-14    
16. s ∨ (w∧t) I∨ 15    

LEVEL 3

[Exercise 5] [Exercise 6]

-1. q ∨ r → ¬(p ∧s)

 ⊦¬(t ∨ m) -1. p → t ∨ r ⊦ ¬p
-2. t ∨ m → k ∧ m   -2. t → s ∧ m  
-3. k → s   -3. m ∨ r → ¬(t ∨ r)  
-4. m→ r   ┌   4.p  
-5. ¬(p ∧ s) → ¬(t ∨ m)   |   5. t ∨ r E→1,4
    | ┌ 6. t  
    | | 7.s∧m E→2,6
    | | 8. m E∧7
    | | 9.m ∨ r I∨ 8
    | ┗ 10. ¬(t ∨ r) E→3,9
    | ┌ 11. r  
    | | 12. m ∨ r I∨11
    | ┗ 13. ¬(t ∨ r) E→3,12
    | 14.¬( t ∨ r) E∨5, 6-10, 11-13
    ┗ 15. (t ∨ r) ∧¬( t ∨ r) I∧3,4
    16. ¬p I¬ 4-15

 

 

 

Next>>