Prove that: $\vdash \forall x \exists !y(y=x)$ Prove that: $$\vdash \forall x \exists !y(y=x)$$ in first order logic.
The first thing to do would be to write this as $$\forall x (\exists y(y=x) \land \forall y\forall z (y=x \land z=x \to y=z))$$
However, I cannot proceed from here. The equality axioms of first order theories don't seem to give me anything.
 A: This seems like a formal matter, thus I will describe how you do this formally using proof rules.
In order to prove
$$\forall x (\exists y(y=x) \land \forall y\forall z (y=x \land z=x \to y=z))$$
We show that 
$$\exists y(y=a) \land \forall y\forall z (y=a \land z=a \to y=z))$$
hold for a general constant $a$, and then if we want to be formal use $\forall$-introduction. 
To prove $\exists y(y=a)$ we may just notice that $a=a$ hold by $=-$introduction and then use $\exists$-intrudction to prove $\exists y(y=a)$. If we want to use the axioms for equality instead of the $=-$introduction rule, we may use $\forall x(x=x)$ and use $\forall-$elimination to conclude that $a=a$ hold and then continue as above.
In order to prove $\forall y\forall z (y=a \land z=a \to y=z))$ We assume that $b,c$ are general constants such that $b=a\land c=a$ hold. Now we may use $=$-elimination (or equality axioms) to conclude that $b=c$ hold. If we want to use the axioms for equality instead we may use the axiom $\forall x\forall y (y=x \wedge P(x)\rightarrow P(y))$, which should hold for any predicate $P$ Thus it also hold if P is the predicate $c=x$. In this case we get the formula
$$\forall x\forall y (y=x \wedge x=c\rightarrow y=c)$$
If we do $\forall-$eliminationputting in $a$ and $c$ we get $a=b\wedge b=c\rightarrow a = c$. which we may use to prove what we wanted.
To finnish the proof we use $\forall-introduction to conclude the formla we want to prove.
A: That was tricky! This isn't standard FOL, but you should be able to translate it if you are familiar with all the "subtleties" of standard FOL (I am not). I introduce the unary predicate $U$ to make the domain of discussion explicit. (This is not the usual practice in standard FOL.) Using this convention, we want to prove:
$$\forall x:[U(x) \implies \exists y:[U(y) \land [x=y \land \forall z:[U(z)\implies [x=z \implies y=z]]]]]$$
Proof:


*

*$U(a)$  (Premise)

*$a=a$  (Reflexivity)

*$U(c)$  (Premise)

*$a=c$  (Premise)

*$a=c \implies a=c$  (Conclusion, 4)

*$\forall z:[U(z) \implies [a=z \implies a=z]]$ (Conclusion, 3)

*$a=a \land \forall z:[U(z) \implies [a=z \implies a=z]]$  (Join, 2,6)

*$U(a) \land [a=a \land \forall z:[U(z) \implies [a=z \implies a=z]]]$  (Join, 1, 7)

*$\exists y:[U(y) \land [a=y \land \forall z:[U(z) \implies [a=z \implies y=z]]]$ (E Gen, 8)

*$\forall x:[U(x) \implies \exists y:[U(y) \land [x=y \land \forall z:[U(z)\implies [x=z \implies y=z]]]]]$ (Conclusion, 1)
