Proving that $\forall x\exists y(x = y)$

Question

How to prove in a formal system (like HFOL) the following formula $\forall x\exists y(x = y)$?

Obviously, we would like to use the axiom $x = x$ and then use a rule for introducing $\exists$, but how do we get $x = y$?

Answer 1

Here's a possible formal proof in a Fitch-style natural deduction system:

\begin{align*} & 1. ~ a = a \mathrm{~(a.k.a.~}(a = y) [ y / a ] \mathrm{)} & \qquad & {=}I \\ & 2. ~ \exists y, a = y \mathrm{~(a.k.a.~}(\exists y, x = y) [ x / a ] \mathrm{)} & \qquad & {\exists}I, 1 \\ & 3. ~ \forall x, \exists y, x = y & \qquad & {\forall}I, 2 \end{align*}