Modus Tollendo Tollens/Proof Rule
Contents
Proof Rule
The Modus Tollendo Tollens is a valid deduction sequent in propositional logic.
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:
- $\displaystyle {\phi \implies \psi \quad \neg \psi \over \neg \phi} \text{MTT}$
Tableau Form
Let $\phi \implies \psi$ be a propositional 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
- Denying the consequent.
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): $\S 1.2$: Conditionals and Negation
- 1973: Irving M. Copi: Symbolic Logic (4th ed.) ... (previous) ... (next): $3.1$: Formal Proof of Validity
- 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