Modus Tollendo Ponens
Contents |
Theorem
The modus tollendo ponens is a valid deduction sequent in propositional logic:
- $p \lor q \dashv \vdash \neg p \implies q$
This is also known as the disjunctive syllogism.
That is:
- If either of two statements is true, and one of them is known not to be true, it follows that the other one is true.
It can be written:
- $\displaystyle {\left({p \lor q}\right) \quad \neg p \over q} \textrm{MTP} \qquad \text{or} \qquad {\left({p \lor q}\right) \quad \neg q \over p} \textrm{MTP}$
Its abbreviation in a tableau proof is $\textrm{MTP}$.
Alternative Renditions
It can alternatively be rendered as:
- $\vdash \left({p \lor q}\right) \iff \left({\neg p \implies q}\right)$
This can be seen to be logically equivalent to the form above.
It is also seen in the format:
- $p \lor q, \neg p \vdash q$
which follows from the above by Modus Ponendo Ponens.
Proof
Proof by Natural Deduction
By the tableau method:
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| 1 | 1 | $p \lor q$ | P | (None) | ||
| 2 | 2 | $p$ | A | (None) | We pick the first of the disjuncts ... | |
| 3 | 3 | $\neg p$ | A | (None) | Assume the negation of it ... | |
| 4 | 2, 3 | $\bot$ | $\neg \mathcal E$ | 2, 3 | ... which of course is a direct contradiction ... | |
| 5 | 2, 3 | $\,\!q$ | $\bot \mathcal E$ | 4 | ... and having derived a falsehood, we can derive any statement - we pick $q$ ... | |
| 6 | 2 | $\neg p \implies q$ | $\implies \mathcal I$ | 3-5 | ... so assuming $\neg p$ implies $q$. | |
| 7 | 7 | $q$ | A | (None) | Then we pick the second of the disjuncts ... | |
| 8 | 8 | $\neg p$ | A | (None) | ... again we assume the negation of $p$ ... | |
| 9 | 7 | $q$ | Law of Identity | 7 | We still have the truth of $q$... | |
| 10 | 7 | $\neg p \implies q$ | $\implies \mathcal I$ | 8, 9 | ... thus from assuming $\neg p$ we can derive $q$. | |
| 11 | 1 | $\neg p \implies q$ | $\lor \mathcal E$ | 1, 2-6, 7-10 | Either of our disjuncts lead to the conclusion, so the proof is demonstrated. |
$\blacksquare$
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| 1 | 1 | $\neg p \implies q$ | P | (None) | ||
| 2 | $p \lor \neg p$ | LEM | (None) | Either $p$ is true or it's not. | ||
| 3 | 3 | $\,\!p$ | A | (None) | Suppose it is ... | |
| 4 | 3 | $p \lor q$ | $\lor \mathcal I_1$ | 3 | ||
| 5 | 5 | $\neg p$ | A | (None) | ... or suppose it's not ... | |
| 6 | 1, 5 | $\,\!q$ | $\implies \mathcal E$ | 1, 5 | ||
| 7 | 1, 5 | $p \lor q$ | $\lor \mathcal I_2$ | 6 | ||
| 8 | 1 | $p \lor q$ | $\lor \mathcal E$ | 2, 3-4, 5-7 | ... both options lead to the conclusion. |
$\blacksquare$
Note that the latter proof requires the Law of Excluded Middle.
Proof by Truth Table
As can be seen by inspection, the truth values under the main connectives match for all models.
$\begin{array}{|ccc||cccc|} \hline p & \lor & q & \neg & p & \implies & q \\ \hline F & F & F & T & F & F & F \\ F & T & T & T & F & T & T \\ T & T & F & F & T & T & F \\ T & T & T & F & T & T & T \\ \hline \end{array}$
$\blacksquare$
Also see
The following are related argument forms:
Linguistic Note
Modus tollendo ponens is Latin for mode that by denying, affirms.
Sources
- Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 3$
- Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 5$: Theorem $\text{T45}$
- E.J. Lemmon: Beginning Logic (1965): $\S 1.5$: Exercises $1 \ \text{(j)}$
- D.J. O'Connor and Betty Powell: Elementary Logic (1980): $\S 1.13$: Exercise $\text{(A)} \ 5$
- Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2.1$: Exercise $1.5: \ 2 \ \text{(c)}$
