Are the following two equivalent?

A. $\left(\exists x:\phi(x)\right)\Rightarrow \psi$

B. $\forall x:\left(\phi(x)\Rightarrow \psi\right)$

where $\psi$ does not depend on $x$.

I think they are and reasoning is as follows: they are both true iff

1. $\psi$ is true
2. $\psi$ is false but $\exists x:\phi(x)$ is false in A. and $\forall x:\neg\phi(x)$ is true in B.

they are false iff $\psi$ is false and $\exists x:\phi(x)$ is true in A. and $\neg\forall x:\neg \phi(x)$ is true in B.

• Been awhile since I did formal logic with quantifiers, but I think they are, in fact, equivalent. Commented Aug 31, 2016 at 5:21

Yes, they are equivalent, in fact, this is equivalence is what is used to define $\exists$-Elimination in natural deduction.

If you accept that

$$\forall\langle x,~P(x)\rangle \lor Q \equiv \forall\langle x,~ P(x) \lor Q\rangle$$

which is the generalization of

$$(P_0 \land P_1 \land P_2 \dots) \lor Q \equiv (P_0 \lor Q) \land (P_1 \lor Q) \land (P_2 \lor Q) \dots$$

then the derivation is straightforward:

\begin{align} % \forall\langle x,~P(x) \implies Q\rangle % &= \forall\langle x,~ \lnot P(x) \lor Q\rangle \\ % &= \forall\langle x,~ \lnot P(x) \rangle \lor Q \\ % &= \lnot \exists \langle x,~ P(x) \rangle \lor Q \\ % &= \exists \langle x,~ P(x) \rangle \implies Q % \end{align}

This equivalence is commonly used to create a prenex normal form.

The case analysis and use of negation seems to check out.

• This should have been a comment Commented Aug 31, 2016 at 5:41
• No, I think it's an answer. Commented Aug 31, 2016 at 5:54