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:

1. $$\lnot p$$
2. $$p \lor q$$
3. p assumption
4. $$\bot$$ from 1&3
5. q from 4

Is it ok 100% ? What can I do to make it perfect ? Thanks!

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

• So if I go like this: ... 6. q assumption 7. q from 5&6 is ok ? Aug 29 '19 at 8:54
• @RazvanStatescu - correct. Aug 29 '19 at 9:01

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/