I managed to prove existence for the following theorem: $$\forall A\in\mathcal{P}(U)\ \exists!B\in\mathcal{P}(U)\ \forall C\in\mathcal{P}(U)\ (C\setminus A=C\cap B)$$ where U is any set. My assumption is that $B=U\setminus A$, and it works for existence, but I'm stuck with proving uniqueness part with $B$ being defined this way.

For uniqueness we need to prove $$\forall B'\in\mathcal{P}(U)\ \forall C\in\mathcal{P}(U)\ (\ (C\setminus A=C\cap B')\rightarrow B'=B)$$ where A is arbitrary element of $\mathcal{P}(U)$ but I don't how to connect $x\in B'$ or $x\in B$ to the assusmed identitiy $C\setminus A=C\cap B'$.

Any pointers are much appreciated.


Here is my attempt of proof.

Proof: Let $A$ be an arbitrary element of $\mathcal{P}(U)$ and let $B=U\setminus A$.
Existence: Let $C$ be an arbitrary element of $\mathcal{P}(U)$. $(\rightarrow)$ Let $x$ be an arbitrary element of $C\setminus A$. Since $C\subseteq U$, then $x\in U\setminus A$. Therefore $x\in C\cap B$. $(\leftarrow)$ Let x be an arbitrary element of $C\cap B$. Then $x\in C\cap (U\setminus A)$, so we can conclude $x\in C\setminus A$.
Uniqueness: Let $B'$ be an arbitrary element of $\mathcal{P}(U)$ and suppose $\forall C\in\mathcal{P}(U)(C\setminus A=C\cap B')$.
$(B'\subseteq B)$ Since $B'\in\mathcal{P}(U)$, then in particular $B'\setminus A=B'\cap B'=B'$, so clearly $B'\cap A=B'\cap (U\setminus B)=\varnothing$. Then $\forall x(x\not\in B'\lor x\not\in U\lor x\in B)$, which is equivalent to $\forall x(x\in B'\cap U\rightarrow x\in B$). Since $B'\subseteq U$, $B'\cap U=B'$, we now have $\forall x(x\in B'\rightarrow x\in B)$, and therefore $B'\subseteq B$.
$(B\subseteq B')$ Let $C=B$. Then $B\setminus A=B\cap B'$, and because $B\cap A=\varnothing$, we have $B=B\cap B'$, so we can conclude $B\subseteq B'$.

  • 2
    $\begingroup$ If you have $B'\setminus A=B'\cap B'=B'$, then $A$ doesn't share a single element with $B'$, they are disjoint. That's where $B'\cap A=B'\cap (U\setminus B)=\varnothing$ is coming from. Although $A=U\setminus B$ seems arbitrary actually comes from the $B=U\setminus A$ proof of which is left out. In the $(B\subseteq B')$, $B\cap A=\varnothing$ comes from the assumed $B=U\setminus A$, and because they're disjoint, $B\setminus A=B$. There is no favourable answer to your last question. It's just long hours, experimentation, and experience. I hate there's no real method to it, but it is what it is. $\endgroup$ – LavaScornedOven Apr 5 '16 at 22:17
  • $\begingroup$ @DanielMak In your bounty comment you say, among other things: "For example, how does one know letting B=U∖A and C=B would work?" Have you checked my answer, for a way to calculate that U∖A is the value for B? $\endgroup$ – Marnix Klooster Apr 7 '16 at 23:11
  • $\begingroup$ @MarnixKlooster I tried understanding your answer, but unfortunately I don't understand the notations you are using; obviously I understand those that are written in standard 1st order logic and set theory but others like '::' are things I have never seen before $\endgroup$ – Daniel Mak Apr 8 '16 at 15:07
  • $\begingroup$ @LavaScornedOven If only I could reward you with the bounty; your comment has resolved most of my confusions! I only have two quick follow ups: A=U∖B: How did you know? I can prove it by proving ∀x(x∈A↔x∈U∖B), but I am sure you didn't do it this way, somehow I think you proved by deducing from the meaning of these formulae alone, I tried really hard but I still couldn't crack it, could you give me a hint please? B∩A=∅: Is it because if B=U∖A then B∩A=U∖A ∩ A, i.e. ∀x(x∈U∧~x∈A∧x∈A), and ~x∈A∧x∈A implies nothing can satisfy this (and thus no member - empty set)? Thank you so much! orz $\endgroup$ – Daniel Mak Apr 9 '16 at 15:07
  • $\begingroup$ You can show $A=U\setminus B$ with $$U\setminus B=U\cap B^C=U\cap (U\setminus A)^C=U\cap(U\cap A^C)^C=U\cap(U^C\cup (A^C)^C)=U\cap(U^C\cup A)=U\cap A=A$$ I tried to leave every step so you could follow the proof more easily. Note that the proof uses just basic set alebra (see Algebra of Sets). As for $B\cap A=\varnothing$, by applying set algebra, $$B\cap A=(U\setminus A)\cap A = U\cap A^C\cap A=U\cap\varnothing=\varnothing$$ which is similar to your approach, but avoids dealing with set elements. $\endgroup$ – LavaScornedOven Apr 12 '16 at 10:17

