Adapt the solved exercises to your subject. Register for free
Solve the following exercises using Gentzen's natural deduction method for predicate logic with identity and descriptions, applying the basic inference rules presented in proof theory:
LEVEL 1
| [Exercise 25] | [Exercise 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 | ||
LEVEL 2
| [Exercise 27] | [Exercise 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)] | Leibniz Law | ||
| | | 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) | Sym = Law | ||
| | | 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) | |||
LEVEL 3
| [Exercise 29] | [Exercise 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 | |||