Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this 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

In my answer to this post you can find the proof according to Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001) : theorem (Q2B) [see Ex 8, page 130].

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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