Fitch natural deduction proof of $\exists xF(x) \lor \exists xG(x) \vdash \exists x (F(x) \lor G(x))$

Question

I'm trying to create a natural deduction proof using the openlogicproject proof checker, but I just can't get it right. I have proven this on paper but I don't know how to get this right on the checker. This is what I have so far:

Can anyone please push me in the right direction?

Answer 1

The way you apply the rule $\exists E$ to eliminate the existential quantifier in your attempt is wrong. You can see that in a twofold way.

1. Syntactically: The syntax of the proof checker openlogicproject requires that, when you apply the rule $\exists E$, you provide two arguments:

   • the line of the formula with the existential quantifier that you want to eliminate, and
   • the (starting and end) lines of the subproof you used to eliminate the existential quantifier.

   In your attempt, you provided only the first argument.

2. Semantically: To eliminate the existential quantifier in a formula of the form $\exists x H(x)$, you suppose $H(a)$ for some $a$ and then you have to build a subproof with conclusion $C$ where $a$ is not free in $C$. This is what you are missing in your attempt, from a "semantic" point of view. Indeed, the conclusion of your subproof to eliminate the existential quantifier from $\exists x F(x)$ (and similarly from $\exists x G(x)$) is $F(a) \lor G(a)$, but $a$ is free in the assumption $F(a)$ you added to eliminate the existential quantifier.

The solution to the "semantic" problem is to avoid that $a$ occurs free in the conclusion of the suproof that eliminate the existential quantifier from $\exists x F(x)$ (and similarly from $\exists x G(x)$). How to do that? You can add an existential quantifier in front of $F(a) \lor G(a)$. You have to do it twice, once to eliminate the existential quantifier from $\exists x F(x)$, and once to eliminate the existential quantifier from $\exists x G(x)$.

So, a correct derivation in natural deduction of $\exists x (F(x) \lor G(x))$ from $\exists x F(x) \lor \exists x G(x)$ is the following (tested with openlogicproject):