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 con identita e descrizioni applicando le regole base di inferenza esposte nella teoria della dimostrazione:
LIVELLO 1
| [Esercizio 25] | [Esercizio 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 | ||
LIVELLO 2
| [Esercizio 27] | [Esercizio 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. Sim = | ||
| | | 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) | |||
LIVELLO 3
| [Esercizio 29] | [Esercizio 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 | |||