Hint: Plug $B$ into the $C$ from the $B'$ assertion to get that $B\setminus A\subseteq B'$, and similarly for $B'$ into $C$ from the $B$ assertion, to have $B'\setminus A\subseteq B$.

Now show that $B'\setminus A=B'$ and $B\setminus A=B$ (plug $C=\varnothing$ into both assertions) and you are done.

  • $\begingroup$ I don't see any inference rule that would bring me from supposing $x\in B$ or $x\in B'$ to $x\in C$ or $x\not\in C$, except for proving by cases $x\in C$ and $x\not\in C$. If not going for elementhood, how exactly do I plug B or B' into C? $\endgroup$ – LavaScornedOven Dec 8 '12 at 12:57
  • 2
    $\begingroup$ If the claim is true for all $C$ then it is true for $C=B'$, for example, therefore $B'\setminus A=B\cap B'$. Show that $B'\setminus A=B'$ then you have that $B'=B\cap B'$; similarly $B=B\cap B'$. From this you can directly deduce the conclusion of equality. $\endgroup$ – Asaf Karagila Dec 8 '12 at 13:02
  • $\begingroup$ Oh, I see. (Palmface...) :) I missed the fact that I can plug into $C\setminus A=C\cap B'$ whatever I wont from $\mathcal{P}(U)$. Thanks for the help. $\endgroup$ – LavaScornedOven Dec 8 '12 at 13:18
  • 4
    $\begingroup$ Facepalm would do, but check this out: d24w6bsrhbeh9d.cloudfront.net/photo/3657230_700b.jpg $\endgroup$ – LavaScornedOven Dec 8 '12 at 14:49
  • 2
    $\begingroup$ @Daniel: I didn't think it was you. Sorry I didn't reply to you. I wanted to tell you that you should ask these questions as a separate thread; but I forgot and it slipped my mind, and then you already set the bounty so it was futile. $\endgroup$ – Asaf Karagila Apr 5 '16 at 15:16

HINT: An easier way is to show that if $B\ne U\setminus A$, there is a $C\in\wp(U)$ such that $C\setminus A\ne C\cap B$. You’ll want to consider two cases, $B\cap A\ne\varnothing$ (loosely, ‘$B$ is too big’) and $A\cup B\ne U$ (loosely, ‘$B$ is too small’).


Here is my attempt at a direct proof for this theorem. Note that $A$, $B$, etc. denote subsets of our 'universe' $U$, and $x$ denotes an element of U.

