A simple question about quantifiers and negation in conditionals

In classical propositional logic $$\neg(A \to B) \equiv A \land \neg B$$. In predicate logic, therefore, do we have $$\neg (\forall x (\phi(x) \to \psi(x)) \equiv \forall x (\phi(x) \land \neg \psi(x))$$?

Or, instead, would $$\neg (\forall x (\phi(x) \to \psi(x)) \equiv \exists x (\phi(x) \land \neg \psi(x))$$?

Or do we have, in fact, $$\neg (\forall x (\phi(x) \to \psi(x)) \equiv \forall x (\phi(x) \land \neg \psi(x))\equiv \exists x (\phi(x) \land \neg \psi(x))$$. If this is the case, then why do we have $$\forall x (\phi(x) \land \neg \psi(x))\equiv \exists x (\phi(x) \land \neg \psi(x))$$ ?

More generally, I don't understand how we understand a formula like (1), as opposed to one like (2):

$$(1)\;\;\forall x (\phi(x) \land \neg \psi(x))$$

$$(2)\; \;\forall x (\phi(x) \to \neg \psi(x))$$

Edit: It is still unclear to me what the precise difference between (1) and (2) is (and their variants $$sans$$ negation). (1) requires the truth of $$\phi(x)$$ for all substitution instances, whereas (2) does not. Is that all?

But then, what might be a natural sentence of English which expresses (1)? Would it be something like (1')?

(1') Every man dances and he doesn't play football

Take it step by step, first apply quantifier duality, and next negate the predicate.

\begin{align}&\lnot\forall x~\big(\phi(x)\to\psi(x)\big)\\[1ex]\equiv ~&\exists x~\lnot\big(\phi(x)\to\psi(x)\big)\\[1ex]\equiv ~&\exists x~\big(\phi(x)\land\lnot\psi(x)\big)\end{align}

• Ah, yes. What about the difference between (1) and (2)? – Edward.Lin Dec 11 '18 at 10:40
• I have revised my question – Edward.Lin Dec 11 '18 at 10:48

In general $$\neg\forall x\;P(x)$$ and $$\exists x\;\neg P(x)$$ are the equivalent.

In words: "not all $$x$$ have property $$P$$" is the same as "some $$x$$ exists that has not property $$P$$".

So if $$P(x)$$ is $$\phi(x)\to\psi(x)$$ then it appears that $$\neg\forall x\;[\phi(x)\to\psi(x)]$$ and $$\exists x\;\neg [\phi(x)\to\psi(x)]$$ are equivalent.

Since $$\neg [\phi(x)\to\psi(x)]$$ and $$\phi(x)\wedge\neg\psi(x)$$ are equivalent, there is also equivalence with $$\exists x\;[\phi(x)\wedge\neg\psi(x)]$$