Modus Tollendo Tollens/Proof Rule
Proof Rule
Modus tollendo tollens is a valid argument in types of logic dealing with conditionals $\implies$ and negation $\neg$.
This includes propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in the form:
- If we can conclude $\phi \implies \psi$, and we can also conclude $\neg \psi$, then we may infer $\neg \phi$.
It can be written:
- $\ds {\phi \implies \psi \quad \neg \psi \over \neg \phi} \text{MTT}$
Tableau Form
Let $\phi \implies \psi$ be a well-formed formula in a tableau proof whose main connective is the implication operator.
The Modus Tollendo Tollens is invoked for $\phi \implies \psi$ and $\neg \psi$ as follows:
Pool: | The pooled assumptions of $\phi \implies \psi$ | ||||||||
The pooled assumptions of $\neg \psi$ | |||||||||
Formula: | $\neg \phi$ | ||||||||
Description: | Modus Tollendo Tollens | ||||||||
Depends on: | The line containing the instance of $\phi \implies \psi$ | ||||||||
The line containing the instance of $\neg \psi$ | |||||||||
Abbreviation: | $\text{MTT}$ |
Explanation
The Modus Tollendo Tollens can be expressed in natural language as:
- If the truth of one statement implies the truth of a second, and the second is shown not to be true, then neither can the first be true.
Also known as
Modus Tollendo Tollens is also known as:
- Modus tollens, abbreviated M.T.
- Denying the consequent.
Also see
- This is a rule of inference of the following proof systems:
Linguistic Note
Modus Tollendo Tollens is Latin for mode that by denying, denies.
The shorter form Modus Tollens means mode that denies.
Technical Note
When invoking Modus Tollendo Tollens in a tableau proof, use the {{ModusTollens}}
template:
{{ModusTollens|line|pool|statement|first|second}}
or:
{{ModusTollens|line|pool|statement|first|second|comment}}
where:
line
is the number of the line on the tableau proof where Modus Tollendo Tollens 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 $\phi \implies \psi$second
is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $\phi$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{I}$: 'NOT' and 'IF': $\S 3$
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
- 1980: D.J. O'Connor and Betty Powell: Elementary Logic ... (previous) ... (next): $\S \text{II}$: The Logic of Statements $(2): \ 1$: Decision procedures and proofs: $2$
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.1$: Rules for natural deduction