Natural deduction in first-order logic

first-order-logicformal-proofslogicnatural-deductionproof-theory

I've sat for more than an hour now and I don't understand how I'm supposed to solve the task below.

$\{\forall x(P(x) \land Q(x)), \exists x\neg P(x)\} \vdash \exists x \neg Q(x) $

So I'm a bit confused if I'm supposed to use RAA or $\neg$ introduction when solving this using natural deduction.

$$
\dfrac{\exists x \, \lnot P(x) \qquad \dfrac{\dfrac{\dfrac{\,?\,}{\bot}}{\lnot Q(u)}}{\exists x \, \lnot Q(x)}\exists_i}{\exists x \, \lnot Q(x)}\exists_e^*
$$

So, I do know that if I extract $P(x)$ and $\neg P(x)$ it will result in a $\bot$, but that's about it. Any help is greatly appreciated!

Best Answer

The premises $\forall x (P(x) \land Q(x))$ and $\exists x \, \lnot P(x)$ are contradictory, so according to the principle of explosion (which corresponds to the rule $\bot_e$, a.k.a. ex falso quodlibet in natural deduction) from them you can derive everything, in particular $\exists x \, \lnot Q(x)$, as showed by the following derivation.

$$ \dfrac{\exists x \, \lnot P(x) \qquad \dfrac{\dfrac{[\lnot P(x)]^* \qquad \dfrac{\dfrac{\forall x (P(x) \land Q(x))}{P(x) \land Q(x)}\forall_e}{P(x)}\land_e}{\bot}\lnot_e}{\exists x \, \lnot Q(x)}\bot_e}{\exists x \, \lnot Q(x)}\exists_e^* $$

Note that there is no need for the rules RAA and $\lnot_i$.

Related Question