Proof Disjunctive Syllogism using Natural Deduction
Andrew Mclaughlin 
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!
$\endgroup$ 02 Answers
$\begingroup$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 :
$\endgroup$ 2 $\begingroup$$¬p, p∨q, p \vdash q$.
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
$\endgroup$
