How to prove $\vdash (\forall v_1 \,\exists v_2\, fv_1=v_2)$

Question

f is a one-place function symbol.

I just don't know where to start.

$\forall v_1 \,\exists v_2\, fv_1=v_2$ might come from $\exists v_2 \,fv_1=v_2$

Then I don't know how to deal with the "exists"

Answer 1

Here's the basic idea (we are working in FOL, first-order logic, where it is assumed that any function sign expresses a total function, i.e. function which produces a value for any input). By the identity rules you have

$$fa = fa.$$

That's because you have $\tau = \tau$ for any [closed] term $\tau$, and $fa$ is of course a term. Whence, by existential quantifier introduction (you can instantiate on any term),

$$\exists v_2\,fa = v_2$$

But $a$ was arbitrary, so you can use universal quantifier introduction to derive

$$\forall v_1\exists v_2\,fv_1= v_2.$$

How exactly you implement this idea inside your preferred deductive system will depend on its fine details.