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