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.