# Prove an equivalence involving $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$.

This question is two-fold. First, I'm looking for feedback on a proof I wrote for the following problem. It's from exercise 18 in section 3.4 of Velleman's How To Prove It. The section deals with proofs involving conjunctions and biconditionals.

Suppose $\mathcal{F}$ and $\mathcal{G}$ are families of sets. Prove that $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$ iff $\forall A \in \mathcal{F} \forall B \in \mathcal{G}(A \cap B \subseteq \cup (\mathcal{F}\cap \mathcal{G}))$.

Here's my attempt at a proof. It proves both ways of the biconditional.

$\implies$ Suppose $\mathcal{F}$ and $\mathcal{G}$ are families of sets, and suppose $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$. Suppose that $A$ is an arbitrary set in $\mathcal{F}$ and $B$ is an arbitrary set in $\mathcal{G}$. Let $x$ be an arbitrary element of the set $A \cap B$. Thus, since $x \in A$ and $A \in \mathcal{F}$, $x \in \cup \mathcal{F}$. Similarly, since $x \in B$ and $B \in \mathcal{G}$, $x \in \cup \mathcal{G}$. Hence $x \in (\cup \mathcal{F}) \cap (\cup \mathcal{G})$. Then since $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$, it follows that $x \in \cup (\mathcal{F}\cap\mathcal{G})$. But we assumed that $x$ was an arbitrary element in the set $A \cap B$, and that $A$ and $B$ were arbitrary sets in $\mathcal{F}$ and $\mathcal{G}$, respectively. Therefore, if $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$, then $\forall A \in \mathcal{F} \forall B \in \mathcal{G}(A \cap B \subseteq \cup (\mathcal{F}\cap \mathcal{G}))$.

$\impliedby$ Suppose that for all sets $A$ in $\mathcal{F}$ and all sets $B$ in $\mathcal{G}$, $A \cap B \subseteq \cup (\mathcal{F} \cap \mathcal{G})$. Suppose $x$ is an arbitrary member of the set $(\cup\mathcal{F})\cap(\cup \mathcal{G})$. Then since $x \in \cup \mathcal{F}$, there must be a set $A'$ in $\mathcal{F}$ such that $x \in A'$. Likewise, since $x \in \cup \mathcal{G}$, there must be a set $B'$ in $\mathcal{G}$ such that $x \in B'$. Based on our assumption that for all sets $A$ in $\mathcal{F}$ and all sets $B$ in $\mathcal{G}$, $A \cap B \subseteq \cup (\mathcal{F} \cap \mathcal{G})$ and the fact that $x \in A' \cap B'$, it follows that $x \in \cup (\mathcal{F} \cap \mathcal{G})$. But we assumed $x$ was an arbitrary member of the set $(\cup \mathcal{F})\cap(\cup \mathcal{G})$. Therefore, if $\forall A \in \mathcal{F} \forall B \in \mathcal{G}(A \cap B \subseteq \cup (\mathcal{F}\cap \mathcal{G}))$, then $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$.

I have specific questions about the proof above. Is it too verbose? Am I backtracking too much when saying things such as 'because we assumed $P(x)$ and $Q(x)$, then $R(x)$'? Does this work for or against the proof? What about the mixing of the textual 'for all sets $A$ in $\mathcal{F}$' with the symbolic '$\forall A \in \mathcal{F}$'? Is there such a thing as too many 'suppose' being thrown together in a short amount of text? I used $A'$ and $B'$ to not interfere with the $A$ and $B$ in the assumptions. Does this make sense, is it necessary?

Secondly, I'm asking for some insight regarding equivalences of quantifiers. My first idea for proving the equivalence above was to use a chain of iff's or equivalences that started with $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G})$ and ended with $\forall A \in \mathcal{F} \forall B \in \mathcal{G}(A \cap B \subseteq \cup (\mathcal{F}\cap \mathcal{G}))$. However, after expanding the notation a bit I got stuck at the following two statements:

• $(\cup \mathcal{F})\cap(\cup \mathcal{G}) \subseteq \cup (\mathcal{F}\cap\mathcal{G}) \iff \forall x \left ( \left ( \exists A \in \mathcal{F}(x \in A) \wedge \exists B \in \mathcal{G}(x \in B) \right ) \implies x \in \cup \left ( \mathcal{F}\cap\mathcal{G} \right ) \right )$
• $\forall A \in \mathcal{F} \forall B \in \mathcal{G}(A \cap B \subseteq \cup (\mathcal{F}\cap \mathcal{G})) \iff \forall A \in \mathcal{F} \forall B \in \mathcal{G}\forall x \left ( x \in A \wedge x \in B \implies x \in \cup (\mathcal{F}\cap \mathcal{G})\right )$

