1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Git Gud Mar 5 '15 at 22:49
  • $\begingroup$ 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? $\endgroup$ – Sebastien Mar 5 '15 at 22:51
  • $\begingroup$ 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. $\endgroup$ – Git Gud Mar 5 '15 at 22:56
1
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.