I am supposed to give a natural deduction proof of $$(P_1∨P_2), \neg P_1 ⊢ P_2$$ My assumption is $(P_1∨P_2)$ and I am going to derive $P_2$ from $\neg P_1$ or I am wrong?

EDIT: Or I am going to derive $(P_1∨P_2)$, and when i am deriving, am i suppose to derive $P_2$ from $\neg P_1$ ?

EDIT2: Have I done right?

EDIT3:The right discharge above the last line with "->-elimination" is wrong. I had intented to write $ [P_1]$. I mixed up the left one with the right one, since the left one can be written as the right one (i am talking about same line). For solution with "words", see below in answer.

enter image description here

  • 2
    $\begingroup$ Your assumptions are $P_1\lor P_2$ and $\neg P_1$.. $\endgroup$ – Git Gud Sep 17 '14 at 23:10
  • $\begingroup$ Could you give some tips to proof it? @GitGud $\endgroup$ – Kim Sep 17 '14 at 23:15
  • 2
    $\begingroup$ Are you following any particular text book? This is highly dependent on what deduction rules you have at your disposal. Can you post them? $\endgroup$ – Git Gud Sep 17 '14 at 23:19
  • $\begingroup$ Can I end the derivation by using VE (elimination rule for disjuntion) and above this line puting $P_1VP_2$ and derivations from ¬P to $P_2$ by using RAA? @GitGud $\endgroup$ – Kim Sep 17 '14 at 23:35
  • $\begingroup$ I mean putting $P_1\lor P_2$ and derivations from $P_1$, respectively $P_2$, to $P_2$. And in the derivation from $P_1$ to $P_2$ I can use ⊥E-rule ? @GitGud $\endgroup$ – Kim Sep 17 '14 at 23:46

You have to derive $P_2$ from assumptions $P_1 \lor P_2$ and $\lnot P_1$.

You have to use proof by cases, i.e. $\lor$-elimination.

1) $P_1 \lor P_2$ --- assumed

2) $\lnot P_1$ --- assumed

3) assuming $P_2$, trivially $P_2$ follows

4) $P_1$ --- assumed

5) $\bot$ --- from 2) and 4) by $\rightarrow$-elim [due to the fact that $\lnot \varphi$ is an abbreviation for : $\varphi \rightarrow \bot$]

6) $P_2$ --- from 5) by by $\bot$-elim [i.e. from $\bot$, infer $\varphi$]

7) having derived $P_2$ from both assumptions $P_1$ and $P_2$, due to assumption 1) we may conclude with $P_2$ by $\lor$-elimination, "discharging" assumptions 3) and 4) :

$(P_1 \lor P_2),\lnot P_1 \vdash P_2$.

  • $\begingroup$ What about my derive in three structure that I posted ? The first discharge $ [\lnot P_1]$ are wrong, I had intended to write $ [P_1]$ $\endgroup$ – Kim Sep 18 '14 at 6:36
  • $\begingroup$ @Kim - With this correction it's right; it's exactly what I've done ... :) $\endgroup$ – Mauro ALLEGRANZA Sep 18 '14 at 6:51
  • $\begingroup$ Great :D i appreciate your time you took to help me :) $\endgroup$ – Kim Sep 18 '14 at 6:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.