Natural deduction proof - I don't' understand the question

Question

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.

Answer 1

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