Modus Tollendo Tollens/Proof Rule/Tableau Form

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

• 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): $\S 1.2$: Conditionals and Negation