Logic, Language and Proof - please help me with 14.13 (Fitch)

Question

I'm not sure how to get line 23... to solve make all my a = e and b = d

Also, thank you to everyone who has helped me out before!!! I grately appreciate it :)

Answer 1

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\def\C#1{\operatorname{Cube}(#1)}$ You have realised that you must use three arbitrary variables to introduce three universal quantifiers.

Well, you should use them.   Eliminate the universal statement $\forall z~(\C z\to z=a\vee z=b)$ to each instance: $c, d, e$, to derive three conditional statements, then use the assumption to derive three disjunctions.

From there you may nest proof by cases to derive the target disjunction.   Note that the purpose of identity elimination in this is to 'eliminate' the variables $a$ and $b$.

$$\small\fitch{\exists x~\exists y~(\C x\wedge \C y\wedge x\neq y\wedge\forall z~(\C z\to z=x\vee z=y))}{\fitch{\boxed a~\exists y~(\C a\wedge \C y\wedge a\neq y\wedge\forall z~(\C z\to z=a\vee z=y))}{\fitch{\boxed b~\C a\wedge \C b\wedge a\neq b\wedge\forall z~(\C z\to z=a\vee z= b)}{\C a\\\C b\\ a\neq b\\\forall z~(\C z\to z=a\vee z=b)\\\fitch{\boxed e}{\fitch{\boxed d}{\fitch{\boxed e}{\C c\to c=a\vee c=b\\\C d\to d=a\vee d=b\\\C e\to e=a\vee e=b\\\fitch{\C c\wedge\C d\wedge\C e}{\C c\\\C d\\\C e\\c=a\vee c=b\\d=a\vee d=b\\e=a\vee e=b\\\fitch{c=a}{\fitch {d=a}{c=d\\c=d\vee c=e\vee d=e}\\\fitch{d=b}{~~\vdots\\c=d\vee c=e\vee d=e}\\c=d\vee c=e\vee d=e}\\\fitch{c=b}{~~\vdots\\c=d\vee c=e\vee d=e}\\c=d\vee c=e\vee d=e}\\ \C c\wedge\C d\wedge\C e\to c=d\vee c=e\vee c=d}\\\forall z~(\C c\wedge\C d\wedge\C z\to c=d\vee c=z\vee d=z)}\\\forall y~\forall z~(\C c\wedge\C y\wedge\C z\to c=y\vee c=z\vee y=z)}\\\forall x~\forall y~\forall z~(\C x\wedge\C y\wedge\C z\to x=y\vee x=z\vee y=z)\\ \exists y~(\C a\wedge\C y\wedge a\neq y)\\\exists x~\exists y~(\C x\wedge\C y\wedge x\neq y)\\ \exists x~\exists y~(\C x\wedge\C y\wedge x\neq y)\wedge \forall x~\forall y~\forall z~(\C x\wedge\C y\wedge\C z\to x=y\vee x=z\vee y=z)}\\ \exists x~\exists y~(\C x\wedge\C y\wedge x\neq y)\wedge \forall x~\forall y~\forall z~(\C x\wedge\C y\wedge\C z\to x=y\vee x=z\vee y=z)}\\ \exists x~\exists y~(\C x\wedge\C y\wedge x\neq y)\wedge \forall x~\forall y~\forall z~(\C x\wedge\C y\wedge\C z\to x=y\vee x=z\vee y=z)}$$