Modus Tollendo Tollens/Proof Rule/Tableau Form
Jump to navigation
Jump to search
Proof Rule
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}$ |
Sources
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): $\S 1.2$: Conditionals and Negation