# Velleman's Proof Designer problem 44

This is an exercise I didn't solve from the group of exercises present on Velleman's site that should be solved using Proof Designer (the little program that comes with the book).

Theorem:
If $\forall \mathcal{F} (\cup \mathcal{F} = A \rightarrow A \in \mathcal{F})$, then $\exists x (A=\{x\})$.

Before addressing my line of reasoning and the tentative proof, just few words on this specific problem. I find it interesting because it shows me that I still have problems figuring (and writing) properly existence results. About this, I would say that no matter what book on proof writing you take, this point is usually quickly considered and the examples are trivial, so not particularly useful for real mathematics. Probably this is related to the fact that existence theorems are in general the "hard ones" to be proven and to be thaught (I guess that they are the most difficult to be grasp by students), but I really don't know and I would like to know the opinions of experts.

Line of Reasoning:
I think the idea is that $x=\emptyset$ and $A=\{\emptyset\})$. In this way, what we have to assume should stand. Indeed, the antecedent should "bind" the nature of the family of sets and the consequence would follow.

Tentative Proof:
Let x be the empty set $\emptyset$. Thus, $\forall \mathcal{F} (\cup \mathcal{F} = \{\emptyset\} \rightarrow \{\emptyset\} \in \mathcal{F})$. Take $\mathcal{F}=\{\emptyset,\{\emptyset\}\}$. Then, we have $\cup \{\emptyset,\{\emptyset\}\} = \{\emptyset\} \rightarrow \{\emptyset\} \in \{\emptyset,\{\emptyset\}\}$, and the result is established.

PS: As I pointed out in another post, in general I try to be more consistent grammatically speaking when I write down proofs, and I avoid the use of logical symbols. I tend to do it when I have doubts about the content of the problem and here... I have no clue at all, so forgive it. Any feedback is more than welcome.

You are still quite far from proving the theorem. The issue seems to be that you misunderstood what the theorem is saying. I will try to explain it with a minimum of logical symbols, as you said you prefer that.

We are given a set $A$. First, let us investigate the premise:

$$\forall \mathcal F: \cup \mathcal F = A \to A \in \mathcal F$$

One could say that this expresses that $A$ is "union-irreducible": when it is the union of any collection of sets $\mathcal F$ (i.e. $\cup\mathcal F = A$), then it must be the case that one of these sets in $\mathcal F$ already is $A$.

It is important that we have the universal quantifier $\forall$ here, because we want to say that $A$ is "irreducible" under all unions, not just some particular ones.

Now let us turn to the conclusion:

$$\exists x: A = \{x\}$$

It does not say anything but: $A$ has precisely one element (formally: "there is an $x$ such that $x$ is the only element of $A$).

Thus, the statement of the theorem becomes: Any union-irreducible set $A$ consists of precisely one element.

In particular, we are not allowed to pick a set $A$, or, equivalently, the element $x \in A$. The theorem has to be proved for all union-irreducible sets.

For completeness, I will indicate a proof of the theorem. Let $A$ be a union-irreducible set.

We have the set $\mathcal F = \{\{x\}:x \in A\}$, comprising a singleton $\{x\}$ for each $x \in A$. It is trivial to see that $\cup\mathcal F = A$.

So now we need the conclusion to hold, i.e. $A \in \mathcal F$. But this means that there must exist an $x\in A$ such that $A = \{x\}$. The theorem follows.

• Ok, as you pointed out I did misunderstand the content of the theorem. Actually I think that this is a side effect of the fact that I was (and I am still involved in) trying to prove it with Proof Designer in which, as far as I learned, you have to name the $x$. So, correct me if I am wrong, the content of the theorem is more general and it is about any singleton, but we can actually come out with a specific implementation that follows the steps of my tentative proof (Proof Designer driven)? – Kolmin May 22 '13 at 10:00
• As @Hagen points out, your tentative proof is in the wrong direction; I don't know anything about Proof Designer, so I don't know how you can translate either of our arguments to fit in that program's structure. Although I think that you should be able to define the $\mathcal F$ I introduced above in terms of $A$ in Proof Designer, and derive the conclusion from there. – Lord_Farin May 22 '13 at 10:13
• +1 That's one elegant $\mathcal F$ to rule them all instead of my two step approach. – Hagen von Eitzen May 22 '13 at 10:17
• As I said I do have big problems with existence theorems, so one last naive question. In Lord_Farin's proof we let $A$ be something and then we establish that the assumption stands. Can I say that the take-home lesson for existence results is that, after establishing the object (even without naming it) we need to go backwards to show that the object satisfies the assumption? If this is the case, I see why I don't have to be particularly scared by the implication assumption that I cannot "divide" by MP or similar. [Sorry for this very naive question] – Kolmin May 22 '13 at 10:21
• Since implications can be false only if their premise is true (material implication), we may safely assume it. In this case, I did that by saying that "$A$ is union-irreducible". In general, having established a candidate for an existence proof, you will always have to verify that it indeed has the sought properties. (Although sometimes this step can be (very) trivial.) – Lord_Farin May 22 '13 at 10:37

Yes, Lord_Farin's elegant proof can be done in Proof Designer. Start by applying the "Universal Instantiation" command to the hypothesis $\forall \mathcal{F}(\bigcup\mathcal{F} = A \to A \in \mathcal{F})$. This allows you to plug in whatever you want for $\mathcal{F}$. You can go ahead and plug in exactly the set suggested by Lord_Farin: $\{\{x\} \mid x \in A\}$.

• Are you the real DJV? – Git Gud May 26 '13 at 19:44

Your tentative proof is the wrong direction: If $A$ is a singleton (in fact a very specific singleton) then the antecedent holds.

Under the assumption of $\forall \mathcal{F} (\cup \mathcal{F} = A \rightarrow A \in \mathcal{F})$, first show $\exists x(x\in A)$. In other words: Show that $A=\emptyset$ implies $\neg\forall \mathcal{F} (\cup \mathcal{F} = A \rightarrow A \in \mathcal{F})$ or equivalently $\exists \mathcal{F} (\cup \mathcal{F} = A \land A \notin \mathcal{F})$. You can do this by specifically exhibiting such $\mathcal F$.

Next show $(x\in A\land y\in A)\rightarrow x=y$. Again, exhibit $\mathcal F$ with $\cup \mathcal{F} = A \land A \notin \mathcal{F}$.

You should already know that $x\in A$ and $(x\in A\land y\in A)\rightarrow x=y$ implies $A=\{x\}$.

• Ok, so the first part is established by some sort of contradiction, while with the second I show that $A$ needs to be a singleton. Just wondering, is it a good way to overcome the problem of having an implication as assumption? Cause, I have problems dealing with them when they stand alone (so to speak) like in this case. – Kolmin May 22 '13 at 10:09