Predicate Logic: Factoring of Quantifiers (Clarification of Concept)

Question

Suppose we have, $\exists x\, P(x) \rightarrow \exists x\,Q(x)$
I know this is logically equivalent to $\exists x\, P(x) \rightarrow \exists y\,Q(y)$

Now, suppose we factor the quantifiers:
$\forall x (P(x) \rightarrow \exists y\,Q(y))$
$\exists \, y\,\forall x\,\, (P(x) \rightarrow Q(y))$

Now, suppose we change the order of the factoring:
$\exists\, y(\exists x P(x) \rightarrow Q(y))$
$\exists \, y\,(\exists x\,\, (P(x) \rightarrow Q(y))$
$\forall\,x\,\exists y(\,(P(x) \rightarrow Q(y))$

My understanding is that where the quantifiers are of different types, the order matters. In this case, depending the order of the factoring, the final order of the quantifiers is different. So, it looks like my understanding of the factoring rules is incorrect. Could someone clarify?

Answer 1

In this precise case, the order of factoring does not matter. (I asked the very same question to my logic professor last year). Since every application of a transformation rule results in an equivalent proposition, the order of the application of equivalence rules does not matter, even though it seems surprising that a sentence beginning with $\forall x\exists y$ should be equivalent to a proposition beginning with $\exists x \forall y$.

Answer 2

It is true that you can't arbitrarily swap quantifiers; for instance, you can't in $\forall x\exists y(xRy)$. What you've found is that you can swap around the quantifiers in a formula that's equivalent to one in which neither quantifier is in the scope of the other. Essentially, the quantifiers in your formula don't "interact" at all, while in my example the values of $y$ that satisfy $xRy$ will in general depend on the particular value for $x$.

Answer 3

Suppose we have $\exists x P(x) \Rightarrow \exists y Q(y)$. This can be viewed as a function which given an $x$ and a proof of $P(x)$ gives you an $y$ with a proof of $Q(y)$.

So the proposition is a function $(x:X, P(x)) \rightarrow (y:X, Q(y))$. You then can use currification which gives you a function which looks like this $(x : X) \rightarrow P(x) \rightarrow ((y:X), Q(y))$ or like $\forall x \left(P(x) \rightarrow \exists y Q(y)\right)$. At loud, you can say

given an $x$ and given a proof of $P(x)$ the proposition gives you an $y$ with a proof of $Q(y)$

But then you're stuck. You can't factor out the $y$ because it depends on the proof you give for $P(x)$ and on $x$. If you don't give every argument (aka the proof that $P(x)$ holds), the function (implication) can't give you the result as it can't evaluate.