MHB Show Sentences Proof: "Hey Again! (Wasntme)

[evinda]

Hey again! (Wasntme)

I want to show the following:

• If $t \in A$, then $t \subseteq \cup A$
• $\cup \varnothing=\varnothing$
• $ \cup \{ a \}=a$

• Let $x \in t$.
  
  So, $\exists t (t \in A \wedge x \in t) \rightarrow x \in \cup A$.
  Therefore, $t \subseteq A$.
  
• $$x \in \cup \varnothing \leftrightarrow \exists b (b \in \varnothing \wedge x \in b)$$
  
  The empty set $\varnothing$ contains no elements, so there is no $b$ such that $b \in \varnothing$, so there is no $x$, such that $x \in \cup \varnothing$.
  
  Therefore, $\cup \varnothing=\varnothing$.
  
• $$x \in \cup \{ a \} \leftrightarrow \exists b (b \in \{ a \} \wedge x \in b) \leftrightarrow (b=a \wedge x \in b) \leftrightarrow x \in a$$
  
  Therefore, $\cup \{ a \}=a$.

Could you tell me if it is right or if I have done something wrong? (Thinking)

 

[Evgeny.Makarov]

Very well! One minor remark about the first problem. You have a set called $t$. In the scope of this proof, it may be considered a constant. I would not call a variable bound by $\exists$ by the same name $t$. The object immediately following $\exists$ is a variable, not a constant, so when you say $\exists t$ you introduce a new variable that happens to have the same name as the existing object $t$. Then, for example, saying "There exists some $t$ (in fact, it is equal to the set $t$ mentioned above)" would be awkward. So I would say
\[
x\in t\land t\in A\to\exists u\;(x\in u\land u\in A)\to x\in\bigcup A.
\]
Saying that the last implication holds by definition of $\bigcup A$ would not hurt, either. But overall, good job.

 

[evinda]

Very well! One minor remark about the first problem. You have a set called $t$. In the scope of this proof, it may be considered a constant. I would not call a variable bound by $\exists$ by the same name $t$. The object immediately following $\exists$ is a variable, not a constant, so when you say $\exists t$ you introduce a new variable that happens to have the same name as the existing object $t$. Then, for example, saying "There exists some $t$ (in fact, it is equal to the set $t$ mentioned above)" would be awkward. So I would say
\[
x\in t\land t\in A\to\exists u\;(x\in u\land u\in A)\to x\in\bigcup A.
\]
Saying that the last implication holds by definition of $\bigcup A$ would not hurt, either. But overall, good job.

I understand! Thank you very much! (Nod)