TITLE: Predicate Logic: Factoring of Quantifiers (Clarification of Concept)
QUESTION [2 upvotes]: 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?

REPLY [0 votes]: 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.
{"set_name": "stack_exchange", "score": 2, "question_id": 577413}