0
$\begingroup$

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} } $

$\endgroup$
3
  • 2
    $\begingroup$ Could you write your attempt in a more readable way? Otherwise it is very difficult to check where is the error. $\endgroup$ Apr 17, 2020 at 19:01
  • 1
    $\begingroup$ Just updated the post. $\endgroup$
    – F. Zer
    Apr 17, 2020 at 19:14
  • $\begingroup$ I got it! I edited my answer with a solution and an exhaustive (I hope) explanation. $\endgroup$ Apr 18, 2020 at 13:33

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
11
  • 1
    $\begingroup$ Thank you. Your solution is neater. I made some progress but I still have one error. Here is a screenshot of exactly what is missing: Proof $\endgroup$
    – F. Zer
    Apr 18, 2020 at 1:03
  • $\begingroup$ I tried your interesting suggestion but I am still getting an error. $\endgroup$
    – F. Zer
    Apr 18, 2020 at 1:04
  • $\begingroup$ @F.Zer - Can you add the assumption $\exists x \, x=x$ to that attempt? What do you get? I'm sorry, I don't know BoxProver and I don't have time to learn its syntax. $\endgroup$ Apr 18, 2020 at 5:11
  • 1
    $\begingroup$ I looked briefly at the syntax rules on the help page and noticed the universal introduction variable is boxed and existential introduction variable is not. Is the variable "a" being treated as to be universally generalized here? Does the prover let you infer Ax(Px -> AxQy)? Does the prover let you do the proof without line 2 boxing and specifying variable "a"? That's the only thing I can think of. $\endgroup$
    – Casey
    Apr 18, 2020 at 7:31
  • 1
    $\begingroup$ Great! I use a proof system that uses basically the same technique for variables so boxing both variables looked like a problem to me. $\endgroup$
    – Casey
    Apr 18, 2020 at 16:07

You must log in to answer this question.

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