Natural deduction derivation of $\forall x (B(x) \to C(x)) \vdash \neg \exists y (B(y) \land \neg C(y))$

Question

I am working on this derivative and I got 3 errors; however, the steps seem correct to me. I don't quite understand the explanations it gives beside the errors.

Reference: https://proofs.openlogicproject.org/

Answer 1

Line 2: Is not a proper application of the rule $\forall E$

That proof checker assumes that the term in the conclusion of $\forall E$ must be an individual constant, not a variable. The letter $y$ is interpreted as a variable, so you have to pick a letter that's understood by the proof checker as a constant symbol, for example $a$, instead.

Line 4: Cites too few ranges of lines for the rule $\exists E$

The proof checker is right, you applied the $\exists E$ rule incorrectly. From $\exists y (By \land \neg Cy)$ you may not conclude $By \land Cy$, for an arbitrary term $y$. Just because $By \land \neg Cy$ is true of some term doesn't mean we can be sure it is true of the particular term $y$. This would be the inference we can do with $\forall E$. Instead, the $\exists E$ rule looks like this:

You must assume $By \land \neg Cy$ for some term $y$ -- as before, this has to be a constant symbol, such as $b$ -- and for some convenient conclusion formula $\mathcal{B}$ that you can derive from this assumption, you may conclude $\mathcal{B}$ outside of the subproof by applying $\exists y$ on the assumption $\exists y (By \land \neg Cy)$ and the subproof from $Bb \land \neg Cb$ to $\mathcal{B}$. The idea of $\exists E$ is: If we know that $\mathcal{B}$ follows under the assumption of the existentially quantified over formula applied to a concrete term $b$, and we know that at least one such term exists, then we can conclude $\mathcal{B}$ for sure.
So instead of what you did, open a new subproof with assumption $Bb \land \neg Cb$ for a new constant symbol $b$, try to derive a convenient formula from it (reading the explanation of the next error will get you in the right direction about what a useful candidate for such a conclusion would be), and then close the subproof by doing $\exists E$ on the assumption $\exists y (By \land \neg Cy)$ and the subproof from $Bb \land \neg Cb$ to the new conclusion $\mathcal{B}$.

Line 8: Is not a proper application of the rule $\neg I$

The proof checker wants the contradiction you derived from $\exists y By \land Cy$ to be explicit in the form of $\bot$:

The contradiction between $Cy$ and $\neg Cy$ is so far only implicit. So you need an application of $\neg E$

on $Cy$ and $\neg Cy$ to show that the assumption led to a contradiction ($\bot$), then you can apply $\neg I$ on the subproof that ends with this contradiction.