Equivalency of Two First-Order Formulae I was reading a paper, and I encountered a definition of some concept. The definition was of the form:
(+)  $\ \qquad\qquad (\exists x) \phi(x) \quad \Rightarrow \quad (\exists y) \psi(y)$
where $\phi$ and $\psi$ are two formulae.
I was wondering if the author's could write the above formula in the form:
(++) $\qquad\qquad (\forall x)(\exists y) \quad \phi(x) \Rightarrow \psi(y)$
That is, if (+) and (++) are equivalent.
Please prove the equivalency, or give a counterexample.
 A: (+) implies (++): suppose first that there is an $x_0$ for which $\varphi(x_0)$ holds, and that (+) holds. Let $y_0$ be a witness for (+) (must exist, since the antecedent holds); then $y_0$ is a witness for (++) for every $x$. If, on the other hand, $\forall(x)(\neg\varphi(x))$ holds, then (++) holds by vacuity (this includes the case in which the domain is empty). 
(++) implies (+): if the domain is empty, then (+) holds by vacuity. If the domain is not empty, and $\forall x(\neg\phi(x))$ holds, then (+) is true by vacuity again. And if there exists $x_0$ such that $\phi(x_0)$ holds, then by (++) there exists $y_0$ such that $\phi(x_0)\Rightarrow \psi(y_0)$ holds, and since $\phi(x_0)$ is true then $\psi(y_0)$ holds, hence (+) holds because the consequent is true.
A: Yes the two formulas say the same. $((\exists x)\phi(x))\to((\exists y)\psi(y))$ is equivalent to $(\lnot(\exists x)\phi(x))\lor((\exists y)\psi(y))$ which is equivalent to $((\forall x)\lnot\phi(x))\lor((\exists y)\psi(y))$ which is equivalent to $(\forall x)(\exists y)(\lnot\phi(x)\lor\psi(y))$ which is what you are looking for, namely $(\forall x)(\exists y)(\phi(x)\to\psi(y))$.
