Adaptez les exercices résolus à votre matière. Inscrivez-vous gratuitement
Résolvez les exercices suivants en utilisant la méthode de déduction naturelle proposée par Gentzen pour la logique des prédicats en appliquant les règles dérivées d'inférence exposées dans la théorie de la démonstration :
NIVEAU 1
| [Exercice 19] | [Exercice 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 | |||
NIVEAU 2
| [Exercice 21] | [Exercice 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) | |||
NIVEAU 3
| [Exercice 23] | [Exercice 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 | |||
Suivant>>