# Proving that if $x$ is not free in $A$, then $(\exists x)(A\to B)\leftrightarrow(A\to(\exists x)(B))$

Assuming $x$ does not occur free in $A$, prove that

$$(\exists x (A \to B)) \leftrightarrow (A \to ( \exists x B))$$

using any of the following axioms; MP, HS, or the Deduction Theorem.

1) $A \to (B \to A)$

2) $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

3) $(\neg A \to \neg B) \to (B \to A)$

4) $(\forall x A) \to A$

5) $(\forall x (A \to B)) \to (A \to \forall x B)$

First of all, I don't know how to convert the existential quantifier into the universal quantifier.

Is $\exists x A$ the same as $\neg (\forall x) \neg A$?

Is $\neg(\forall x) \neg A$ the same as $A$?

Second, I'd appreciate your help with the original question.

-
If you have double negation ($\neg\neg A\to A$), then $(\exists x)(A)$ is equivalent to $\neg((\forall x)(\neg A))$. But $\neg(\forall x)(\neg A)$ is not generally the same as $A$. Presumably, you'll use the fact that $x$ is not free in $A$ (which I think is part of the assumptions of your axiom 5 as well). – Arturo Magidin May 1 '12 at 5:37
In axioms 4 and 5, x does not occur free. Sorry, I forgot to mention that. – Mark13426 May 1 '12 at 5:40
Given that you don't have any axioms for $\exists$ quantifier, it is natural to assume that it has been introduced as a shorthand for $\lnot (\forall x) (\lnot A)$. But you need to check your notes (or textbook) to be sure. – Levon Haykazyan May 1 '12 at 11:49
The proof system is similar to Mendelson's one, but is lacking of Generalization rule : if $\vdash \varphi$, then $\vdash \forall x \varphi$. I suppose you are using Enderton's system (which use modus ponens as only rule of inference). Note: ia Ax 4) we do not have the restriction : $x \notin FV(A)$. – Mauro ALLEGRANZA May 15 '14 at 9:36