Modus Tollendo Tollens/Proof Rule/Tableau Form

From ProofWiki
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