fitch proof. P v Q Q→ ¬ R ¬ P ¬ R → ¬ S GOAL: ¬ S

Need help exercise using the FITCH program format. I'm stuck on where to start. The following 4 steps must be used to prove the goal.

P v Q
Q→ ¬ R
¬ P
¬ R → ¬ S

GOAL: ¬ S

Now I know: ¬ P and P v Q is true - hence, Q is true. Q is true and Q→ ¬ R is true. As true implies true statement, ¬ R is true. ¬ R → ¬ S is true. Since true never implies a false statement ¬ S is true. I just don't know where to start.

Now I know: ¬ P and P v Q is true - hence, Q is true. Q is true and Q→ ¬ R is true. As true implies true statement, ¬ R is true. ¬ R → ¬ S is true. Since true never implies a false statement ¬ S is true. I just don't know where to start.

That is basically it. The only question is whether you can use the rule of Disjunctive Syllogism, or need to build a proof by cases using fundamental rules of inference.

a.| ¬P
b.| P v Q
:
c.| Q       DS a, b        | Disjunctive Syllogism
:
:
d.|  |_ P   A              | Proof by Cases
e.|  |  #   ¬E d,a         |
f.|  |  Q   X  e           |
:                        |
g.|  |_ Q   A              |
:                        |
h.|  Q      vE b,d-f,g-g   |
• Below I added a photo of my current progress. May 14 '20 at 4:28
• No photo has been added. May 14 '20 at 4:58

You will need to use Disjunction Elimination (Proof by cases). As P v Q is one of your premises, assume P and derive a sentence, then assume Q and derive that same sentence; you are now allowed to discharge it. The only remaining step is using Implication Elimination to reach the goal.

1. |  P v Q
2. |  Q → ¬ R
3. |  ¬ P
4. |_ ¬ R → ¬ S
5. |  |_ P
6. |  |  ⊥          ⊥ Intro: 5,3
7. |  |  ¬ R        ⊥ Elim: 6
8. |  |_ Q
9. |  | ¬R          → Elim: 2,8
10.|  ¬R            v Elim: 1, 5-7,8-9
11.| ¬ S            → Elim: 4,10
• This makes sense, but I'm unsure if my edits above are correct. May 14 '20 at 1:49
• If you meant Negation Elimination (where you wrote INTRO), then that step is correct. I do not understand the step where you annotated elim (6). Can you clarify ? May 14 '20 at 2:17
• elim ⊥ is eliminate in reference to step 6 (the step before). And the reit is reiterating premise 2 May 14 '20 at 2:20
• In step 6, you are deriving P v Q, but that is one of your premises. Can you use Explosion rule ? Also, no need to reiterate premise 2, I think. Does your system require that step ? May 14 '20 at 2:32
• No, I can't use Explosion rule. Disjunction Elimination is certainly correct, but I'm not sure how to add it on Fitch May 14 '20 at 2:44