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 avec identité et descriptions en appliquant les règles de base d'inférence exposées dans la théorie de la démonstration :
NIVEAU 1
| [Exercice 25] | [Exercice 26] | ||
-1.∀x(Px→ Qx) |
⊦Qb | 1. ∃x∀x(ιxPx=x ∧ y≠x) | ⊦Qa |
| -2. Pa | |||
| -3. b=a | |||
| 4. Pa → Qa | E∀1 | ||
| 5. Qa | E→2,4 | ||
| 6. ∀x(x=a →Qx) | I=5 | ||
| 7. b=a → Qb | E∀6 (x:b) | ||
| 8. Qb | E→3,7 | ||
NIVEAU 2
| [Exercice 27] | [Exercice 28] | |||
|
⊦(x)yz[(x≠y)∧(y=z) → (x≠z)] | -1. a=ιxPx | ⊦PιxPx | |
| ┌ | -1. (a≠b)∧(b=c) | -2.∀x(Qx→ ¬Px) | ||
| | | 2. (x)y((x≠y)∧(y=z) → (x≠z)] | L. Leibniz | ||
| | | 3. (a≠b)∧(c=b)→ a≠c | E∀2 (x:a; y:c) | ||
| | | 4. b=c | E^1 | ||
| | | 5. (x)y(x=y →y=x) | L. Sym = | ||
| | | 6. b=c → c=b | E∀5(x:b; y:c) | ||
| | | 7. c=b | E→6,4 | ||
| | | 8. a≠b | E^1 | ||
| | | 9. a≠b ∧ c=b | I^8,7 | ||
| | | 10. a ≠c | E→3,9 | ||
| ┗ | 11. (a≠b)∧(b=c)→ a≠c | I→1-10 | ||
| 12. (x)yz[(x≠y)∧(y=z) → (x≠z)] | i∀11(a:x, b:y, c:z) | |||
NIVEAU 3
| [Exercice 29] | [Exercice 30] | |||
1. ¬∃x∃y(x≠y) |
⊦∃xPx→∀xPx | -1.∀x(Sx→ Qx) | ⊦a≠ιxFx | |
| -2.∀x(¬Px→ ¬Qx) | ||||
| -3.SιxPx | ||||
| -4. ¬Pa | ||||
| ┌ | 5. a=ιxFx | |||
| | | 6. ∀x(x=ιxFx → Sx) | I=3 | ||
| | | 7. a=ιxFx → Sa | E∀6 | ||
| | | 8. Sa | E→5,7 | ||
| | | 9. Sa → Qa | E∀1 | ||
| | | 10.Qa | E→8,9 | ||
| | | 11. ¬Pa → ¬Qa | E∀2 | ||
| | | 12. ¬Qa | E→4,11 | ||
| ┗ | 13. Qa ∧ ¬Qa | I^10, 12 | ||
| 14. ¬(a=ιxFx) | I¬5-13 | |||