# Disjunctions in Derivations

Disjunctions in derivations are, as the current inference rules stand, difficult to deal with. Using an already derived disjunction by applying Disjunction Elimination (DE) is not too bad, but there is an easier to use alternative. Deriving a disjunction in the first place is more difficult. Our Disjunction Introduction (DI) rule turns out to be a rather anemic tool for this task. In this module, we introduce derived rules which provide alternative methods for dealing with disjunctions in derivations.

## Using already derived disjunctions
### Modus Tollendo Ponens

We start with a new (to be) derived rule of inference. This will provide a useful alternative to Disjunction Elimination (DE).
    Modus Tollendo Ponens, Form I (MTP)
       $(\varphi \lor \psi )\,\!$
       ${\underline {\lnot \varphi \quad \quad }}\,\!$
       $\psi \,\!$
    Modus Tollendo Ponens, Form II (MTP)
       $(\varphi \lor \psi )\,\!$
       ${\underline {\lnot \psi \quad \quad }}\,\!$
       $\varphi \,\!$
Modus Tollendo Ponens is sometimes known as Disjunctive Syllogism and occasionally as the Rule of the Dog.

### Supporting theorems

This new rule requires the following two supporting theorems.
    $\mathbf {T16.} \quad (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$
| 1. | $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \,\!$ | Assumption $[(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!$ |
| 2. | $\mathrm {P} \lor \mathrm {Q} \,\!$ | 1 KE |
| 3. | $\lnot \mathrm {P} \,\!$ | 1 KE |
| 4. | $\mathrm {P} \rightarrow \mathrm {Q} \,\!$ | 3 CAdd |
| 5. | $\mathrm {Q} \rightarrow \mathrm {Q} \,\!$ | T1 [P/Q] |
| 6. | $\mathrm {Q} \,\!$ | 2, 4, 5 DE |
| 7. | $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$ | 1–6 CI |
    $\mathbf {T17.} \quad (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} \,\!$
| 1. | $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \,\!$ | Assumption $[(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} ]\,\!$ |
| 2. | $\mathrm {P} \lor \mathrm {Q} \,\!$ | 1 KE |
| 3. | $\lnot \mathrm {Q} \,\!$ | 1 KE |
| 4. | $\mathrm {Q} \rightarrow \mathrm {P} \,\!$ | 3 CAdd |
| 5. | $\mathrm {P} \rightarrow \mathrm {P} \,\!$ | T1 |
| 6. | $\mathrm {P} \,\!$ | 2, 4, 5 DE |
| 7. | $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} \,\!$ | 1–6 CI |

### Example derivation

For an example using MTP, we redo the example derivation from Constructing a Complex Derivation.
    $\mathrm {P} \land \mathrm {R} \rightarrow \mathrm {T} ,\ \ \mathrm {S} \land \lnot \mathrm {T} ,\ \ \mathrm {S} \rightarrow \lnot \mathrm {Q} \,\!$ ∴ $\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} \,\!$
| 1. | $\mathrm {P} \land \mathrm {R} \rightarrow \mathrm {T} \,\!$ | Premise |
| 2. | $\mathrm {S} \land \lnot \mathrm {T} \,\!$ | Premise |
| 3. | $\mathrm {S} \rightarrow \lnot \mathrm {Q} \,\!$ | Premise |
| 4. | $\mathrm {P} \lor \mathrm {Q} \,\!$ | Assumption $[\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!$ |
| 5. | $\mathrm {R} \,\!$ | Assumption $[\lnot \mathrm {R} ]\,\!$ |
| 6. | $\mathrm {S} \,\!$ | 2 KE |
| 7. | $\lnot \mathrm {Q} \,\!$ | 3, 6 CE |
| 8. | $\mathrm {P} \,\!$ | 4, 7 MTP |
| 9. | $\mathrm {P} \land \mathrm {R} \,\!$ | 5, 8 KI |
| 10. | $\mathrm {T} \,\!$ | 1, 9 CE |
| 11. | $\lnot \mathrm {T} \,\!$ | 2 KE |
| 12. | $\lnot \mathrm {R} \,\!$ | 5–11 NI |
| 13. | $\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} \,\!$ | 4–12 CI |
After Line 4, we did not bother with subderivations for deriving the antecedent lines needed for DE. Instead, we went straight to a subderivation for the conclusion's consequent. At line 8, we applied MTP.

## Deriving disjunctions
### Conditional Disjunction

The next derived rule significantly reduces the labor of deriving disjunctions, thus providing a useful alternative to Disjunction Introduction (DI).
    Conditional Disjunction (CDJ)
       ${\underline {(\lnot \varphi \rightarrow \psi )}}\,\!$
       $(\varphi \lor \psi )\,\!$

### Supporting theorem

    $\mathbf {T18.} \quad (\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} \,\!$
| 1. | $\lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$ | Assumption $[(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} ]\,\!$ |
| 2. | $\lnot (\mathrm {P} \lor \mathrm {Q} )\,\!$ | Assumption $[\mathrm {P} \lor \mathrm {Q} ]\,\!$ |
| 3. | $\mathrm {P} \,\!$ | Assumption $[\lnot \mathrm {P} ]\,\!$ |
| 4. | $\mathrm {P} \lor \mathrm {Q} \,\!$ | 3 DI |
| 5. | $\lnot (\mathrm {P} \lor \mathrm {Q} )\,\!$ | 2 R |
| 6. | $\lnot \mathrm {P} \,\!$ | 3–5 NI |
| 7. | $\mathrm {Q} \,\!$ | 1, 6 CE |
| 8. | $\mathrm {P} \lor \mathrm {Q} \,\!$ | 7 DI |
| 9. | $\mathrm {P} \lor \mathrm {Q} \,\!$ | 2–8 NI |
| 10. | $(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} \,\!$ | 1–9 CI |

### Example derivation

This derivation will make use of T12 (introduced at Derived Inference Rules) even though its proof was left to the reader as an exercise. The correctness the following derivation, particularly Line 2, assumes that you have indeed proved T12.
    ∴ $(\mathrm {P} \rightarrow \mathrm {Q} )\lor (\mathrm {Q} \rightarrow \mathrm {R} )\,\!$
| 1. | $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\,\!$ | Assumption $[\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )]\,\!$ |
| 2. | $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \land \lnot \mathrm {Q} \,\!$ | T12 |
| 3. | $\mathrm {P} \land \lnot \mathrm {Q} \,\!$ | 1, 2 CE |
| 4. | $\lnot \mathrm {Q} \,\!$ | 3 KE |
| 5. | $\mathrm {Q} \rightarrow \mathrm {R} \,\!$ | 4 CAdd |
| 7. | $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )\,\!$ | 1–6 CI |
| 8. | $(\mathrm {P} \rightarrow \mathrm {Q} )\lor (\mathrm {Q} \rightarrow \mathrm {R} )\,\!$ | 7 CDJ |
Here we attempted to derive the desired conditional by first deriving the antecedent line needed for CDJ.