Deduction for $\exists v_1 \forall v_2 \lnot f(v_2) = v_1 \vdash \exists v_1 \exists v_2 \lnot v_2 =v_1$

Question

I'm trying to find a deduction for $$\exists v_1 \forall v_2 \lnot f(v_2) = v_1 \vdash \exists v_1 \exists v_2 \lnot v_2 =v_1$$

with these axioms & lemma.

---

For any function $f$ and relation $R$
E1) $x=y$
E2) $[(x_1=y_1) \land (x_2=y_2) \land ... \land (x_n=y_n)] \rightarrow f(x_1, x_2, ... , x_n)=f(y_1, y_2, ... ,y_n)$
E3) $[(x_1=y_1) \land (x_2=y_2) \land ... \land (x_n=y_n)] \rightarrow (x_1, x_2, ... , x_n) \in R \leftrightarrow (y_1, y_2, ... ,y_n) \in R$

For any term $t$ substitutable for a variable $x$ in a formula $\phi$
Q1) $(\forall x)(\phi) \rightarrow \phi^x_t $
Q2) $\phi^x_t \rightarrow (\exists x)(\phi)$

Propositional Consequence (PC)
$(\left\{\phi_1, \phi_2, ... \phi_n \right\}, \phi)$ is an inference rule where $(\phi_1 \land \phi_2 \land ... \land \phi_n) \rightarrow \phi$ is an instance of tautology.

Quantifier Rule (QR)
$(\left\{ \psi \rightarrow \phi \right\}, \psi \rightarrow (\forall x)(\phi)), (\left\{\phi \rightarrow \psi \right\}, (\exists x)(\phi) \rightarrow \psi)$ are inference rules where $x$ is not free in $\psi$

Lemma
For a set of formula $\Sigma$ and a formula $\phi$
$\Sigma \vdash \phi$ if and only if $\Sigma \vdash \forall x \phi$

---

This is the part of my deduction
(1) $ v_2 = v_1 \rightarrow f(v_2)=f(v_1)$ & E1
(2) $\lnot f(v_2)=f(v_1) \rightarrow \lnot v_2 = v_1$ & PC from 1
(3) $\exists v_1 \forall v_2 \lnot f(v_2)=v_1$ & non-logical axiom
(4) $\forall v_1 \exists v_1 \forall v_2 \lnot f(v_2)=v_1$ & Lemma
(5) $\forall v_1 \exists v_1 \forall v_2 \lnot f(v_2)=v_1 \rightarrow \exists f(v_1) \forall v_2 \lnot f(v_2)=f(v_1)$ & Q1
(6) $\exists f(v_1) \forall v_2 \lnot f(v_2)=f(v_1)$ & PC from 4, 5

If I can somehow get $\forall v_2 \lnot f(v_2)=f(v_1)$, then I can use Q1 and (2) to get $\lnot v_2 = v_1$ then I can apply some few more rules to complete the deduction but I'm stuck here.

Any Ideas? Thanks.

Answer 1

I would do a proof by contradiction.

So, assuming $$\neg \exists v_1 \exists v_2 \ \lnot v_2 =v_1$$ you get

$$\forall v_1 \forall v_2 \ v_2 =v_1 \tag{*}$$

(meaning that there is exactly one object in the domain)

Then, given the premise that $$\exists v_1 \forall v_2 \lnot f(v_2) = v_1$$ you know that for some object $a$:

$$\forall v_2 \lnot f(v_2) = a$$

and thus specifically:

$$\lnot f(a) = a$$

But from $(*)$ we get:

$$f(a) = a$$

and thus we have a contradiction.

I'll leave it to you to make this proof idea into an actual formal proof.