2
$\begingroup$

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!

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

1 Answer 1

Reset to default
1
$\begingroup$

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

$\endgroup$
5
  • $\begingroup$ In our course material we haven't been introduced to falso quodlibet which seems odd if this is correct. $\endgroup$
    – Fredrik Andersson
    Aug 20, 2018 at 18:18
  • $\begingroup$ @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). $\endgroup$
    – Taroccoesbrocco
    Aug 20, 2018 at 18:26
  • $\begingroup$ 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$. $\endgroup$
    – Fredrik Andersson
    Aug 20, 2018 at 18:38
  • $\begingroup$ @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$. $\endgroup$
    – Taroccoesbrocco
    Aug 20, 2018 at 18:47
  • $\begingroup$ Interesting, thank you! $\endgroup$
    – Fredrik Andersson
    Aug 20, 2018 at 18:49

You must log in to answer this question.

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