Disjunction of Implications

From ProofWiki
Jump to navigation Jump to search

Theorem

$\vdash \left({p \implies q}\right) \lor \left({q \implies r}\right)$


Proof

By the tableau method of natural deduction:

$\vdash \left({p \implies q}\right) \lor \left({q \implies r}\right)$
Line Pool Formula Rule Depends upon Notes
1 $q \lor \neg q$ Law of Excluded Middle (None)
2 2 $q$ Assumption (None)
3 2 $p \implies q$ Sequent Introduction 2 True Statement is implied by Every Statement
4 2 $\left({p \implies q}\right) \lor \left({q \implies r}\right)$ Rule of Addition: $\lor \mathcal I_1$ 3
5 5 $\neg q$ Assumption (None)
6 5 $q \implies r$ Sequent Introduction 5 False Statement implies Every Statement
7 5 $\left({p \implies q}\right) \lor \left({q \implies r}\right)$ Rule of Addition: $\lor \mathcal I_2$ 6
8 $\left({p \implies q}\right) \lor \left({q \implies r}\right)$ Proof by Cases: $\text{PBC}$ 1, 2 – 4, 5 – 7 Assumptions 2 and 5 have been discharged

$\blacksquare$


Sources