I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can give the proof in your preferred system then I will be able to translate it (hopefully). I am using predicate calculus with equality. Also, I hope that it is clear from the context which symbol is variable, term, formula, held free, held fixed, and so forth. If not, please let me know.
$\exists !x (A(x))$ stands for $\exists x (A(x) \land \forall y (A(y) \implies y=x))$.
- $ \lnot \exists x (t=x \land \forall y (t=y \implies y=x)) \vdash \forall x(\lnot(t=x \land \forall y (t=y \implies y=x))) \vdash \lnot(t=t \land \forall y (t=y \implies y=t))$.
By negation of existential quantifier and by $\forall$– elimination where $t$ is free for $x$.
- $\vdash t=t$.
Axiom for equality.
- $\vdash t = y \implies y = t$, so $\vdash \forall y(t=y \implies y=t)$.
By property of equality and $\forall$-introduction where $y$ is free for $y$.
Combining three results we obtain a contradiction, so, by skipping some steps,
- $\vdash \lnot \lnot \exists x (t=x \land \forall y (t=y \implies y=x))
\vdash \exists x (t=x \land \forall y (t=y \implies y=x))$
By $\lnot$-introduction and $\lnot$-elimination.
Best Answer
I see that you are trying a proof by contradiction, which was my first inclination as well, but there is probably no need for it. Or at least, here is a direct proof done in my preferred system, Fitch:
Please note that the software implementation of this system treats $t$ as a variable, so I had to use $c$ instead of $t$