Language, Proof and Logic $14.12$ Solution $\left(\text{I need help}\tiny\overset{\cdot~\cdot}{\frown}\right)$

Question

I can only use Taut Con in this assignment but I dont know how to change line $15$ to line $16$ using it. Would appreciate any help!

I thought I could used $\lor~$Elim but I can't seem to do it.

Answer 1

Hint

$\begin{array}{|ll}a=c\\\hline a=a &\textsf{identity introduction}\\ c=a & \textsf{identity elimination}\\ \vdots\end{array}$

Answer 2

So you can do this the long way with $\vee$ elimination. I don't know the exact nomenclature that you are using, but here are the rough lines:

15) a = c $\vee$ b = c

16) a = c $\qquad$ Assumption

17) c = a $\qquad$ 16, Reflexivitiy of =

18) c = a $\vee$ c = b $\qquad$ 17, $\vee$ introduction

19) b = c $\qquad$ Assumption

20) c = b $\qquad$ 19, Reflexivitiy of =

21) c = a $\vee$ c = b $\qquad$ 17, $\vee$ introduction

22) c = a $\vee$ c = b $\qquad$ 15,16,18,19,21 $\vee$ elimination

$\\$

Does that make sense?

Answer 3

Alternatively, the universal eliminations could instantiate $x$ as $c$, $y$ as $a$, and $z$ as $b$, so to obtain:

$$\def\C#1{\operatorname{\sf Cube}(#1)}\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{\exists x~\exists y~(\C x\wedge\C y\wedge x\neq y) \\\forall x~\forall y~\forall z~(\C x\wedge\C y\wedge\C z\to x=y\vee x=z\vee y=z)}{\fitch{\boxed a~\exists y~(\C a\wedge\C y\wedge a\neq y)}{\fitch{\boxed b~\C a\wedge\C b\wedge a\neq b}{\fitch{\boxed c}{\fitch{\C c}{a\neq b\\\C a\wedge\C b\\\C c\wedge\C a\wedge\C b\\\forall y~\forall z~(\C c\wedge\C y\wedge\C z\to c=y\vee c=z\vee y=z)\\\forall z~(\C c\wedge\C a\wedge\C z\to c=a\vee c=z\vee a=z)\\\C c\wedge\C a\wedge\C b\to c=a\vee c=b\vee a=b\\c=a\vee c=b\vee a=b\\\fitch{c=a\vee c=b}{}\\\fitch{a=b}{\bot\\c=a\vee c=b}\\c=a\vee c=b}\\\C c\to c=a\vee c=b}\\\forall z~(\C z\to z=a\vee z=b)\\\C a\wedge\C b\wedge a\neq b\wedge\forall z~(\C z\to z=a\vee z=b)\\\exists y~(\C a\wedge\C y\wedge a\neq y\wedge\forall z(\C z\to z=a\vee z=y)}\\\exists y~(\C a\wedge\C y\wedge a\neq y\wedge\forall z(\C z\to z=a\vee z=y))\\\exists x~\exists y~(\C x\wedge\C y\wedge x\neq y\wedge\forall z~(\C z\to z=x\vee z=y))}\\\exists x~\exists y~(\C x\wedge\C y\wedge x\neq y\wedge\forall z~(\C z\to z=x\vee z=y))}$$