Adapt the solved exercises to your subject. Register for free
Solve the following exercises using Gentzen's natural deduction method for predicate logic, applying the basic inference rules presented in proof theory:
LEVEL 1
| [Exercise 13] | [Exercise 14] | ||
-1.∀x(Px→ Qx) |
⊦∃xQx | -1.∀xPx∧∀xQx | ⊦∀x(Px∧Qx) |
| -2. Pa | |||
| 3. Pa → Qa | E∀1 (x:a) | ||
| 4. Qa | E→ 2,3 | ||
| 5. ∃xQx | I∃4 | ||
LEVEL 2
| [Exercise 15] | [Exercise 16] | ||||
| -1.∀xPx ∨ ∀xQx | ⊦∀x(Px∧Qx) | -1.∀x∀y∀z((Rxy∧Ryz)→Rxz) | ⊦∀x∀y(Rxy→¬Ryx) | ||
| -2.∀x¬Rxx | |||||
| ┌ | 3. Rab | ||||
| | | ┌ | 4. Rba | |||
| | | | | 5. Rab ∧ Rba | I∧3,2 | ||
| | | | | 6. Rab ∧Rba → Raa | E∀1 (x:a, y: b, z:a) | ||
| | | | | 7. Raa | E→5,6 | ||
| | | | | 8. ¬Raa | E∀2 (x:a) | ||
| | | ┗ | 9. Raa∧¬Raa | I∧7,8 | ||
| ┗ | 10. ¬Rba | I¬4-9 | |||
| 11. Rab → ¬Rba | I→3-10 | ||||
| 12. ∀x∀y(Rxy→¬Ryx) | I∀11 | ||||
LEVEL 3
| [Exercise 17] | ||
| -1.∀x(Px→ Qx) | ⊦∀x(∀y(Px∧Ryx)→∀y(Qx ∧Ryx)) | |
| ┌ | 1. ∀y(Pa∧Rya) | |
| | | 2. Pa ∧ Rba | E∀1 (y:b) |
| | | 3. Pa | E∧2 |
| | | 4. Pa→ Qa | E∀1 (x:a) |
| | | 5. Qa | E→3,4 |
| | | 6. Rba | E∧2 |
| | | 7.Qa ∧ Rba | I∧5,6 |
| ┗ | 8. ∀y(Qa∧Rya) | I∀7 (b:y) |
| 9. ∀y(Pa∧Rya) →∀y(Qa∧Rya | I→1-8 | |
| 10. ∀x(∀y(Px∧Ryx)→∀y(Qx ∧Ryx)) | I∀9 (a:x) | |
| [Exercise 18] | |
-1.∀x(Px→( ∀y(Qy∧Ryz)↔¬Sx)) |
⊦∀x((Px∧∀y¬(Qy∧Ryx))→ ¬Sx) |