2

Prove P v Q ⇔ ¬Q → P

So far I have the obvious things...

1.   P v Q
 _
|  2.   ¬Q
|  _
|  3.
|  4.
|  5.
|  6.
|  7.
|  8.   P
9.   ¬Q → P   → Intro 2-8

I think the problem here is that I do not understand how to apply disjunction elimination. What I tired to do is add another subproof to show that if Q it introduces a contradiction, but that does not help me further down the path.

I need some advice or nudge in the right direction.

5

(A) : For the left-to-tight direction we have :

1.   P v Q
 _
|  2.   ¬Q --- assumed [1]
|  3.   P --- assumed [2] for v-Elim
|  4.   P --- from 3
|  5.   Q --- assumed [3] for v-Elim
|  6.   ⊥ --- from 2 and 5 by →-Elim (recall that : ¬Q is abbrev for Q → ⊥)
|  7.   P --- from 6 by ⊥-Elim
|  8.   P --- from 3-4 an 5-7 with 1 by v-Elim, discharging [2] and [3]
|  9.   ¬Q → P --- from 2 and 8 by →-Intro, discharging [1]
10.   (P v Q) → (¬Q → P)   --- from 1 and 9 by →-Intro

(B) : For the right-to-left direction we have :

1.   ¬Q → P
 _
|  2.   ¬(P v Q) --- assumed [1]
|  3.   Q --- assumed [2]
|  4.   P v Q --- from 2 by v-Intro
|  5.   ⊥ --- from 2 and 4 by →-Elim (recall that : ¬A is abbrev for A → ⊥)
|  6.   ¬Q --- from 3 and 5 by →-Intro discharging [2]
|  7.   P --- from 6 and 1 by →-Elim
|  8.   P v Q --- from 7 by v-Intro
|  9.   ⊥ --- from 2 and 8 by →-Elim 
|  10.  P v Q --- from 2 and 9 by RAA (or Double Negation) discharging [1]
11.   (¬Q → P) → (P v Q) --- from 1 and 10 by →-Intro
2

To eliminate the disjunction, prove your conclusion (here P) for each terms of the disjunction in sub proofs. If the conclusion holds for each terms separately, then it holds for the disjunction of them too.

Alternatively, you can prove P by drawing a contradiction from not-P (then again you'll have to show that each term of the disjunction entails a contradiction, given not-P).

1

How much help do you want? This is a fairly short and direct proof, but if you need more explicit help than @quen_tin's (correct) answer, read below:

Your line 3 should be P v Q (from 1). Then you'll have to show that if you assume either side of the disjunction, you'll get the same result (P). The left side should be easy. For the right side, further assume not P and derive a contradiction (hint, the contradiction doesn't need to actually involve P).

0

I agree with the answer provided by Mauro ALLEGRANZA.

The following proof shows a different way to eliminate the disjunction, "P v Q", by using disjunctive syllogism (DS). See forall x: Calgary Remix, pp 124-5, for more information.

If you have that rule, it is similar to considering the two cases of the disjunction, case "P" and case "Q", and deriving "P" in both cases. However, because we need to assume "¬Q" to derive the desired implication, which you have done on your line 2, we can take a short-cut. That assumption means we don't have to check the "Q" case in the disjunction. It is contradictory. So we can derive "P" immediately which is what we want. Then we can discharge the assumption by introducing a conditional.

The other direction shows a way to proceed without using an indirect proof. It does use the law of the excluded middle (LEM).

enter image description here


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/

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.