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

Here is a proof using a Fitch-style proof checker. 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/