# P <=> (Q v R), P, -Q⊢R Propositional Logic Question

<=> is bi-conditional, "-" is negation, "v" is disjunction.

I can't figure out where to take it from line 4. Negated Q is throwing me for a loop.

P <=> (Q v R), P, -Q ⊢ R

1. P <=> (Q v R) P
2. P P
3. -Q P/R
4. QvR 1,2<=>E (biconditional elimination rule removing P)
• Not sure why you edited it back. All I did was format it. Oct 28 '16 at 0:59
• The period denotes it in a different contextual basis, but it disappears if it's not there, which is odd. Oct 28 '16 at 1:00
• Not sure what you mean by "different contextual basis" per se but the SE markdown syntax is pretty picky. If you really want to avoid the . in a list, then you can use the preformatted syntax. Oct 28 '16 at 1:01

Given 3 and 4, the normal move is disjunctive syllogism which enables:

1. A v B
2. ~A
3. Therefore B

This would yield:

1. R DS 3,4

If you don't have access to disjunctive syllogism, then it's going to be a lot harder to do.

• I do not have access to disjunctive syllogism yet, that's in our next unit. Oct 28 '16 at 1:03
• do you have access to conditional proofs or reduction ad absurdum? Oct 28 '16 at 1:06
• We only have access to Conjunction Introduction & Elimination, Conditional Introduction & Elimination, Reiteration, Negation Introduction & Elimination, Disjunction Introduction & Elimination and Biconditional Introduction & Elimination. Oct 28 '16 at 1:08
• conditional introduction is a synonym for conditional proof (faculty.washington.edu/smcohen/120/Chapter8.pdf) Oct 28 '16 at 1:14
• I take it we're using a wide array of synonym's in this course because things are named slightly different when I research them. But yeah. Oct 28 '16 at 1:16

Usually when there's a disjunction you're going to have to use the disjunction elimination rule. So when you see it you have to think how that rule can get you to the conclusion.

In this case, we would need the following:

``````1. Q v R
2. Q → R
3. R → R
``````

Using disjunction elimination, these would get you to `R`. You already have 1, and 3 is trivial. So we need to figure out how to get 2. This can be done in the following tricky way:

``````1. ~Q
2. | Q
3. | | ~R
4. | | ~Q
5. | | Q
6. | | Q & ~Q
7. | ~~R
8. | R
9. Q → R
``````

Now you have all 3 statements needed for the disjunction elimination rule which will get you to `R`.

• Assuming he's allowed to do step 7, but it's not entirely clear. Oct 28 '16 at 7:57

I agree with virmaior's answer using disjunctive syllogism (DS). Here is how Kevin Klement's proof checker would format the proof using disjunctive syllogism:

Disjunctive syllogism is derived from disjunction elimination (vE). Here is a proof using the disjunction elimination illustrating the derivation for disjunctive syllogism from disjunction elimination given in forall x: Calgary Remix (page 137):

Note how this uses conjunction introduction of "R" with itself on line 9 and then conjunction elimination on line 10 to get "R" again. The rules of this proof checker eliminates the need for those steps.

Here is a third version of the proof:

The OP has the same first four lines and states: "I can't figure out where to take it from line 4." The above shows three ways to proceed and there may be more depending on the proof checker one uses.

References

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/