Modus Tollendo Ponens/Proof Rule/Tableau Form
Jump to navigation
Jump to search
Proof Rule
Let $\phi \lor \psi$ be a well-formed formula in a tableau proof whose main connective is the disjunction operator.
The Modus Tollendo Ponens is invoked for $\phi \lor \psi$ in either of the two forms:
- Form 1
Pool: | The pooled assumptions of $\phi \lor \psi$ | ||||||||
The pooled assumptions of $\neg \phi$ | |||||||||
Formula: | $\psi$ | ||||||||
Description: | Modus Tollendo Ponens | ||||||||
Depends on: | The line containing the instance of $\phi \lor \psi$ | ||||||||
The line containing the instance of $\neg \phi$ | |||||||||
Abbreviation: | $\text{MTP}_1$ |
- Form 2
Pool: | The pooled assumptions of $\phi \lor \psi$ | ||||||||
The pooled assumptions of $\neg \psi$ | |||||||||
Formula: | $\phi$ | ||||||||
Description: | Modus Tollendo Ponens | ||||||||
Depends on: | The line containing the instance of $\phi \lor \psi$ | ||||||||
The line containing the instance of $\neg \psi$ | |||||||||
Abbreviation: | $\text{MTP}_2$ |