I've been working on proving equivalent formulas using equivalences in predicate logic however I'm stuck trying to prove that these two formulas are equivalent:
$ \forall x (A(x) \Rightarrow \exists y B(x,y)) $
$ \forall x \exists y (A(x) \Rightarrow B(x,y)) $
The only step I've managed to get so far is by swapping the quantifies on the second formula:
$ \exists y \forall x (A(x) \Rightarrow B(x,y)) $
But I'm not sure how to proceed from here. I've checked what equivalences I can use but I don't see any that I can use here anymore.
Does anyone see a way to go further from here?
(1) $\lnot \exists x X \equiv \forall x \lnot X$ or alternatively $\exists x \lnot X \equiv \lnot \forall x X$
(2) $ \lnot (X \implies Y) \equiv (X \cdot \lnot Y)$
$\forall x (A(x) \implies \exists y B(x, y) )$
By double negation
$\lnot \lnot \forall x (A(x) \implies \exists y B(x, y) )$
By (1) $\lnot\exists x (\lnot (A(x) \implies \exists y B(x, y) ))$
By (2) $\lnot\exists x ((A(x) \cdot \lnot \exists y B(x, y) ))$
By (1) $\lnot\exists x ((A(x) \cdot \forall y \lnot B(x, y) ))$
Since A does not depend on y,
$A(x) \equiv \forall y A(x)$
$\lnot\exists x ((\forall y A(x) \cdot \forall y \lnot B(x, y) ))$
$\lnot\exists x (\forall y (A(x) \cdot\lnot B(x, y) ))$
By (1) $\forall x \lnot(\forall y (A(x) \cdot\lnot B(x, y) ))$
By(1) $\forall x (\exists y \lnot(A(x) \cdot\lnot B(x, y) ))$
By(2) $\forall x (\exists y (A(x) \implies B(x, y) ))$