Adatta gli esercizi risolti alla tua materia. Registrati gratis
Risolvere i seguenti esercizi mediante il metodo di deduzione naturale proposto da Gentzen per la logica dei predicati applicando le regole derivate di inferenza esposte nella teoria della dimostrazione:
LIVELLO 1
| [Esercizio 19] | [Esercizio 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 | Iv 7 | ||
| 9.Pa → Sa ∨ Ra | I→3-8 | |||
| 10. ∀x(Px→ Sx ∨ Rx) | I∀ 10 | |||
LIVELLO 2
| [Esercizio 21] | [Esercizio 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) | |||
LIVELLO 3
| [Esercizio 23] | [Esercizio 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 | |||
Successivo>>