Is this a valid propositional natural deduction proof? I'm new to logic and I tried to solve an exercise. Since there isn't a given answer, I'd appreciate an indication of whether this is correct
    Prove that p | q , !p |- q 

1   p|q         premise
2   !p          premise
-----------------------
3   !q          assumption
4   p|q         copy 1
    -------------------
5   p           assumption
6   FALSUM      !e 2,5
    -------------------
    -------------------
7   q           assumption
8   FALSUM      !e 3,8 
    -------------------
9   !(p|q)      !e 5-8
10  FALSUM      !e 1,9
-----------------------
11  q           !e 3-10

 A: The proof is not correct.
You have two premises: 1) and 2), and three temporary assumptions:

3) $\lnot q$
5) $p$
7) $q$;

in 9) you have derived $\lnot (p \lor q)$ by $\lnot$-intro, discharging 1).
The final step 11) derives $q$ by RAA (or Double Negation) from 3) and 10) and discharges 3).
In conclusion, the proof is:


$\lnot p, p, q \vdash q$.


A: I placed the attempted proof into a proof checker to see how far I could go before I ran into a problem, or until the proof completed successfully.  I was able to reach line 8.
Here is the original proof:

Here is how I was able to complete it after line 8 in the proof checker:

Observations:


*

*In the original proof the FALSUM on line 8 should reference lines 3 and 7, not lines 3 and 8.

*One line 9 instead of "!(p|q)" I have "⊥" or FALSUM. This is the result of disjunction elimination "vE" using lines 4, the "p" side on lines 5 and 6 and the "q" side on lines 7 and 8.

*That "⊥" on line 9 allowed me to claim that the assumption "Q" on line 3 is false and using indirect proof (IP) as a justification write "Q" which was the goal.



Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
