# In fitch, S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R)

Construct a proof for the argument: S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R) I have gotten to the point in the illustration, but I am unable to figure out where to go from here. I get tricked up on the format of this Fitch exercise, but I am able to reason through it.

Another approach is to assume ~(Q ∨ R) as I did on line 9 below. This leads to a contradiction on line 17 so that you can complete the the other half of the disjunction.

```1   |   (S→(R ∨ P))        Premise
2   |_  (P→(~R→Q))         Premise
3   | |_  S                Assumption
4   | |   (R ∨ P)          1,3  →E
5   | | |_  R              Assumption
6   | | |   (Q ∨ R)        5  ∨I
7   | | |_  P              Assumption
8   | | |   (~R→Q)         2,7  →E
9   | | | |_  ~(Q ∨ R)     Assumption
10  | | | | |_  ~R         Assumption
11  | | | | |   Q          8,10  →E
12  | | | | |   (Q ∨ R)    11  ∨I
13  | | | | |   ⊥          9,12  ⊥I
14  | | | |   ~~R          10-13  ~I
15  | | | |   R            14  ~E
16  | | | |   (Q ∨ R)      15  ∨I
17  | | | |   ⊥            9,16  ⊥I
18  | | |   ~~(Q ∨ R)      9-17  ~I
19  | | |   (Q ∨ R)        18  ~E
20  | |   (Q ∨ R)          4,5-6,7-19  ∨E
21  |   (S→(Q ∨ R))        3-20  →I
```

Hint

Assume S and derive R ∨ P from 1st premise.

Now two sub-proofs, for -elim:

1) Assume R and derive Q ∨ R by -intro, and it is done.

2) Assume P and derive ¬R → Q from 2nd premise.

Now use R ∨ ¬R (Excluded Middle) for a new -elim:

2.1) Assume R and derive Q ∨ R.

2.2) Assume ¬R and derive Q from ¬R → Q and then derive Q ∨ R.

Having derived Q ∨ R in each case, we can conclude with:

S → (Q ∨ R)

by -intro.

Like Pe I did a proof by contradiction ... and by making the assumption of ~(Q v R) earlier in the proof (and exploiting Fitch's shortcut of allowing ~ Intro to be used while getting rid of the negation of the assumption), I was able to shave off a few lines: What to me is really interesting about this proof is that the subproof starting with R is used twice: as a proof by contradiction to infer ~R, as well as a proof by cases to get the contradiction. You don't see that kind of thing too often.

The following is one way to prove this. The first two lines contain the premises.

Since the goal is a conditional, I assumed the antecedent, "S", in a subproof starting on line 3. My goal was to reach the consequent, "Q v R", which I did on line 13. This allowed me to discharge the assumption and close the subproof by introducing a conditional to complete the proof.

To get to line 13, I assumed the negation of that consequent I wanted to prove by starting a new subproof. I aimed to reach a contradiction which I did in line 12. Using the disjunctive syllogism (DS) on line 8 allowed me to cut short testing the two cases of the disjunction on line 6.

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/