2
$\begingroup$

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.

  • 0
    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)$.2014-05-15

1 Answers 1

1

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].