# 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

(∃x) (A → B) ↔ (A → (∃x)(B))

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

1) (A → (B → A)

2) (A → (B → C)) → ((A → B) → (A → C))

3) (~A → ~B) → (B → A)

4) ((∀x)A → A)

5) (∀x)(A → B) → (A → (∀x)B)

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

Is (∃x)A the same as ~(∀x)~A ?

Is ~(∀x)~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