Modus Tollendo Ponens/Proof Rule/Tableau Form

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