Proof Disjunctive Syllogism using Natural Deduction So, how can I have to prove this using natural deduction:
$\lnot p, p \lor q \vdash q$
What I did is:


*

*$\lnot p$

*$p \lor q$

*p assumption

*$\bot$ from 1&3

*q from 4


Is it ok 100% ? What can I do to make it perfect ?
Thanks!
 A: No, it is not.
You have a disjunction as 2nd premise : thus you have to consider both disjuncts with $(\lor \text E)$.
The first sub-case, with $p$ as assumption, is Ok.
You have to add the second sub-case, with $q$ as assumption, in which case the conclusion $q$ is immediate.
Then, having derived $q$ in both cases, you can use $(\lor \text E)$ and conclude.

The flaw in your derivation is that you have the undischarged assumption 3. Thus, what your derivation amounts to is really :

$¬p, p∨q, p \vdash q$.

A: It helps to use a proof checker to make sure one uses the rules correctly. Here is a proof:

The first five lines are the same as your proof. However, they only considered the left side, $P$, of the disjunction on line 2. You have to also consider the right side, $Q$. Note how that was done in this proof checker simply by stating the assumption on line 6. Line 6 was also the derivation of the goal. 
The justification for line 7 was given as "∨E 2, 3–5, 6–6". That can be understood as using disjunction elimination (∨E) on the disjunction on line 2 noted as "2" in the justification. One side of the disjunction started with an assumption on line 3 and derived the goal, $Q$, on line 5. That subproof was noted as "3-5". The other side of the disjunction started with an assumption on line 6 and since it already was what I wanted to derive I ended the subproof on line 6 as well. This was noted as "6-6".

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
A: Proof without ⊥ elimination (or any derived rules).
Sorry for necroposting, but here's a way of solving the proof without the use of a contradiction elimination I couldn't find online.

Lines 9 and 10 could be combined into one line if instead of introducing the negation on line 9, we eliminated it, but some proof checkers, such as this one don't seem to support eliminations of this specific form.
