Double Negation/Double Negation Elimination/Proof Rule/Tableau Form

From ProofWiki
Jump to navigation Jump to search

Proof Rule

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

Double Negation Elimination is invoked for $\neg \neg \phi$ as follows:

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