1
$\begingroup$

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!

$\endgroup$
0
3
$\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 :

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

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

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

enter image description here

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/

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.