- ∃x ∃y (Cube(x) ∧ Cube(y) ∧ ¬x = y ∧ ∀z (Cube(z) → (z = x ∨ z = y)))
- a∃y (Cube(a) ∧ Cube(y) ∧ ¬a = y ∧ ∀z (Cube(z) → (z = a ∨ z = y)))
- bCube(a) ∧ Cube(b) ∧ ¬a = b ∧ ∀z (Cube(z) → (z = a ∨ z = b))
- Cube(a) ∧ Cube(b) ∧ ¬a = b ∧ Elim : 3
- ∀z (Cube(z) → (z = a ∨ z = b)) ∧ Elim : 3
- c
- d
- eCube(c) ∧ Cube(d) ∧ Cube(e)
- Cube(e) → (e = a ∨ e = b) ∀ Elim : 5
- Cube(e) ∧ Elim : 8
- e = a ∨ e = b → Elim : 9, 10
- e = a
- a = a = Intro
- a = e = Elim : 12, 13
- a = b ∨ a = e ∨ b = e ∨ Intro : 14
- e = b
- b = b = Intro
- b = e = Elim : 16, 17
- a = b ∨ a = e ∨ b = e ∨ Intro : 18
- a = b ∨ a = e ∨ b = e ∨ Elim : 11, 12-15, 16-19
- ∀z ((Cube(c) ∧ Cube(d) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∀ Intro : 8-20
- ∀y ∀z ((Cube(c) ∧ Cube(y) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∀ Intro : 7-21
- ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∀ Intro : 6-22
- Cube(a) ∧ Cube(b) ∧ ¬a = b ∧ ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∧ Intro : 4, 23
- ∃x ∃y (Cube(x) ∧ Cube(y) ∧ ¬x = y ∧ ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (x = y ∨ x = z ∨ y = z))) ∃ Intro : 24
- ∃x ∃y (Cube(x) ∧ Cube(y) ∧ ¬x = y) ∧ ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (x = y ∨ x = z ∨ y = z)) ∃ Elim : 3-25, 2
- ∃x ∃y (Cube(x) ∧ Cube(y) ∧ ¬x = y) ∧ ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (x = y ∨ x = z ∨ y = z)) ∃ Elim : 1, 2-26 Goals ∃x ∃y (Cube(x) ∧ Cube(y) ∧ ¬x = y) ∧ ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (x = y ∨ x = z ∨ y = z)) May use intro/elim rules for t/f connectives. May use intro/elim rules for identity. May use intro/elim rules for quantifiers. May use full Taut Con.
-
Hint: You need to unpack everything in line 8 and do a lot of work with the disjunctions.– user3017Commented Oct 21, 2017 at 22:07
Add a comment
|
1 Answer
{1} 1. ƎxƎy[Cx & Cy & ~x=y & ∀z[Cz → (z=x ∨ z=y)]] Prem
{2} 2. Ǝy[Ca & Cy & ~a=y & ∀z[Cz → (z=a ∨ z=y)]] Assum. TD(a)
{3} 3. Ca & Cb & ~a=b & ∀z[Cz → (z=a ∨ z=b)] Assum. TD(b)
{3} 4. Ca & Cb & ~a=b 3 &E
{3} 5. ∀z[Cz → (z=a ∨ z=b)] 3 &E
{6} 6. Cc & Cd & Ce Assum.
{6} 7. Cc 6 &E
{3} 8 . Cc → (e=a ∨ e=b) 5 UE
{3,6} 9 . c=a ∨ c=b 7,8 MP
{6} 10. Cd 6 &E
{3} 11. Cd → (d=a ∨ d=b) 5 UE
{3,6} 12. d=a ∨ d=b 10,11 MP
{6} 13. Ce 6 &E
{3} 14. Ce → (e=a ∨ e=b) 5 UE
{3,6} 15. e=a ∨ e=b 13,14 MP
{16} 16. c=a Assum. (9 1st Disj.)
{17} 17. d=a Assum. (12 1st Disj.)
{16,17} 18. c=d 16,17 =E
{16,17} 19. c=d ∨ c=e ∨ d=e 18 ∨I (12 1st Conc.)
{20} 20. d=b Assum. (12 2nd Disj.)
{21} 21. e=a Assum. (15 1st Disj.)
{16,21} 22. c=e 16,21 =E
{16,21} 23. c=d ∨ c=e ∨ d=e 22 ∨I (15 1st Conc.)
{24} 24. e=b Assum. (15 2nd Disj.)
{20,24} 25. d=e 20,24 =E
{20,24} 26. c=d ∨ c=e ∨ d=e 25 ∨I (15 2nd Conc.)
{16,20} 27. c=d ∨ c=e ∨ d=e 15,21,23,24,26 ∨E (12 2nd Conc.)
{16} 28. c=d ∨ c=e ∨ d=e 12,17,18,19,27 ∨E (9 1st Conc.)
{29} 29. c=b Assum. (9 2nd Disj.)
{30} 30. d=a Assum. (12 1st Disj.)
{31} 31. e=a Assum. (15 1st Disj.)
{30,31} 32. d=e 30,31 =E
{30,31} 33. c=d ∨ c=e ∨ d=e 32 ∨I (15 1st Conc.)
{34} 34. e=b Assum. (15 2nd Disj.)
{29,34} 35. c=e 29,34 =E
{29,34} 36. c=d ∨ c=e ∨ d=e 35 ∨I (15 2nd Conc.)
{29,30} 37. c=d ∨ c=e ∨ d=e 15,31,33,34,36 ∨E (12 1st Conc.)
{38} 38. d=b Assum. (12 2nd Disj.)
{29,38} 39. c=d 29,38 =E
{29,38} 40. c=d ∨ c=e ∨ d=e 39 ∨I (12 2nd Conc.)
{29} 41. c=d ∨ c=e ∨ d=e 12,30,37,38,40 ∨E (9 2nd Conc.)
{3,6} 42. c=d ∨ c=e ∨ d=e 9,16,28,29,41 ∨E
{3} 43. (Cc & Cd & Ce) → (c=d ∨ c=e ∨ d=e) 6,43 CP
{3} 44. ∀z[(Cc & Cd & Cz) → (c=d ∨ c=z ∨ d=z)] 43 UI
{3} 45. ∀y∀z[(Cc & Cy & Cz) → (c=y ∨ c=z ∨ y=z)] 44 UI
{3} 46. ∀x∀y∀z[(Cx & Cy & Cz) → (x=y ∨ x=z ∨ y=z)] 45 UI
{3} 47. Ǝy[Ca & Cy & ~a=y] 4 EI
{3} 48. Ǝxy[Cx & Cy & ~x=y] 47 EI
{3} 49. Ǝxy[Cx & Cy & ~x=y] & ∀x∀y∀z[(Cx & Cy & Cz) → (x=y ∨ x=z ∨ y=z)] 46,48 &I
{2} 50. Ǝxy[Cx & Cy & ~x=y] & ∀x∀y∀z[(Cx & Cy & Cz) → (x=y ∨ x=z ∨ y=z)] 2,3,49 EI
{1} 51. Ǝxy[Cx & Cy & ~x=y] & ∀x∀y∀z[(Cx & Cy & Cz) → (x=y ∨ x=z ∨ y=z)] 1,2,50 EI