# (P → Q) v (Q → R), Fitch-style proof

I'm trying to construct a Fitch-style proof for $(P \to Q) \lor (Q \to R)$ using reductio ad absurdum and the introduction and elimination rules for conjunction, disjunction, and implication. I'm not allowed to use ex falso quodlibet.

I've started by assuming the negation $\lnot((P \to Q) \lor (Q \to R))$ and got to $\lnot(P \to Q)$ and $\lnot(Q \to R)$, but have no idea what to do anymore.

This is all that I've got:

 1. ¬((P → Q) v (Q → R))                        [Assumption]
2. P → Q                                       [Assumption]
3. (P → Q) V (Q → R)                           [2, V introduction]
4. ((P → Q) v (Q → R)) & ¬((P → Q) v (Q → R))  [1,3, & I]
5. ¬(P → Q)                                    [2-4, - I]
6. Q → R                                       [Assumption]
7. (P → Q) v (Q → R)                           [6, V I]
8. ((P → Q) v (Q → R)) & ¬((P → Q) v (Q → R))  [1,7, & I]
9. ¬(Q → R)                                    [6-8, - I]


I've tried to proceed by assuming $Q$ and then $P$, but didn't manage to get anything that allowed to negate the initial assumption.

• Do you mean $(P \to Q) \vee (Q \to P)$? – Joe Johnson 126 Sep 19 '18 at 1:14
• Unfortunately not. I noticed that had been previously answered at least twice. – Humanist Sep 19 '18 at 1:21
• This is all that I've got: 1. - ((P → Q) v (Q → R)) [Assumption] 2. P → Q [Assumption] 3. (P → Q) V (Q → R) [2, V introduction] 4. ((P → Q) v (Q → R)) & - ((P → Q) v (Q → R)) [1,3, & I] 5. - (P → Q) [2-4, - I] 6. Q → R [Assumption] 7. (P → Q) v (Q → R) [6, V I] 8. ((P → Q) v (Q → R)) & - ((P → Q) v (Q → R)) [1,7, & I] 9. - (Q → R) [6-8, - I] I've tried to proceed by assuming Q and then P, but didn't manage to get anything that allowed to negate the initial assumption. (And I regrettably also couldn't figure out how to format the comment to be readable..) – Humanist Sep 19 '18 at 1:59
• Don't squish it into the comments. Edit your original post. – Graham Kemp Sep 19 '18 at 2:09
• Hint: Don't assume the implications, derive them. – Graham Kemp Sep 19 '18 at 2:34

Hint: Assume $\neg((P\to Q)\lor(Q\to R))$ aiming to derive a contradiction. To do that assume $Q$ aiming to derive $R$.

I've tried to proceed by assuming Q and then P, but didn't manage to get anything that allowed to negate the initial assumption.

You will, try again. $$\def\fitch#1#2{~~\begin{array}{|l} #1 \\ \hline #2\end{array}}\fitch{}{\fitch{\neg((P\to Q)\lor(Q\to R))}{\fitch{Q}{\fitch{P}{\vdots}\\\vdots\\\bot\\R}\\Q\to R\\(P\to Q)\lor(Q\to R)\\\bot}\\\neg\neg((P\to Q)\lor(Q\to R))\\(P\to Q)\vee(Q\to R)}$$

The OP desires to prove the following without using ex falso quodlibet, that is, explosion, but using reductio ad absurdum, that is, indirect proof (IP), as well as "introduction and elimination rules for conjunction, disjunction, and implication".

∴ (P → Q) ∨ (Q → R)

Here is one attempt that does not use ex falso quodlibet, but does use indirect proof with contradiction introduction (that is, reductio ad absurdum). However, the above proof also uses De Morgan rules (DeM), modus tollens (MT), and double negative elimination DNE).

Derivations of two of the De Morgan rules are provided in section 19.6 of forallx. The authors derive modus tollens in section 19.3. They discuss double negative elimination in section 16.4. Consult this text to see if the use of these rules are acceptable.

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/