If we assume the proof is correct, and we let $P(x)$ stand for $x \in \cup (\mathcal{F}\cap \mathcal{G})$, then the following must be true (I'm not sure if using $=$ here constitutes an abuse of notation, but I mean the two formulas around it are equivalent):

$\forall x \left ( \left ( \exists A \in \mathcal{F}(x \in A) \wedge \exists B \in \mathcal{G}(x \in B) \right ) \implies P(x) \right ) = \forall A \in \mathcal{F} \forall B \in \mathcal{G}\forall x \left ( x \in A \wedge x \in B \implies P(x)\right )$

However, I couldn't derive one from the other using the other equivalences introduced at this point (the distributive law for conjunction and disjunction, the DeMorgan laws, the negation quantifier laws, etc.). Is there a fundamental reason why it is not possible to do so? Is it a shortcoming of First Order Logic or something along those lines?

Edit: regarding the second portion of my question, I was lucky enough to stumble upon this other question that answered it. If I'm not wrong, you can actually prove the equivalence by recursively applying other conversion rules. In this case what I was missing was an introduction to the concept of Prenex normal form. I was able to prove the equivalence mechanically by applying the rules described in that Wikipedia article. However, the whole thing is messy and lengthy so I'm not including it here. (One could say it's left as an exercise to the reader.)

Having said that, I'm marking pjs36's reply as the answer to this question. Thanks!

Math does indeed require a lot of "Suppose..." statements. I usually write "Let [assumption 1], [assumption 2], ... , and [assumption $n$]." rather than multiple "suppose" statements, but that's just me. Most seem to naturally grow ruthlessly terse, I wouldn't worry much about it now. Plus, this theorem lends itself to nothing but symbol-chasing, so there isn't much you can do to liven it up like use a wider variety of language, etc.

The $\Rightarrow$ direction seemed perfectly fine to me. I had a minor stylistic issue with the $\Leftarrow$ portion, here:

Based on our assumption that for all sets $A$ in $\mathcal{F}$ [...]

I had to go back to see what you'd just shown, because that wall of assumptions really made me lose track of where we were in the proof. Since you'd just established that $x \in A'$ and $x \in B'$ I'd just say something like

Therefore $x \in A' \cap B' \subseteq \cup(\mathcal{F} \cup \mathcal{G})$, the latter inclusion by assumption, hence $x \in \cup (\mathcal{F} \cup \mathcal{G})$, which means $(\cup \mathcal{F}) \cap (\cup \mathcal{G}) \subseteq \cup (\mathcal{F} \cup \mathcal{G})$, as desired.

Again, it's all up to you, stylistically. But repeating all the assumptions you used, even if some were a while ago, makes me personally lose track of where you are in the proof. When concluding a proof, I'm lucky if I even write the conclusion (e.g., hence ____, as desired), let alone the premise(s).

I think using $A'$ and $B'$ was fine, and there are probably occasions when I do the equivalent of using $A$ and $B$, not differentiating my objects from those in the assumptions. I don't see either as being incorrect, or as better than the other (although differentiating is probably a good habit, in case you need to introduce multiple objects satisfying the same premise).

But, that's all just my opinion. I'm never studied logic beyond a very basic undergrad level, so my opinion on style may be all you should even consider.

From your question, it sounds like you might be looking for a proof like the following. Note that my notations are those of Dijkstra/Feijen/Gries/Schneider; see EWD1300 for more background.


We calculate as follows, starting at the left hand side, for any $\;\F,\G,X\;$: $$\calc (\bigcup \F) \cap (\bigcup \G) \;\subseteq\; X \op\equiv\hint{definitions of \;\subseteq,\cap,\bigcup\;} \langle \forall x : \langle \exists A : A \in \F : x \in A \rangle \land \langle \exists B : B \in \G : x \in B \rangle : x \in X \rangle \op\equiv \hints{merge \;\exists A\; and \;\exists B\; quantifications} \hint{-- to bring \;A,B\; together just as in the right hand side} \langle \forall x : \langle \exists A,B : A \in \F \land B \in \G : x \in A \land x \in B \rangle : x \in X \rangle \op{\tag{*}\equiv}\hint{logic: \;\langle \exists z :: P \rangle \then Q\; iff \;\langle \forall z :: P \then Q \rangle\;, if \;Q\; contains no \;z\;} \langle \forall x,A,B : A \in \F \land B \in \G \land x \in A \land x \in B : x \in X \rangle \op\equiv\hint{logic: reorder quantifications: \;A \in \F \land B \in \G\; doesn't contain \;x\;} \langle \forall A,B : A \in \F \land B \in \G : \langle \forall x : x \in A \land x \in B : x \in X \rangle \rangle \op\equiv\hint{definitions of \;\cap,\subseteq\;} \langle \forall A,B : A \in \F \land B \in \G : A \cap B \subseteq X \rangle \endcalc$$ which completes the proof.

Now, this proof doesn't have much variation in words, no "suppose"s and "assume"s: it is a chain of iffs, just like you were looking for. And I don't think that this is lengthy and messy... :-)

Also note the structure of this proof: we expand the definitions to go from the 'set level' to the 'logic level', then simplify and rearrange using the laws of logic, and finally go back to sets.

Finally, as you noted in your update to your question, a key step is $\ref *$, which one could prove in more detail as follows: $$\calc \langle \exists z :: P \rangle \then Q \op\equiv\hint{write \;\phi \then \psi\; as \;\lnot \phi \lor \psi\;} \lnot \langle \exists z :: P \rangle \lor Q \op\equiv\hint{DeMorgan} \langle \forall z :: \lnot P \rangle \lor Q \op{\tag{**}\equiv}\hint{\;Q\; does not contain \;z\;} \langle \forall z :: \lnot P \lor Q \rangle \op\equiv\hint{write \;\lnot \phi \lor \psi\; as \;\phi \then \psi\;} \langle \forall z :: P \then Q \rangle \endcalc$$ where the key step is obviously $\ref{**}$.