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
    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).2012-05-01
  • 0
    In axioms 4 and 5, x does not occur free. Sorry, I forgot to mention that.2012-05-01
  • 0
    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.2012-05-01
  • 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