-1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Magdiragdag Feb 7 '18 at 18:31
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.