Conditional disjunction equivalence proof using FItch

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.

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

1.   P v Q
_
|  2.   ¬Q --- assumed 
|  3.   P --- assumed  for v-Elim
|  4.   P --- from 3
|  5.   Q --- assumed  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  and 
|  9.   ¬Q → P --- from 2 and 8 by →-Intro, discharging 
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 
|  3.   Q --- assumed 
|  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 
|  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 
11.   (¬Q → P) → (P v Q) --- from 1 and 10 by →-Intro

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

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

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). 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/