Double Negation/Double Negation Introduction/Proof Rule/Tableau Form

Proof Rule

Let $\phi$ be a well-formed formula in a tableau proof.

Double Negation Introduction is invoked for $\phi$ as follows:

			Pool:					The pooled assumptions of $\phi$
			Formula:					$\neg \neg \phi$
			Description:					Double Negation Introduction
			Depends on:					The line containing the instance of $\phi$
			Abbreviation:					$\text{DNI}$ or $\neg \neg \II$