Prove there is a unique set $A$ such that for every set $B$, $A \cup B=B$ using Natural Deduction.

elementary-set-theoryfirst-order-logicnatural-deductionsolution-verification

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.

Best Answer

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.

Related Solutions

Proving $\forall x\forall y(P(x) \to Q(y)) \vdash \exists x(P(x) \to \forall y \, Q(y))$ using natural deduction.

Your proof in Fitch-style notation is absolutely correct, even though it can be simplified (see below). The problem is your formalization in the proof checker BoxProver, which is wrong because it does not corresponds exactly to your Fitch-style derivation, or more precisely it doesn't respect the (heavy) syntax used by BoxProver to deal with individual variables (as correctly suggested by @Casey in his comment).

The way BoxProver handles individual variables is not intuitive, so you did something wrong there (which is invisible in a Fitch-style derivation but is fundamental for BoxProver). Indeed, according to BoxProver's documentation, you have to create a box to declare the generic variable only for the rule $\forall_I$ introducing the universal quantifier, and not for the rule $\forall_E$ eliminating the universal quantifier or for the rule $\exists_I$ introducing the existential quantifier. So, your box introducing var [a] is not required and actually, for BoxProver, is wrong because it is not associated with any rule $\forall_I$. On the contrary, your box introducing var [b] is correct (also for BoxProver) because it is associated with the rule $\forall_I$ introducing $\forall y \, Q(y)$.

A correct formalization of your proof on BoxProver is below and here.

%abbrev
test : {P} {Q} {t} proof (all ([x] all ([y] P x => Q y)), |- exi ([x] P x => (all ([y] Q y)))) = [P] [Q] [t]

all ([x] all ([y] P x => Q y)) premise; [l1]
    (
        P t             assumption; [l2] 
        (
            var [b]
            (
                ~ Q b             assumption; [l3]
                all ([y] P t => Q y) by all_e t l1 ; [l4]
                P t => Q b by all_e b l4 ; [l5]
                Q b by imp_e l2 l5 ; [l6]
                bot by neg_e l6 l3
            ); [box1]
            ~ ~ Q b by neg_i box1 ; [l7]
            Q b by nne l7
        ); [box2]
        all([y] Q y) by all_i box2
    ); [box3]
    P t => all([y] Q y) by imp_i box3 ; [box4]
exi ([x] P x => (all ([y] Q y))) by exi_i t box4.

By the way, if you use the rule $\forall_E$ to elminate the universal quantifier, the instanciated variable should be declared somewhere, this is the reason why there are {t} and [t] in the "heading" of my derivation on BoxProver.

Note that to prove $\forall x\forall y(P(x) \to Q(y)) \vdash \exists x(P(x) \to \forall y \, Q(y))$ there is no need for using the rule DNE (or other non-constructive inference rules). You can derive $\forall x\forall y(P(x) \to Q(y)) \vdash \exists x(P(x) \to \forall y \, Q(y))$ directly, essentially by pushing $\forall y$ inside the formula and then inferring $\exists x$ form $\forall x$ (in a system where the domain is non-empty). Formally, the direct derivation using Fitch-style notation is the following.

$ \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\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 x \forall y(P(x) \to Q(y))}{ \fitch{2.\, P(a)}{ 3.\, \forall y(P(a) \to Q(y)) \Ae{1} 4.\, P(a) \to Q(b) \Ae{3} 5.\, Q(b) \ie{4,2} 6.\, \forall y \, Q(y) \Ai{5} }\\ 7.\, P(a) \to \forall y \, Q(y) \ii{2-6} 8.\, \exists x(P(x) \to \forall y \, Q(y)) \Ei{7} } $

A correct formalization of my derivation on BoxProver is below and here.

%abbrev
test : {P} {Q} {t} proof (all ([x] all ([y] P x => Q y)), |- exi ([x] P x => (all ([y] Q y)))) = [P] [Q] [t]

all ([x] all ([y] P x => Q y)) premise; [l1]
    (
        P t             assumption; [l2] 
        (
            var [b]
            all ([y] P t => Q y) by all_e t l1 ; [l3]
            P t => Q b by all_e b l3 ; [l4]
            Q b by imp_e l2 l4 
        ); [box1]
        all([y] Q y) by all_i box1
    ); [box3]
    P t => all([y] Q y) by imp_i box3 ; [box4]
exi ([x] P x => (all ([y] Q y))) by exi_i t box4.

As a final remark, to formally check your Fitch-style derivations I suggest to use the proof checker available here, which more user-friendly than BoxProver. In particular, here the syntax is less heavy and the way individual variables are handled is more intuitive, because you don't have to create a box to declare the generic variable in order to use the rule $\forall_I$ for the introduction of the universal quantifier. As a consequence, formal derivations here are more similar (actually, identical) to Fitch-style derivations in natural deduction.

Best Answer

Related Solutions

Proving $\forall x\forall y(P(x) \to Q(y)) \vdash \exists x(P(x) \to \forall y \, Q(y))$ using natural deduction.

Related Question