# 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$

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.

• Note that $\forall v_2 \lnot f(v_2) = f(v_1)$ can never be true: take $v_2 = v_1$. So you won't be able to derive that. – Magdiragdag Feb 7 '18 at 18:31

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.