# Natural deduction in first-order logic

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!

• Can you add the deduction system you are using? – blub Aug 20 '18 at 15:56
• GrahamKemp here is the task: imgur.com/a/5qlW3iN – Fredrik Andersson Aug 20 '18 at 16:01
• Well isn't that just lovely... Thanks for pointing that out. – Fredrik Andersson Aug 20 '18 at 16:04
• @GrahamKemp - I disagree with you. Please, see my answer and in case tell me where I'm wrong. – Taroccoesbrocco Aug 20 '18 at 18:10
• Hmmm... yes....indeed. Appologies. @FredrikAndersson , Taroccoesbrocco is correct. – Graham Kemp Aug 20 '18 at 23:00

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$.
• @FredrikAndersson - Ex falso quodlibet ($\bot_e$) is just a special case of RAA, where you do not discharge anything. In the rule RAA you can discharge an arbitrary finite number ($0$ or $1$ or $2$ or ...) of formula occurrences, the $\bot_e$ is just the special case of RAA where in particular you discharge $0$ formula occurrences. If you accept RAA, you must accept $\bot_e$ (and call it RAA if you prefer). – Taroccoesbrocco Aug 20 '18 at 18:26
• So what I did initially would be on the right track? I just did one unnecessary step where I could have included $\exists$ as well right after $\bot$. – Fredrik Andersson Aug 20 '18 at 18:38
• @FredrikAndersson - Yes, it is, but in your attempt you should also complete the part with "$?$". Note that your unnecessary step under $\bot$ is not wrong, just unnecessary. In other words, you can complete your attempt by putting together my derivation above $\bot$ and your derivation below $\bot$. – Taroccoesbrocco Aug 20 '18 at 18:47