$(\forall (x,y) \in F\times G, \phi(x) \lor \psi(y) ) \Leftrightarrow (\forall x\in F, \phi(x)) \lor (\forall y\in G, \psi(y))$?

All the question is in the title: is the equivalency $$(\forall (x,y) \in F\times G, \phi(x) \lor \psi(y) ) \Leftrightarrow (\forall x\in F, \phi(x)) \lor (\forall y\in G, \psi(y))$$ true (where $\phi(x)$ (resp. $\psi(y)$) is a formula where $y$ (resp. $x$) doesn't appear)?

I would like say yes, but I'm not sure: do we have $$(\forall x\in F (\phi(x)\lor \psi(y))) \Leftrightarrow ((\forall x\in F, \phi(x))\lor \psi(y))$$ If yes, I could say:

\begin{aligned} (\forall (x,y) \in F\times G, \phi(x) \lor \psi(y) )&\Leftrightarrow (\forall y\in F(\forall x\in G (\phi(x)\lor \psi(y))) \\ &\Leftrightarrow (\forall y\in F((\forall x\in G, \phi(x))\lor \psi(y)) \\&\Leftrightarrow (\forall x\in F, \phi(x)) \lor (\forall y\in G, \psi(y)) \end{aligned}

• You do have that and the statements are equivalent. But if you feel the need to ask, then you're not satisfied with your proof. – Git Gud Mar 5 '15 at 22:49
• Indeed, I'm not pretty sure of $(\forall x\in F (\phi(x)\lor \psi(y))) \Leftrightarrow ((\forall x\in F, \phi(x))\lor \psi(y))$. Is that a kind of axiom of logic? – Sebastien Mar 5 '15 at 22:51
• Well, it depends on the axioms. But first let me rectify a small detail. In the 'equivalence' you mention, neither side is a statement because $y$ isn't quantified. If they aren't statements, you can't say they are equivalent, that stuff it reserved for statements. However in the actual proof $y$ is quantified and it's correct. How you want to prove it depends on your tools. An informal proof wouldn't be much different from what I argue in the last comment here. – Git Gud Mar 5 '15 at 22:56

Yes, as long as $x$ is not free in $\psi_y$, then $\psi_y$ is constant with respect to $x$ - its validity is not affected by varying $x$ in any way.
$$\forall x (x\in F\to \phi_x \vee \psi_y)\quad\text{ iff }\quad\forall x (x\in F\to \phi_x) \vee \psi_y$$

$$\text{any x in F satisfies either \phi_x or \psi_y" iff either \psi_y is true or every x in F satisfies \phi_x"}$$

Slightly more formally:

Assuming $\psi_y$, then $\psi_y, \forall x (x\in F\to \phi_x \vee \psi_y) \vdash \forall x(x\in F\to \psi_y) \vdash \psi_y$

Assuming $\neg\psi_y$, $\neg \psi_y, \forall x (x\in F\to \phi_x \vee \psi_y) \vdash \forall x(x\in F\to \phi_x)$

Therefore, $\forall x (x\in F\to \phi_x \vee \psi_y) \vdash \forall x(x\in F\to \psi_x)\vee \psi_y$

And you can prove the converse.

PS: we should also ensure $F$ is not empty.

• If $F$ is empty there is no problem. – Git Gud Mar 6 '15 at 1:31