Modus Ponendo Tollens/Proof Rule
Proof Rule
Modus ponendo tollens is a valid argument in types of logic dealing with conjunctions $\land$ 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 $\map \neg {\phi \land \psi}$, and we can also conclude $\phi$, then we may infer $\neg \psi$.
- $(2): \quad$ If we can conclude $\map \neg {\phi \land \psi}$, and we can also conclude $\psi$, then we may infer $\neg \phi$.
It can be written:
- $\ds {\map \neg {\phi \land \psi} \quad \phi \over \neg \psi} \textrm{MPT}_1 \qquad \text{or} \qquad {\map \neg {\phi \land \psi} \quad \psi \over \neg \phi} \textrm{MPT}_2$
Tableau Form
Let $\phi \land \psi$ be a well-formed formula in a tableau proof whose main connective is the conjunction operator.
The Modus Ponendo Tollens is invoked for $\neg \left({\phi \land \psi}\right)$ in either of the two forms:
- Form 1
Pool: | The pooled assumptions of $\neg \left({\phi \land \psi}\right)$ | ||||||||
The pooled assumptions of $\phi$ | |||||||||
Formula: | $\neg \psi$ | ||||||||
Description: | Modus Ponendo Tollens | ||||||||
Depends on: | The line containing the instance of $\neg \left({\phi \land \psi}\right)$ | ||||||||
The line containing the instance of $\phi$ | |||||||||
Abbreviation: | $\text{MPT}_1$ |
- Form 2
Pool: | The pooled assumptions of $\neg \left({\phi \land \psi}\right)$ | ||||||||
The pooled assumptions of $\psi$ | |||||||||
Formula: | $\neg \phi$ | ||||||||
Description: | Modus Ponendo Tollens | ||||||||
Depends on: | The line containing the instance of $\neg \left({\phi \land \psi}\right)$ | ||||||||
The line containing the instance of $\psi$ | |||||||||
Abbreviation: | $\text{MPT}_2$ |
Explanation
The Modus Tollendo Ponens can be expressed in natural language as:
If two statements cannot both be true, and one of them is true, it follows that the other one is not true.
Also see
- This is a rule of inference of the following proof systems:
Linguistic Note
Modus Ponendo Tollens is Latin for mode that by affirming, denies.
Technical Note
When invoking Modus Ponendo Tollens in a tableau proof, use the {{ModusPonendoTollens}}
template:
{{ModusPonendoTollens|line|pool|statement|first|second|1 or 2}}
or:
{{ModusPonendoTollens|line|pool|statement|first|second|1 or 2|comment}}
where:
line
is the number of the line on the tableau proof where Modus Ponendo 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 $\neg \left({\phi \land \psi}\right)$second
is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $\phi$ or $\psi$1 or 2
should hold 1 forModusPonendoTollens_1
, and 2 forModusPonendoTollens_2
comment
is the (optional) comment that is to be displayed in the Notes column.