Modus Tollendo Ponens/Proof Rule
Proof Rule
Modus tollendo ponens is a valid argument in types of logic dealing with disjunctions $\lor$ and negation $\neg$.
This includes propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in either of the two forms:
- $(1): \quad$ If we can conclude $\phi \lor \psi$, and we can also conclude $\neg \phi$, then we may infer $\psi$.
- $(2): \quad$ If we can conclude $\phi \lor \psi$, and we can also conclude $\neg \psi$, then we may infer $\phi$.
It can be written:
- $\ds {\paren {\phi \lor \psi} \quad \neg \phi \over \psi} \textrm {MTP}_1 \qquad \text{or} \qquad {\paren {\phi \lor \psi} \quad \neg \psi \over \phi} \textrm {MTP}_2$
Tableau Form
Let $\phi \lor \psi$ be a well-formed formula in a tableau proof whose main connective is the disjunction operator.
The Modus Tollendo Ponens is invoked for $\phi \lor \psi$ in either of the two forms:
- Form 1
Pool: | The pooled assumptions of $\phi \lor \psi$ | ||||||||
The pooled assumptions of $\neg \phi$ | |||||||||
Formula: | $\psi$ | ||||||||
Description: | Modus Tollendo Ponens | ||||||||
Depends on: | The line containing the instance of $\phi \lor \psi$ | ||||||||
The line containing the instance of $\neg \phi$ | |||||||||
Abbreviation: | $\text{MTP}_1$ |
- Form 2
Pool: | The pooled assumptions of $\phi \lor \psi$ | ||||||||
The pooled assumptions of $\neg \psi$ | |||||||||
Formula: | $\phi$ | ||||||||
Description: | Modus Tollendo Ponens | ||||||||
Depends on: | The line containing the instance of $\phi \lor \psi$ | ||||||||
The line containing the instance of $\neg \psi$ | |||||||||
Abbreviation: | $\text{MTP}_2$ |
Explanation
The Modus Tollendo Ponens can be expressed in natural language as:
If either of two statements is true, and one of them is not to be true, it follows that the other one is true.
- Once you eliminate the impossible, whatever remains, no matter how improbable, must be the truth.
- -- Sherlock Holmes (Sir Arthur Conan Doyle, 1890: The Sign of the Four, ch. 6)
Also known as
The Modus Tollendo Ponens is also known as the Disjunctive Syllogism, abbreviated D.S.
Also see
- This is a rule of inference of the following proof systems:
Linguistic Note
Modus Tollendo Ponens is Latin for mode that by denying, affirms.
Technical Note
When invoking Modus Tollendo Ponens in a tableau proof, use the {{ModusTollendoPonens}}
template:
{{ModusTollendoPonens|line|pool|statement|first|second|1 or 2}}
or:
{{ModusTollendoPonens|line|pool|statement|first|second|1 or 2|comment}}
where:
line
is the number of the line on the tableau proof where Modus Tollendo Ponens is to be invokedpool
is the pool of assumptions (comma-separated list)statement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimitersfirst
is the first of the two lines of the tableau proof upon which this line directly depends, the one in the form $p \lor q$second
is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $\neg p$1 or 2
should hold 1 forModusTollendoPonens_1
, and 2 forModusTollendoPonens_2
comment
is the (optional) comment that is to be displayed in the Notes column.
Sources
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$