We start out by simplifying everything inside $\exists!$, as follows: $$ \begin{align*} & \langle \forall C :: C \setminus A \;=\; C \cap B \rangle \\ \equiv & \;\;\;\;\;\text{"extensionality; definitions of $\setminus$ and $\cap$"} \\ & \langle \forall C :: \langle \forall x :: x \in C \land x \notin A \;\equiv\; x \in C \land x \in B \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: move $x \in C$ out of $\equiv$, then into range"} \\ & \langle \forall C :: \langle \forall x : x \in C : x \not\in A \equiv x \in B \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: what Dijkstra calls shunting"} \\ & \langle \forall x : \langle \exists C :: x \in C \rangle : x \not\in A \equiv x \in B \rangle \\ \equiv & \;\;\;\;\;\text{"range is true: take $C:=\lbrace x \rbrace$"} \\ & \langle \forall x :: x \not\in A \equiv x \in B \rangle \\ \equiv & \;\;\;\;\;\text{"definition of complement; extensionality"} \\ & B = A^c \\ \end{align*} $$ This trivially proves existence and uniqueness, but for completeness I will spell it out anyway. Using the following not-so-well-known definition of $\exists!$ (where $w$ is a fresh variable) $$ \langle \exists! v :: P \rangle \;\equiv\; \langle \exists w :: \langle \forall v :: P \:\equiv\: v=w \rangle \rangle $$ the original theorem is proven as follows: $$ \begin{align*} & \langle \forall A :: \langle \exists! B :: \langle \forall C :: C \setminus A \;=\; C \cap B \rangle \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"by the above calculation"} \\ & \langle \forall A :: \langle \exists! B :: B = A^c \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"by the above definition"} \\ & \langle \forall A :: \langle \exists B' :: \langle \forall B :: B = A^c \:\equiv\: B = B' \rangle \rangle \rangle \\ \Leftarrow & \;\;\;\;\;\text{"what Dijkstra calls Leibniz' rule"} \\ & \langle \forall A :: \langle \exists B' :: A^c = B' \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: what Dijkstra calls the one-point rule"} \\ & \langle \forall A :: \mathrm{true} \rangle \\ \equiv & \;\;\;\;\;\text{"logic"} \\ & \mathrm{true} \\ \end{align*} $$

Hope this helps...

  • $\begingroup$ Where could I find material with that proving "style"? It looks interesting to explore. $\endgroup$ – LavaScornedOven Mar 19 '13 at 12:13
  • $\begingroup$ @LavaScornedOven See the note at the end of another answer of mine./11994. $\endgroup$ – Marnix Klooster Mar 19 '13 at 13:39
  • $\begingroup$ Thanks for the reply. I'm currently investigating different approaches, and your suggestion comes as very helpful. $\endgroup$ – LavaScornedOven Mar 20 '13 at 2:14

Let $B := U \setminus A$.
Let $B' \subseteq U$ be any subset that satisfies the hypothesis: $\forall C \in \mathcal P(U) (C \setminus A = C \cap B')$

Case I:
Assume $x \in B' \setminus B$.

\begin{align*} \implies & x \in A \\ \text{Let } & C = \{x\} \\ \implies & \left( C \setminus A \right) = \varnothing \ne C = \left( C \cap B' \right) \\ \implies & \impliedby (contradiction) \end{align*}

Case II:
Assume $y \in B \setminus B'$.

\begin{align*} \implies & y \notin A \\ \text{Let } & C = \{y\} \\ \implies & \left( C \setminus A \right) = C \ne \varnothing = \left( C \cap B' \right) \\ \implies & \impliedby (contradiction) \end{align*}

$\implies B'=B$ is unique.


I think this even might be an easier proof:


Existence. Let $A$ be an arbitrary element of $\mathscr P(U)$ and let $B = U\setminus A ∈ \mathscr P(U)$. Then clearly for every $C ∈ \mathscr P(U)$, $C ∩ B = C ∩ U\setminus A = C\setminus A$.

Uniqueness. Let $A$ be an arbitrary element of $\mathscr P(U)$. To see that $B$ is unique, suppose that $B' ∈ \mathscr P(U)$ and for all $C ∈ \mathscr P(U)$, $C\setminus A = C ∩ B'$. Then in particular, taking $C = U$, we can conclude that $U\setminus A = U ∩ B' = B'$. So we have $B' = U\setminus A = B.$


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.