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

first-order-logicformal-proofslogicnatural-deductionsolution-verification

I am getting an error presumably in the last line (application of $\mathbf{E I}$ rule, i.e. introduction of the existential quantifier) using proof checker BoxProver. The proof seems correct, but nevertheless I couldn't find why it fails. Here it is:

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

all ([x] all ([y] P x => Q y)) premise; [l1]
(
    var [a]
    (
        P a             assumption; [l2] 
        (
            var [b]
            (
                ~ Q b             assumption; [l3]
                all ([y] P a => Q y) by all_e a l1 ; [l4]
                P a => 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 a => all([y] Q y) by imp_i box3
); [box4]
exi ([x] P x => (all ([y] Q y))) by exi_i box4.

And here is the proof in Fitch-style notation:

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

Best Answer

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.

Related Question