Modus Tollendo Ponens/Proof Rule/Tableau Form

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$