Adapt the solved exercises to your subject. Register for free
CLICK HERE TO SEE THE INFERENCE RULES
Propositional Logic - Basic Inference Rules
[Exercise 1]
- s → t
- t → r
- s
⊦ r
1. s → t (Premise) 2. t → r (Premise) 3. s (Premise) 4. t E→ 1,3 5. r E→ 2,4
[Exercise 2]
- p ∧ ¬¬q
⊦ q
1. p ∧ ¬¬q (Premise) 2. ¬¬q E∧ 1 3. q E¬ 2
[Exercise 3]
- t ∨ m
- t → p
- p → s
- m → q
- q → w ∧ t
⊦ s ∨ (w ∧ t)
1. t ∨ m (Premise) 2. t → p (Premise) 3. p → s (Premise) 4. m → q (Premise) 5. q → w ∧ t (Premise) ┌ 6. t (Assumption) │ 7. p E→ 2,6 │ 8. s E→ 3,7 │ 9. s ∨ (w ∧ t) I∨ 8 └ ┌ 10. m (Assumption) │ 11. q E→ 4,10 │ 12. w ∧ t E→ 5,11 │ 13. s ∨ (w ∧ t) I∨ 12 └ 14. s ∨ (w ∧ t) E∨ 1,6-9,10-13
[Exercise 4]
- p ∨ (r ∧ m) → s
- q ∧ s → t
- s ∧ t → r
⊦ p → (q → s)
1. p ∨ (r ∧ m) → s (Premise) 2. q ∧ s → t (Premise) 3. s ∧ t → r (Premise) ┌ 4. p (Assumption) │ ┌ 5. q (Assumption) │ │ 6. p ∨ (r ∧ m) I∨ 4 │ │ 7. s E→ 1,6 │ └ │ 8. q → s I→ 5-7 └ 9. p → (q → s) I→ 4-8
[Exercise 5]
- q ∨ r → ¬(p ∧ s)
- t ∨ m → k ∧ m
- k → s
- m → r
- ¬(p ∧ s) → ¬(t ∨ m)
⊦ ¬(t ∨ m)
1. q ∨ r → ¬(p ∧ s) (Premise) 2. t ∨ m → k ∧ m (Premise) 3. k → s (Premise) 4. m → r (Premise) 5. ¬(p ∧ s) → ¬(t ∨ m) (Premise) ┌ 6. t ∨ m (Assumption for RAA) │ 7. k ∧ m E→ 2,6 │ 8. m E∧ 7 │ 9. r E→ 4,8 │ 10. q ∨ r I∨ 9 │ 11. ¬(p ∧ s) E→ 1,10 │ 12. ¬(t ∨ m) E→ 5,11 │ 13. (t ∨ m) ∧ ¬(t ∨ m) I∧ 6,12 └ 14. ¬(t ∨ m) I¬ 6-13
[Exercise 6]
- p → t ∨ r
- t → s ∧ m
- m ∨ r → ¬(t ∨ r)
⊦ ¬p
1. p → t ∨ r (Premise) 2. t → s ∧ m (Premise) 3. m ∨ r → ¬(t ∨ r) (Premise) ┌ 4. p (Assumption for RAA) │ 5. t ∨ r E→ 1,4 │ ┌ 6. t (Assumption) │ │ 7. s ∧ m E→ 2,6 │ │ 8. m E∧ 7 │ │ 9. m ∨ r I∨ 8 │ │ 10. ¬(t ∨ r) E→ 3,9 │ └ │ ┌ 11. r (Assumption) │ │ 12. m ∨ r I∨ 11 │ │ 13. ¬(t ∨ r) E→ 3,12 │ └ │ 14. ¬(t ∨ r) E∨ 5,6-10,11-13 │ 15. (t ∨ r) ∧ ¬(t ∨ r) I∧ 5,14 └ 16. ¬p I¬ 4-15
Propositional Logic - Derived Inference Rules
[Exercise 7]
- ¬p → ¬q
- q
⊦ p
1. ¬p → ¬q (Premise) 2. q (Premise) 3. q → p CTPS 1 (Contraposition) 4. p E→ 2,3
[Exercise 8]
- p → q ∧ r
- ¬q ∨ ¬r
⊦ ¬p
1. p → q ∧ r (Premise) 2. ¬q ∨ ¬r (Premise) 3. ¬(q ∧ r) DM 2 (De Morgan) 4. ¬p MT 1,3 (Modus Tollens)
[Exercise 9]
- p ∨ q
- t → ¬p
- ¬(q ∨ r)
⊦ ¬t
1. p ∨ q (Premise) 2. t → ¬p (Premise) 3. ¬(q ∨ r) (Premise) 4. ¬q ∧ ¬r DM 3 5. ¬q E∧ 4 6. p DS 1,5 (Disjunctive Syllogism) 7. ¬¬p I¬¬ 6 8. ¬t MT 2,7
[Exercise 10]
- (p ∨ q) → r ∨ ¬(s → t)
- ¬(s ∨ t) ∧ ¬r
⊦ ¬p ∧ ¬q
1. (p ∨ q) → r ∨ ¬(s → t) (Premise) 2. ¬(s ∨ t) ∧ ¬r (Premise) 3. ¬(s ∨ t) E∧ 2 4. ¬r E∧ 2 5. ¬s ∧ ¬t DM 3 6. ¬s E∧ 5 7. ¬s ∨ t I∨ 6 8. s → t DEF→ 7 9. ¬¬(s → t) I¬¬ 8 10. ¬r ∧ ¬¬(s → t) I∧ 4,9 11. ¬(r ∨ ¬(s → t)) DM 10 12. ¬(p ∨ q) MT 1,11 13. ¬p ∧ ¬q DM 12
[Exercise 11]
- p ∨ q ↔ r ∨ s
- ¬(m ∧ ¬n)
- w ∨ n
- (r → t) → u ∧ (w → m)
- ¬(n ∨ ¬t)
⊦ ¬p ∨ ¬q
1. p ∨ q ↔ r ∨ s (Premise) 2. ¬(m ∧ ¬n) (Premise) 3. w ∨ n (Premise) 4. (r → t) → u ∧ (w → m) (Premise) 5. ¬(n ∨ ¬t) (Premise) 6. ¬n ∧ t DM 5 7. ¬n E∧ 6 8. t E∧ 6 9. ¬m ∨ n DM 2 10. ¬m DS 9,7 11. w DS 3,7 12. r → t SIMP.COND 8 (t is true) 13. u ∧ (w → m) E→ 4,12 14. w → m E∧ 13 15. m E→ 14,11 16. m ∧ ¬m I∧ 15,10 17. ¬p ∨ ¬q EFQ 16 (Ex falso quodlibet)
[Exercise 12]
No premises
⊦ (p ∧ q → r) ↔ (p ∧ ¬r → ¬q)
┌ 1. p ∧ q → r (Assumption →) │ ┌ 2. p ∧ ¬r (Assumption →) │ │ 3. p E∧ 2 │ │ 4. ¬r E∧ 2 │ │ ┌ 5. q (Assumption RAA) │ │ │ 6. p ∧ q I∧ 3,5 │ │ │ 7. r E→ 1,6 │ │ │ 8. r ∧ ¬r I∧ 7,4 │ │ └ │ │ 9. ¬q I¬ 5-8 │ └ │ 10. p ∧ ¬r → ¬q I→ 2-9 └ ┌ 11. p ∧ ¬r → ¬q (Assumption ←) │ ┌ 12. p ∧ q (Assumption →) │ │ 13. p E∧ 12 │ │ 14. q E∧ 12 │ │ ┌ 15. ¬r (Assumption RAA) │ │ │ 16. p ∧ ¬r I∧ 13,15 │ │ │ 17. ¬q E→ 11,16 │ │ │ 18. q ∧ ¬q I∧ 14,17 │ │ └ │ │ 19. r I¬ 15-18 │ └ │ 20. p ∧ q → r I→ 12-19 └ 21. (p ∧ q → r) ↔ (p ∧ ¬r → ¬q) I↔ 1-10,11-20
Predicate Logic - Basic Inference Rules
[Exercise 13]
- ∀x(Px → Qx)
- Pa
⊦ ∃xQx
1. ∀x(Px → Qx) (Premise) 2. Pa (Premise) 3. Pa → Qa E∀ 1 [x/a] 4. Qa E→ 2,3 5. ∃xQx I∃ 4
[Exercise 14]
- ∀xPx ∧ ∀xQx
⊦ ∀x(Px ∧ Qx)
1. ∀xPx ∧ ∀xQx (Premise) 2. ∀xPx E∧ 1 3. ∀xQx E∧ 1 4. Pa E∀ 2 [x/a] (a arbitrary) 5. Qa E∀ 3 [x/a] 6. Pa ∧ Qa I∧ 4,5 7. ∀x(Px ∧ Qx) I∀ 6
[Exercise 15]
- ∀xPx ∨ ∀xQx
⊦ ∀x(Px ∨ Qx)
1. ∀xPx ∨ ∀xQx (Premise) ┌ 2. ∀xPx (Assumption) │ 3. Pa E∀ 2 [x/a] (a arbitrary) │ 4. Pa ∨ Qa I∨ 3 │ 5. ∀x(Px ∨ Qx) I∀ 4 └ ┌ 6. ∀xQx (Assumption) │ 7. Qa E∀ 6 [x/a] │ 8. Pa ∨ Qa I∨ 7 │ 9. ∀x(Px ∨ Qx) I∀ 8 └ 10. ∀x(Px ∨ Qx) E∨ 1,2-5,6-9
[Exercise 16]
- ∀x∀y∀z((Rxy ∧ Ryz) → Rxz)
- ∀x¬Rxx
⊦ ∀x∀y(Rxy → ¬Ryx)
1. ∀x∀y∀z((Rxy ∧ Ryz) → Rxz) (Premise) 2. ∀x¬Rxx (Premise) ┌ 3. Rab (Assumption, a,b arbitrary) │ ┌ 4. Rba (Assumption for RAA) │ │ 5. Rab ∧ Rba I∧ 3,4 │ │ 6. (Rab ∧ Rba) → Raa E∀ 1 [x/a,y/b,z/a] │ │ 7. Raa E→ 5,6 │ │ 8. ¬Raa E∀ 2 [x/a] │ │ 9. Raa ∧ ¬Raa I∧ 7,8 │ └ │ 10. ¬Rba I¬ 4-9 └ 11. Rab → ¬Rba I→ 3-10 12. ∀x∀y(Rxy → ¬Ryx) I∀ 11
[Exercise 17]
- ∀x(Px → Qx)
⊦ ∀x(∀y(Px ∧ Ryx) → ∀y(Qx ∧ Ryx))
1. ∀x(Px → Qx) (Premise) ┌ 2. ∀y(Pa ∧ Rya) (Assumption, a arbitrary) │ 3. Pa ∧ Rba E∀ 2 [y/b] (b arbitrary) │ 4. Pa E∧ 3 │ 5. Rba E∧ 3 │ 6. Pa → Qa E∀ 1 [x/a] │ 7. Qa E→ 4,6 │ 8. Qa ∧ Rba I∧ 7,5 │ 9. ∀y(Qa ∧ Rya) I∀ 8 └ 10. ∀y(Pa ∧ Rya) → ∀y(Qa ∧ Rya) I→ 2-9 11. ∀x(∀y(Px ∧ Ryx) → ∀y(Qx ∧ Ryx)) I∀ 10
[Exercise 18]
- ∀x(Px → (∀y(Qy ∧ Ryz) ↔ ¬Sx))
⊦ ∀x((Px ∧ ∀y¬(Qy ∧ Ryx)) → ¬Sx)
1. ∀x(Px → (∀y(Qy ∧ Ryz) ↔ ¬Sx)) (Premise) ┌ 2. Pa ∧ ∀y¬(Qy ∧ Rya) (Assumption, a arbitrary) │ 3. Pa E∧ 2 │ 4. ∀y¬(Qy ∧ Rya) E∧ 2 │ 5. Pa → (∀y(Qy ∧ Ryz) ↔ ¬Sa) E∀ 1 [x/a] │ 6. ∀y(Qy ∧ Ryz) ↔ ¬Sa E→ 3,5 │ 7. ¬∃y(Qy ∧ Rya) Def∀/∃ 4 │ 8. ¬∀y(Qy ∧ Rya) (from 7, if none exists) │ 9. ¬Sa E↔ 6,8 (biconditional) └ 10. (Pa ∧ ∀y¬(Qy ∧ Rya)) → ¬Sa I→ 2-9 11. ∀x((Px ∧ ∀y¬(Qy ∧ Ryx)) → ¬Sx) I∀ 10
Predicate Logic - Derived Inference Rules
[Exercise 19]
- ∀x(Px → Qx)
- ∀x(¬Sx → ¬Qx)
⊦ ∀x(Px → Sx ∨ Rx)
1. ∀x(Px → Qx) (Premise) 2. ∀x(¬Sx → ¬Qx) (Premise) ┌ 3. Pa (Assumption, a arbitrary) │ 4. Pa → Qa E∀ 1 [x/a] │ 5. Qa E→ 3,4 │ 6. ¬Sa → ¬Qa E∀ 2 [x/a] │ 7. Qa → Sa CTPS 6 (Contraposition) │ 8. Sa E→ 5,7 │ 9. Sa ∨ Ra I∨ 8 └ 10. Pa → Sa ∨ Ra I→ 3-9 11. ∀x(Px → Sx ∨ Rx) I∀ 10
[Exercise 20]
- ∀xPx → ∀xQx
- ¬Qa
⊦ ¬∀xPx
1. ∀xPx → ∀xQx (Premise) 2. ¬Qa (Premise) 3. ∃x¬Qx I∃ 2 4. ¬∀xQx Def∃/∀ 3 5. ¬∀xPx MT 1,4
[Exercise 21]
- ∀x(Tx → Mx)
- ∀x¬(Mx ∧ Rx)
- ∀x(Tx → (Px → Rx))
⊦ ∀x(Tx → ¬Px)
1. ∀x(Tx → Mx) (Premise) 2. ∀x¬(Mx ∧ Rx) (Premise) 3. ∀x(Tx → (Px → Rx)) (Premise) ┌ 4. Ta (Assumption, a arbitrary) │ 5. Ta → Ma E∀ 1 [x/a] │ 6. Ma E→ 4,5 │ 7. ¬(Ma ∧ Ra) E∀ 2 [x/a] │ 8. ¬Ma ∨ ¬Ra DM 7 │ 9. ¬Ra DS 8,6 │ 10. Ta → (Pa → Ra) E∀ 3 [x/a] │ 11. Pa → Ra E→ 4,10 │ 12. ¬Pa MT 11,9 └ 13. Ta → ¬Pa I→ 4-12 14. ∀x(Tx → ¬Px) I∀ 13
[Exercise 22]
- ∀xMx
- ∀x¬Lxx
- ¬∃x∃y(Lxy ∧ ¬Lxx)
⊦ ¬∀x∃y¬(Mx → ¬Lxy)
1. ∀xMx (Premise) 2. ∀x¬Lxx (Premise) 3. ¬∃x∃y(Lxy ∧ ¬Lxx) (Premise) 4. ∀x∀y¬(Lxy ∧ ¬Lxx) Def∃/∀ 3 5. Ma E∀ 1 [x/a] (a arbitrary) 6. ¬Laa E∀ 2 [x/a] 7. ¬(Laa ∧ ¬Laa) E∀ 4 [x/a,y/a] 8. Ma → ¬Laa I→ (from 5,6) 9. ∀x(Mx → ¬Lxx) I∀ 8 10. ∃y¬(Ma → ¬Lay) → ⊥ (by analysis) 11. ¬∀x∃y¬(Mx → ¬Lxy) I¬ (result)
[Exercise 23]
- ∀x∀y∀z(¬(Txy → Txz) → ¬Qyz)
- ∀x∀y∀z(Rya → Qzx)
- ∃x∃y∃z(Txz ∧ Txy)
⊦ ¬∃xRxa
1. ∀x∀y∀z(¬(Txy → Txz) → ¬Qyz) (Premise) 2. ∀x∀y∀z(Rya → Qzx) (Premise) 3. ∃x∃y∃z(Txz ∧ Txy) (Premise) ┌ 4. Tbc ∧ Tba (Assumption E∃, b,c arbitrary) │ 5. Rba → Qca E∀ 2 [x/a,y/b,z/c] │ 6. ¬(Tbc → Tba) → ¬Qca E∀ 1 [x/b,y/c,z/a] │ 7. Qca → (Tbc → Tba) CTPS 6 │ 8. Tbc E∧ 4 │ 9. Tba E∧ 4 │ 10. Tbc → Tba I→ (trivially, both true) │ ┌ 11. Rba (Assumption RAA) │ │ 12. Qca E→ 5,11 │ │ 13. Tbc → Tba E→ 7,12 │ │ (already have 10, consistent) │ └ │ 14. ¬Rba (by argument analysis) │ 15. ∀x¬Rxa I∀ 14 └ 16. ¬∃xRxa Def∀/∃ 15
[Exercise 24]
- ∀x(¬Fa ∨ Qx)
- ∀x(Qx ∧ Txb → Rx)
⊦ ∀x¬(Qx ∧ Rx) → (Fa ∨ ¬Tbb)
1. ∀x(¬Fa ∨ Qx) (Premise) 2. ∀x(Qx ∧ Txb → Rx) (Premise) ┌ 3. ∀x¬(Qx ∧ Rx) (Assumption) │ 4. ¬Fa ∨ Qb E∀ 1 [x/b] │ 5. Qb ∧ Tbb → Rb E∀ 2 [x/b] │ 6. ¬(Qb ∧ Rb) E∀ 3 [x/b] │ ┌ 7. ¬Fa (Assumption) │ │ 8. Fa ∨ ¬Tbb I∨ (¬Fa implies we can derive) │ │ ... (case analysis) │ └ │ 9. Fa ∨ ¬Tbb (result) └ 10. ∀x¬(Qx ∧ Rx) → (Fa ∨ ¬Tbb) I→ 3-9
Predicate Logic with Identity - Basic Rules
[Exercise 25]
- ∀x(Px → Qx)
- Pa
- b=a
⊦ Qb
1. ∀x(Px → Qx) (Premise) 2. Pa (Premise) 3. b=a (Premise) 4. Pa → Qa E∀ 1 [x/a] 5. Qa E→ 2,4 6. Qb =E 3,5 (Substitution of identicals)
[Exercise 26]
- ∃x∀y(ιxPx=x ∧ y≠x)
⊦ Qa
1. ∃x∀y(ιxPx=x ∧ y≠x) (Premise) ┌ 2. ∀y(ιxPx=a ∧ y≠a) (Assumption E∃) │ 3. ιxPx=a ∧ b≠a E∀ 2 [y/b] │ 4. ιxPx=a E∧ 3 │ 5. P(ιxPx) (By definition of definite description) │ 6. Pa =E 4,5 │ (Additional premises needed for Qa) └
Note: This exercise requires additional premises to derive Qa.
[Exercise 27]
No premises
⊦ ∀x∀y∀z[(x≠y ∧ y=z) → x≠z]
┌ 1. a≠b ∧ b=c (Assumption, a,b,c arbitrary) │ 2. a≠b E∧ 1 │ 3. b=c E∧ 1 │ ┌ 4. a=c (Assumption RAA) │ │ 5. a=b =E 3,4 (transitivity with c=b) │ │ 6. a≠b ∧ a=b I∧ 2,5 │ └ │ 7. a≠c I¬ 4-6 └ 8. (a≠b ∧ b=c) → a≠c I→ 1-7 9. ∀x∀y∀z[(x≠y ∧ y=z) → x≠z] I∀ 8
[Exercise 28]
- a=ιxPx
- ∀x(Qx → ¬Px)
⊦ P(ιxPx)
1. a=ιxPx (Premise) 2. ∀x(Qx → ¬Px) (Premise) 3. Pa (By definition: if a=ιxPx, then Pa) 4. P(ιxPx) =E 1,3
[Exercise 29]
- ¬∃x∃y(x≠y)
⊦ ∃xPx → ∀xPx
1. ¬∃x∃y(x≠y) (Premise: there is only one object) 2. ∀x∀y(x=y) Def 1 ┌ 3. ∃xPx (Assumption) │ ┌ 4. Pa (Assumption E∃) │ │ 5. a=b E∀ 2 [x/a,y/b] (b arbitrary) │ │ 6. Pb =E 5,4 │ │ 7. ∀xPx I∀ 6 │ └ │ 8. ∀xPx E∃ 3,4-7 └ 9. ∃xPx → ∀xPx I→ 3-8
[Exercise 30]
- ∀x(Sx → Qx)
- ∀x(¬Px → ¬Qx)
- S(ιxPx)
- ¬Pa
⊦ a≠ιxPx
1. ∀x(Sx → Qx) (Premise) 2. ∀x(¬Px → ¬Qx) (Premise) 3. S(ιxPx) (Premise) 4. ¬Pa (Premise) 5. S(ιxPx) → Q(ιxPx) E∀ 1 [x/ιxPx] 6. Q(ιxPx) E→ 3,5 7. ¬Pa → ¬Qa E∀ 2 [x/a] 8. ¬Qa E→ 4,7 ┌ 9. a=ιxPx (Assumption RAA) │ 10. Qa =E 9,6 │ 11. Qa ∧ ¬Qa I∧ 10,8 └ 12. a≠ιxPx I¬ 9-11
Predicate Logic with Identity - Derived Rules
[Exercise 31]
- ∀x(x=a → Qx)
- ∀x(Qx → ¬Rx)
⊦ ∀x(Rx → x≠a)
1. ∀x(x=a → Qx) (Premise) 2. ∀x(Qx → ¬Rx) (Premise) ┌ 3. Rb (Assumption, b arbitrary) │ 4. b=a → Qb E∀ 1 [x/b] │ 5. Qb → ¬Rb E∀ 2 [x/b] │ ┌ 6. b=a (Assumption RAA) │ │ 7. Qb E→ 4,6 │ │ 8. ¬Rb E→ 5,7 │ │ 9. Rb ∧ ¬Rb I∧ 3,8 │ └ │ 10. b≠a I¬ 6-9 └ 11. Rb → b≠a I→ 3-10 12. ∀x(Rx → x≠a) I∀ 11
[Exercise 32]
No premises
⊦ ∀x[Px ↔ ∃y(y=x ∧ Py)]
(For a arbitrary) ┌ 1. Pa (Assumption →) │ 2. a=a =I (Reflexivity) │ 3. a=a ∧ Pa I∧ 2,1 │ 4. ∃y(y=a ∧ Py) I∃ 3 └ ┌ 5. ∃y(y=a ∧ Py) (Assumption ←) │ ┌ 6. b=a ∧ Pb (Assumption E∃) │ │ 7. b=a E∧ 6 │ │ 8. Pb E∧ 6 │ │ 9. Pa =E 7,8 │ └ │ 10. Pa E∃ 5,6-9 └ 11. Pa ↔ ∃y(y=a ∧ Py) I↔ 1-4,5-10 12. ∀x[Px ↔ ∃y(y=x ∧ Py)] I∀ 11
[Exercise 33]
No premises
⊦ ∀x∀y∀z[x≠y ∧ y=z → x≠z]
(Same as Exercise 27) ┌ 1. a≠b ∧ b=c (Assumption) │ 2. a≠b E∧ 1 │ 3. b=c E∧ 1 │ ┌ 4. a=c (Assumption RAA) │ │ 5. c=b SYM 3 │ │ 6. a=b TRANS 4,5 │ │ 7. ⊥ I∧ 2,6 │ └ │ 8. a≠c I¬ 4-7 └ 9. (a≠b ∧ b=c) → a≠c I→ 1-8 10. ∀x∀y∀z[x≠y ∧ y=z → x≠z] I∀ 9
[Exercise 34]
- ∃xPx ∧ ∀x∀y(Px ∧ Py → x=y)
⊦ ¬∃x∃y[x≠y ∧ ∀z(Pz ↔ x=z ∨ y=z)]
1. ∃xPx ∧ ∀x∀y(Px ∧ Py → x=y) (Premise: exactly one P exists) 2. ∃xPx E∧ 1 3. ∀x∀y(Px ∧ Py → x=y) E∧ 1 ┌ 4. ∃x∃y[x≠y ∧ ∀z(Pz ↔ x=z ∨ y=z)] (Assumption RAA) │ ┌ 5. a≠b ∧ ∀z(Pz ↔ a=z ∨ b=z) (Assumption E∃) │ │ 6. a≠b E∧ 5 │ │ 7. ∀z(Pz ↔ a=z ∨ b=z) E∧ 5 │ │ 8. Pa ↔ a=a ∨ b=a E∀ 7 [z/a] │ │ 9. a=a =I │ │ 10. a=a ∨ b=a I∨ 9 │ │ 11. Pa E↔ 8,10 │ │ 12. Pb ↔ a=b ∨ b=b E∀ 7 [z/b] │ │ 13. b=b =I │ │ 14. a=b ∨ b=b I∨ 13 │ │ 15. Pb E↔ 12,14 │ │ 16. Pa ∧ Pb I∧ 11,15 │ │ 17. Pa ∧ Pb → a=b E∀ 3 [x/a,y/b] │ │ 18. a=b E→ 16,17 │ │ 19. a≠b ∧ a=b I∧ 6,18 │ └ │ 20. ⊥ E∃ 4,5-19 └ 21. ¬∃x∃y[x≠y ∧ ∀z(Pz ↔ x=z ∨ y=z)] I¬ 4-20
[Exercise 35]
No premises
⊦ ∃xPx ∧ ∀x∀y(Px ∧ Py → x=y) ↔ ∃x∀y(Py ↔ x=y)
(→) Assume ∃xPx ∧ ∀x∀y(Px ∧ Py → x=y) Let Pa (by E∃). For any b: - If Pb, then Pa ∧ Pb, so a=b - If a=b, then Pb (by Pa and substitution) Thus: ∀y(Py ↔ a=y) Therefore: ∃x∀y(Py ↔ x=y) (←) Assume ∃x∀y(Py ↔ x=y) Let ∀y(Py ↔ a=y) (by E∃) - Pa ↔ a=a, and a=a is true, so Pa. Thus ∃xPx. - If Pb ∧ Pc, then a=b and a=c, so b=c. Therefore: ∃xPx ∧ ∀x∀y(Px ∧ Py → x=y)
[Exercise 36]
No premises
⊦ ∃x∃y(x≠y) ↔ ∀x∃y(x≠y)
(→) Assume ∃x∃y(x≠y) Let a,b be such that a≠b. For any c: - If c=a, then c≠b (since a≠b) - If c≠a, then c≠a Thus: ∀x∃y(x≠y) (←) Assume ∀x∃y(x≠y) In particular, for some a: ∃y(a≠y) Let b be such that a≠b. Then ∃x∃y(x≠y) (taking x=a, y=b)