Modus Ponendo Tollens/Proof Rule/Tableau Form
Jump to navigation
Jump to search
Tableau Form of Modus Ponendo Tollens
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$ |