$(\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))$ ?

Question

Toda la cuestión está en el título: ¿es la equivalencia $$(\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))$$ verdadero (donde $\phi(x)$ (resp. $\psi(y)$ ) es una fórmula en la que $y$ (resp. $x$ ) no aparece)?

Me gustaría decir que sí, pero no estoy seguro: ¿tenemos $$(\forall x\in F (\phi(x)\lor \psi(y))) \Leftrightarrow ((\forall x\in F, \phi(x))\lor \psi(y))$$ En caso afirmativo, podría decir:

$$\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}$$

Answer 1

Sí, siempre que $x$ no es gratuito en $\psi_y$ entonces $\psi_y$ es constante con respecto a $x$ - su validez no se ve afectada por la variación $x$ de ninguna manera.
$$\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 $"}$$

---

Ligeramente más formalmente:

Suponiendo que $\psi_y$ entonces $\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$

Suponiendo que $\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)$

Por lo tanto, $\forall x (x\in F\to \phi_x \vee \psi_y) \vdash \forall x(x\in F\to \psi_x)\vee \psi_y$

Y puedes demostrar lo contrario.

---

PD: también debemos garantizar $F$ no está vacío.