ThmDex – An index of mathematical definitions, results, and conjectures.
Principle of double-negation is a propositional tautology
Formulation 0
Let $\phi \in \text{Proposition}$ be a D2966: Propositional expression.
Then \begin{equation} \models \neg \neg \phi \leftrightarrow \phi \end{equation}
Formulation 1
Let $\phi \in \text{Proposition}$ be a D2966: Propositional expression.
Then \begin{equation} \neg \neg \phi \quad \iff \quad \phi \end{equation}