How to prove $(\forall x)(A\to B)\to(\exists x)A\to(\exists x)B$

Question

I am stuck on this one, I know I have to use Ax3 which is $$(\forall x)(A\to B)\to(\exists x)A\to(\exists x)B$$ and convert the existential quantifier to universal, but I have problem making it to become just as Ax3

The original was just like the following:

Show that |- $(\forall x)(A\to B)\to(\exists x)A\to(\exists x)B$

Hint: Use the definition of existential quantifier to eliminate ∃

You're missing parentheses, the formula is ill-formed. What rules and axioms do you have available? — Git Gud, Dec 06 '15 at 17:24
@MauroALLEGRANZA I believe it's the axoim quoted in the question. And I don't believe it's enough. — Colm Bhandal, Dec 06 '15 at 17:24
the parentheses are exactly like the one given in the question — swordgit, Dec 06 '15 at 17:41
@ColmBhandal the axoim is just the one i guess i might make use of — swordgit, Dec 06 '15 at 17:42
If you are working with an Hilbert-style proof system like Enderton's one, you need some basic meta-theorems, like Deduction Th and Generalization Th as well as $\vdash ( ∃ xβ →α) ↔ ∀x(β → α)$, where $x$ does not occur free in $α$. — Mauro ALLEGRANZA, Dec 06 '15 at 17:43

score 0 · Answer 1 · answered Dec 06 '15 at 17:27

0

I don't think you can use Ax3 to prove that property. I don't know what rules you're allowed to use, but I would do the following: Assume that $\forall x (A \implies B)$ and $\exists x A$. Then eliminate the existential to get some particular $A$. Then apply $\forall x (A \implies B)$ to get a particular $B$. Then use this $B$ as the witness to the final existential.

answered Dec 06 '15 at 17:27

Colm Bhandal

4,649

Ohh ok, got it! thank you! – swordgit Dec 06 '15 at 17:50

How to prove $(\forall x)(A\to B)\to(\exists x)A\to(\exists x)B$

1 Answers1