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 derived inference rules presented in proof theory:
LEVEL 1
| [Exercise 19] | [Exercise 20] | |||
-1.∀x(Px→ Qx) |
⊦∀x(Px→ Sx ∨ Rx) | -1.∀xPx → ∀xQx | ⊦¬∀xPx | |
| -2.∀x(¬Sx→ ¬Qx) | -2. ¬Qa | |||
| ┌ | 3. Pa | |||
| | | 4. Pa→ Qa | E∀1 | ||
| | | 5. Qa | E→3,4 | ||
| | | 6. ¬Sa → ¬Qa | E∀2 | ||
| | | 7. Sa | MT 5,6 | ||
| ┗ | 8. Sa ∨ Ra | I∨ 7 | ||
| 9.Pa → Sa ∨ Ra | I→3-8 | |||
| 10. ∀x(Px→ Sx ∨ Rx) | I∀ 10 | |||
LEVEL 2
| [Exercise 21] | [Exercise 22] | ||
| -1.∀x(Tx → Mx) | ⊦∀x(Tx→ Mx) | -1. ∀xMx | ⊦¬∀x∃y¬(Mx→¬Lxy) |
| -2. ∀x¬(Mx ∧ Rx) | -2. ∀x¬Lxx | ||
| 3. ∀x(Tx →( Px → Rx)) | -3. ¬∃x∃y(Lxy ∧¬Lxx) | ||
| 4,∀x∀y¬(Lxy ∧¬Lxx) | |||
| 5. ¬(Lab ∧¬Laa) | |||
| 6. Lab → Laa | |||
| 7. ¬Laa | |||
| 8. ¬Lab | |||
| 9.Ma →¬Lab | |||
| 10. ∀y(Ma →¬Lay) | |||
| 11.∃x∀y(Mx →¬Lxy) | |||
| 12. ∃x¬∃y¬(Mx →¬Lxy) | |||
| 13. ∀x∃y¬(Mx→¬Lxy) | |||
LEVEL 3
| [Exercise 23] | [Exercise 24] | |||
| -1.∀x∀y∀z(¬(Txy→Txz) →¬Qyz) | ⊦¬∃xRxa | -1.∀x(¬Fa ∨ Qx) |
⊦∀x¬(Qx∧ Rx)→ Fa ∨ ¬Tbb) |
|
| -2.∀x∀y∀z(Rya→Qzx) | -2. ∀x(Qx ∧Txb → Rx) | |||
| -3. ∃x∃y∃z(Txz ∧ Txy) | ||||
| ┌ | 4. Tbc ∧Tba | |||
| | | 5. Rba → Qca | E∀2(y:b, x:a, z:c) | ||
| | | 6. ¬(Tbc → Tba) → ¬Qca | E∀1(x:b, y:c, z:a) | ||
| | | 7. Qca → (Tbc →Tba) | CTPS 6 | ||
| | | 8. Rba →(Tbc →Tba) | Tr → 5, 8 | ||
| | | 9. Rba →¬(Tbc ∧¬Tba) | Def (intersec) →/∧ 8 | ||
| | | 10. ¬Rba | MT 4,9 | ||
| | | 11. ∀x¬Rba | I∀11 | ||
| ┗ | 12. ¬∃xRxa | Def ∀/∃ 11 | ||
| 13. ¬∃xRxa | E∃4-12 | |||
Next>>