Is $\forall x\exists y (p(x) \lor q(y)) \implies \exists y\forall x (p(x) \lor q(y))$ correct? I am stuck with a question, and wanted to ask here.
Let $p$ and $q$ be predicates
I know that $\forall x\exists y p(x ,y) \implies \exists y\forall x p(x ,y)$ isn't always right.
But, what goes on when there is two predicates like the one in the title. I'm having hard times to evaluate this proposition: $\forall x\exists y (p(x) \lor q(y)) \implies \exists y\forall x (p(x) \lor q(y)) $
I would be happy if you help me to understand this.
All answers will be appreciated, thank you.
 A: Yes, that holds. In fact, they are equivalent, i.e. we have:
$\forall x\exists y (p(x) \lor q(y)) \iff \exists y\forall x (p(x) \lor q(y))$ 
The key difference with the general $\forall x\exists y p(x,y)$, where you cannot swap the quantifiers, is that in $\forall x\exists y (p(x) \lor q(y)) $ you do not have any predicate that refers to both $x$ and $y$ at once. Hence, you apply the Prenex Equivalence Laws:
Prenex Laws
Where $\varphi$ is any formula and where $x$ is not a free variable in $\psi$:
$ \forall x \ \varphi \lor \psi \Leftrightarrow \forall x (\varphi \lor \psi)$
$  \psi \lor \forall x \ \varphi  \Leftrightarrow \forall x (\psi \lor \varphi)$
$ \exists x \ \varphi \lor \psi \Leftrightarrow \exists x (\varphi \lor \psi)$
$  \psi \lor \exists x \ \varphi  \Leftrightarrow \exists x (\psi \lor \varphi)$
Therefore:
$$\forall x\exists y (p(x) \lor q(y)) \iff $$
$$\forall x (p(x) \lor \exists y \ q(y)) \iff $$
$$\forall x p(x) \lor \exists y \ q(y) \iff $$
$$\exists y  (\forall x p(x) \lor \ q(y)) \iff $$
$$\exists y\forall x (p(x) \lor q(y))$$
A: Suppose $\forall x\exists y(p(x)\vee p(y))$ true. Therefore, there is no $x$ s.t. for all $y$, $p(x)$ and $q(y)$ are false. 


*

*So, if $p(x)$ is always true, then $p(x)\vee q(y)$ always true. 

*Suppose there is an $x$ s.t. $p(x)$ false. By hypothesis, there is $y$ s.t. $q(y)$ true. Therefore, for all $x$, $p(x)\vee q(y)$ true. 
The claim follow. 
A: The statement
$$∀x∃y (p(x) \lor q(y)) \implies ∃y∀x (p(x) \lor q(y))$$
is true in classical logic and my proof requires excluded middle principle.
If $\forall x p(x)$ is true then clearly $∃y∀x (p(x) \lor q(y))$ is true as well.
On the other hand, if $\neg\forall x p(x)$, then $\exists x\neg p(x)$.
By assumption, $∀x∃y (p(x) \lor q(y))$ hence there exists $y$ such that $q(y)$ is true.
Consequently, $∃y∀x (p(x) \lor q(y))$ holds also in this case.
A: Both $\forall x\exists y (p(x) \lor q(y))$ as well as $\exists y\forall x (p(x) \lor q(y))$ are equivalent to
$$\bigg(\forall x.p(x)\bigg) \lor \bigg(\exists y.q(y)\bigg)$$
although the 2nd is only equivalent when the universe is empty.  If the universe is empty the implication doesn't hold.
