What's the converse proposition of $\forall x(P(x)\implies Q(x))$? As we all know, the converse proposition of $P\rightarrow Q$ is $Q\rightarrow P$. But when it comes to predicate logic, things may become different. Consider this:
$$(\forall x) (P(x)\rightarrow Q(x)).\tag{1}$$
Should its converse be $(\forall x) (Q(x)\rightarrow P(x))$?
I don't think so. In my opinion, we shouldn't neglect the quantifier $\forall$, which constrains $(Q(x)\rightarrow P(x))$.
Consider another proposition: $$(\exists x) (P(x)\rightarrow Q(x))\tag{2}.$$
When we deduce its converse, we can rewrite it as
$$(\forall x) P(x)\rightarrow (\exists x)Q(x) \tag{3}.$$ At this moment, we can readily obtain its converse: $(\exists x)Q(x)\rightarrow (\forall x) P(x)$.
Let's return to proposition (1) now. Unfortunately, I cannot rewrite it in the form of proposition (3). So I can't get its converse.
Did I make a mistake in the deduction above? And what's the converse of proposition (1)? Thanks a lot!
 A: [[A]] Concept of "Converse" is well Defined for things like "$P \rightarrow Q$" & "All $P$ are $Q$" , while that is not well Defined (or Does not even Exist) for Cases like $\forall X (\cdots)$ & $\exists X (\cdots)$ , hence in Such Cases , we try to convert to "$U \rightarrow V$" form , where we may (or may not) have to lose some Exactness/rigour.
[[B]] Your Example (2) $\iff$ (3) is a Case where we have the Exact Converse , we do not lose rigour.
[[C]] The "Exact Converse" of (1) seems like it Does not Exist , hence we have to lose some Exactness/rigour to try that.
$(\forall x) (P(x)\rightarrow Q(x))\tag{1}$
$\iff$
$\lnot \lnot (\forall x) (P(x)\rightarrow Q(x))$
$\iff$
$\lnot (\exists x) \lnot (P(x)\rightarrow Q(x))$
$\iff$
$\lnot (\exists x) \lnot (\lnot P(x) \lor Q(x))$
$\iff$
$\lnot (\exists x) P(x) \land \lnot Q(x)$
Till here , it is BiDirectional , here we are forced to use UniDirectional :
$\lnot (\exists x) P(x) \land \lnot Q(x)$
$\rightarrow$
$\lnot (\exists x) P(x) \land (\exists x) \lnot Q(x)$
$\iff$
$(\lnot (\exists x) P(x)) \lor (\lnot (\exists x) \lnot Q(x))$
$\iff$
$((\forall x) \lnot P(x)) \lor (\lnot (\exists x) \lnot Q(x))$
$\iff$
$(\exists x) \lnot Q(x) \implies (\forall x) \lnot P(x)\tag{4}$
While (1) $\rightarrow$ (4) , it is not (1) $\iff$ (4) , hence we are losing Exactness/rigour here. It is in the "$U \implies V$" form.
Hence the "Weak Converse" may be :
$(\forall x) \lnot P(x) \implies (\exists x) \lnot Q(x)\tag{7}$
$ \lnot (\exists x) P(x) \implies \lnot (\forall x) Q(x)\tag{8}$
[[D]] I think , this is the best we can get , online Articles [[ Eg https://nokyotsu.com/qscripts/2014/07/distribution-of-quantifiers-over-logic-connectives.html ]] all show that (1) has no Exact/rigorous Converse.
