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 de base d'inférence exposées dans la théorie de la démonstration :
NIVEAU 1
| [Exercice 13] | [Exercice 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 | ||
NIVEAU 2
| [Exercice 15] | [Exercice 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)E | ||
| | | ┗ | 9. Raa∧¬Raa | i^7,8 | ||
| ┗ | 10. ¬Rba | i^4-9 | |||
| 11. Rab --> ¬Rba | i→3-10 | ||||
| 12. ∀x∀y(Rxy→¬Ryx) | i∀11 | ||||
NIVEAU 3
| [Exercice 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) | |
| [Exercice 18] | |
-1.∀x(Px→( ∀y(Qy^Ryz)↔¬Sx)) |
⊦∀x((Px^∀y¬(Qy^Ryx))→ ¬Sx) |