I'm doing a very simple proof to show the following distributive property:
$$A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$$
The website proofwiki argues as follows:
$\displaystyle$ $x \in A \cap (A \cup B)$
$\iff$ {Definition of Set Union and Definition of Set Intersection}
$\displaystyle x \in A \land (x \in B \lor x \in C)$
$\iff$ {Conjunction is Left Distributive over Disjunction}
$\displaystyle (x \in A \land x \in B) \lor (x \in A \land x \in C)$
$\iff$ {Definition of Set Union and Definition of Set Intersection}
$\displaystyle x \in (A \cap B \cup (A \cap C)$
$\blacksquare$
The rewrites for the definitions they use are simply:
$x \in A \cup B \iff x \in A \lor x \in B$
$x \in A \cap B \iff x \in A \land x \in B$
My Problem
I think those definitions are a little informal and I wish to use the Set Builder notation for defining my sets properly:
$A \cup B = \{x: x \in A \lor x \in B\}$
$A \cap B = \{x: x \in A \land x \in B\}$
The use of these definitions cause problems in my proof because I need some semantics or some theorems on set builder notation to shuffle the symbols:
$\{x: x \in A \cap ( B \cup C)\}$
$\iff$ {My Definition of Set Intersection}
$\{x: x \in \{y: y \in A \land y \in (B \cup C) \} \}$
$\iff$ {My Definition of Set Union}
$\{x: x \in \{y: y \in A \land y \in \{z: z \in B \lor z \in C\} \}$
This part is confusing because I don't have any useful lemma/theorem to rewrite the variables that bind the inner sets using the variable in the outer scope. (like Lambda calculus has α-conversion, β-reduction)
My question: How can I get the semantics of this language of set builders so that I can rewrite the above statement where I can distribute the conjunction and how can I then re-use my definitions to get to the RHS?
Best Answer
The set-builder notation is an "operator" that has as input a formula and outputs a term (a "name").
The meaning of $\{ x \mid \varphi(x) \}$ is:
The fundamental property of the notation is:
What does it mean in terms of your problem ?
That $\{ x \mid x \in A \cap (B \cup C) \} = \{ x \mid x \in A \text { and } (x \in B \text { or } x \in C)\}$.
The formula $\varphi(x)$ used to "specify" the condition inside the set-builder notation is:
and you can work on it using distributivity trasforming it into the equivalent : $(x \in A \text { and } x \in B) \text { or } (x \in A \text { and } x \in C)$.