0
$\begingroup$

I added $\forall Y(\emptyset \cup Y = Y)$ as a premise; the exercise does not provide it.

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $ $ \fitch{1.\, \forall Y(\emptyset \cup Y = Y)}{ 2.\, \exists X\forall Y(X \cup Y = Y) \Ei{1} \fitch{3.\, \forall Y(C \cup Y=Y)}{ \fitch{4.\, \forall Y(D \cup Y=Y)}{ 5.\, C \cup D=D \Ae{3} 6.\, D \cup C = C \Ae{4} \vdots\\ C = D }\\ \forall Y(D \cup Y=Y) \to C=D\\ \forall Z(\forall Y(Z \cup Y=Y) \to C=Z)\\ k. \forall Y(C \cup Y=Y) \land \forall Z(\forall Y(Z \cup Y=Y) \to C=Z) \ci{4,k} k+1.\, \exists X[\forall Y(X \cup Y=Y) \land \forall Z(\forall Y(Z \cup Y=Y) \to X=Z] \Ei{k+1} }\\ \exists X[\forall Y(X \cup Y=Y) \land \forall Z(\forall Y(Z \cup Y=Y) \to X=Z] \Ee{3-k+1} } $

Is this proof skeleton correct ? Am I going in a good direction ?

EDIT:

Following advice in the comments, I made another version including 3 axioms as premises and deriving $\forall Y(\emptyset \cup Y = Y)$. I omitted the instantiation of the axioms. Going to include it in a final version.

$ \fitch{1.\, \forall x\neg(x \in \emptyset)\\2.\,\forall A\forall B \forall x(x \in A \cup B \leftrightarrow a \in A \lor a \in B)\\3.\,\forall A\forall B(\forall x(x \in A \leftrightarrow x \in B) \to A=B)}{ \fitch{4.\, a \in \emptyset \cup A}{ 5.\, a \in \emptyset \lor a \in A \\ 6.\, \neg(a \in \emptyset)\\ 7.\,a \in A }\\ \fitch{8.\, a \in A}{ 9.\, a \in A\\ 10.\,a \in \emptyset \lor a \in A\\ 11.\,a \in \emptyset \cup A }\\ 12.\, a \in \emptyset \cup A \leftrightarrow a \in A\\ 13.\,\, \forall Y(\emptyset \cup Y=\emptyset) \\ 14.\, \exists X\forall Y(X \cup Y=X) \\ \fitch{\forall Y(C \cup Y=Y)}{ \fitch{4.\, \forall Y(D \cup Y=Y)}{ 5.\, C \cup D=D \Ae{3} 6.\, D \cup C = C \Ae{4} \vdots\\ C = D }\\ \forall Y(D \cup Y=Y) \to C=D\\ \forall Z(\forall Y(Z \cup Y=Y) \to C=Z)\\ k. \forall Y(C \cup Y=Y) \land \forall Z(\forall Y(Z \cup Y=Y) \to C=Z) k+1.\, \exists X[\forall Y(X \cup Y=Y) \land \forall Z(\forall Y(Z \cup Y=Y) \to X=Z] \Ei{} }\\ \exists X[\forall Y(X \cup Y=Y) \land \forall Z(\forall Y(Z \cup Y=Y) \to X=Z] \Ee{} } $

P.S.: It is Example 3.6.2 of the book "How to Prove It" by Daniel Velleman.

$\endgroup$
6
  • 2
    $\begingroup$ $\forall Y~(\emptyset\cup Y=Y)$ should not be a premise but something which you derive from the axiom of empty set: $\exists S\forall T~\neg(T\in S)$ $\endgroup$
    – Graham Kemp
    Apr 28, 2020 at 1:17
  • $\begingroup$ Which axioms of set theory are you allowed to use? $\endgroup$
    – Taroccoesbrocco
    Apr 28, 2020 at 6:00
  • $\begingroup$ Thank you, @Graham Kemp. That's exactly what I was looking for. How would you derive it ? Any hint ? $\endgroup$
    – F. Zer
    Apr 28, 2020 at 9:39
  • $\begingroup$ @Taroccoesbrocco, the exercise does not clarify which axioms I am allowed to use. But I suppose the axiom Graham suggests and equality of sets. $\endgroup$
    – F. Zer
    Apr 28, 2020 at 9:41
  • 2
    $\begingroup$ I would suppose it depends on whether $\emptyset$, $\cup$ are functional symbols in the language or not. If they are, then probably the relevant axioms would be empty set $\forall x, \lnot(x \in \emptyset)$, union $\forall A \forall B \forall x, x \in A \cup B \leftrightarrow x \in A \vee x \in B$, and extensionality $\forall A \forall B, (\forall x, x \in A \leftrightarrow x \in B) \rightarrow A = B$. $\endgroup$
    – Daniel Schepler
    Apr 28, 2020 at 16:23

2 Answers 2

Reset to default
1
$\begingroup$

Clearly empty set $\cup$ A = A for all sets A.
Assume for all sets A, E $\cup$ A = A.
Thus E = E $\cup$ empty set = empty set.

Exercise. Prove the dual theorem that
the universal set U is the unique set with
U $\cap$ A = A, for all sets A.

$\endgroup$
0
$\begingroup$

Here is a proof in Fitch. I used $e$ for the empty set. Unfortunately this software does not have $\cup$ as a built-in symbol so I had to use my own $union$ function symbol.

I think the only tricky part may be the use of $=$ Elim on line 31:

enter image description here

enter image description here

$\endgroup$
3
  • $\begingroup$ Thank you so much ! Your proof is great ! $\endgroup$
    – F. Zer
    Apr 30, 2020 at 14:39
  • $\begingroup$ One question: In steps 24 thru 31, are you working with the empty set and an arbitrary set a ? $\endgroup$
    – F. Zer
    Apr 30, 2020 at 14:40
  • 1
    $\begingroup$ @F.Zer Yes. $e$ is the empty set, and $a$ is an arbitrary set ... $a$ is introduced in line 19, and since it is a 'new' constant, it takes the role of an arbitrary object, which is why on line 37 you can do a universal introduction $\endgroup$
    – Bram28
    Apr 30, 2020 at 14:46

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .