To explain the title, in proving $X \times Y = \emptyset \iff X = \emptyset \vee Y = \emptyset$, we have the following

\begin{align*} X \times Y = \emptyset &\iff \forall x \forall y \left((x,y) \notin X \times Y\right)\\ &\iff \forall x \forall y \left(x \notin X \vee y \notin Y\right) \\ &\iff \forall x (x \notin X) \vee \forall y (y \notin Y) \\ &\iff X = \emptyset \vee Y = \emptyset , \end{align*}

and in particular going from the second to the third line, we can (?) split up the statement $(x \notin X \vee y \notin Y)$ and quantifiers $\forall x \forall y$ into two separate statements each with its own quantifier. I'm not sure why this is true. It seems obvious that this is true, but is there a proof, or is it axiomatic? Or is it not true at all?

Thanks in advance - recently deleted a completely wrong proof of this statement so hopefully this one is at least correct

  • $\begingroup$ If you are writing or reading predicate logic proofs, how is it you haven't found out what proof rules, rule schemas & identities you are allowed to use/expect? (Rhetorical.) $\endgroup$
    – philipxy
    Mar 31, 2023 at 2:39
  • $\begingroup$ You said "rhetorical", but I actually answered that question in the reply to Lee's answer below. $\endgroup$
    – jacob
    Mar 31, 2023 at 9:14

1 Answer 1


You could insert the following intermediate steps: \begin{align*} \forall x \forall y \left(x \notin X \vee y \notin Y\right) & \iff \forall x\bigl( \forall y (x \notin X \vee y \notin Y) \bigr) \\ & \iff \forall x\bigl(x \notin X \vee \forall y (y \notin Y)\bigr) \\ & \iff \bigl(\forall x (x \notin X)\bigr) \vee \bigl(\forall y (y \notin Y) \bigr) \end{align*} The second and third steps are applications of one of the Laws of Quantifier Movement in predicate logic, which says that if the free variable $x$ does not occur in the statement $P$ then you can move a universal $x$ quantifier into an "or" statement that involves $P$, in the following manner: $$\forall x (P \vee Q(x)) \iff P \vee (\forall x Q(x)) $$ I think of this as an "infinite" version of de Moivre's Theorem: if $x_1,x_2,...$ is a "list" of the values of $x$ then $$(P \vee Q(x_1)) \wedge (P \vee Q(x_2)) \wedge \cdots \iff P \vee (Q(x_1) \wedge Q(x_2) \wedge \cdots) $$

  • $\begingroup$ Thanks Lee. I'm reading an analysis book which is attempting to touch on proving statements rigorously using first order logic in the first chapter, but they don't mention this at all. Perhaps the author has tried to do too much. $\endgroup$
    – jacob
    Mar 30, 2023 at 12:13
  • $\begingroup$ What I said about deMoivre's Theorem is a little careless, the implication is only one way. But I don't have time to fix it right now. $\endgroup$
    – Lee Mosher
    Mar 30, 2023 at 12:26
  • $\begingroup$ cheers for the heads up $\endgroup$
    – jacob
    Mar 30, 2023 at 14:02
  • $\begingroup$ Okay, fixed now. $\endgroup$
    – Lee Mosher
    Mar 30, 2023 at 14:24
  • $\begingroup$ By the way, regarding the author doing "too much", even a first analysis course might assume, as a prerequisite, some knowledge of predicate calculus including laws of quantifiers. Books at that level sometimes have a "chapter zero" to bring a student up to speed on set theory and maybe also on predicate logic, but not always. $\endgroup$
    – Lee Mosher
    Mar 30, 2023 at 15:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .