# If it is not all wrong, then I have a problem in line 25. Can anybody help, please?

1. ∃x ∃y (Cube(x) ∧ Cube(y) ∧ ¬x = y ∧ ∀z (Cube(z) → (z = x ∨ z = y)))
2. a∃y (Cube(a) ∧ Cube(y) ∧ ¬a = y ∧ ∀z (Cube(z) → (z = a ∨ z = y)))
3. bCube(a) ∧ Cube(b) ∧ ¬a = b ∧ ∀z (Cube(z) → (z = a ∨ z = b))
4. Cube(a) ∧ Cube(b) ∧ ¬a = b ∧ Elim : 3
5. ∀z (Cube(z) → (z = a ∨ z = b)) ∧ Elim : 3
6. c
7. d
8. eCube(c) ∧ Cube(d) ∧ Cube(e)
9. Cube(e) → (e = a ∨ e = b) ∀ Elim : 5
10. Cube(e) ∧ Elim : 8
11. e = a ∨ e = b → Elim : 9, 10
12. e = a
13. a = a = Intro
14. a = e = Elim : 12, 13
15. a = b ∨ a = e ∨ b = e ∨ Intro : 14
16. e = b
17. b = b = Intro
18. b = e = Elim : 16, 17
19. a = b ∨ a = e ∨ b = e ∨ Intro : 18
20. a = b ∨ a = e ∨ b = e ∨ Elim : 11, 12-15, 16-19
21. ∀z ((Cube(c) ∧ Cube(d) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∀ Intro : 8-20
22. ∀y ∀z ((Cube(c) ∧ Cube(y) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∀ Intro : 7-21
23. ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∀ Intro : 6-22
24. Cube(a) ∧ Cube(b) ∧ ¬a = b ∧ ∀x ∀y ∀z ((Cube(x) ∧ Cube(y) ∧ Cube(z)) → (a = b ∨ a = z ∨ b = z)) ∧ Intro : 4, 23
25. ∃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
26. ∃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
27. ∃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. – user3017 Oct 21 '17 at 22:07

```{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
```