$(P → Q) \lor (Q → R)$, Fitch-style proof

Question

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.

Answer 1

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/

Answer 2

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)}$$

using reductio ad absurdum and the introduction and elimination rules for conjunction, disjunction, and implication. I'm not allowed to use ex falso quodlibet.

Ex falso quodlibet is derived from reductio ad absurdum . If you can derive a contradiction, you can use reductio ad absurdum on the assumption of any negation.$$\fitch{\cdots}{~~\vdots\\A\\~~\vdots\\\neg A\\\bot\\\fitch{\neg B}{\bot}\\B}$$