1. Where $\to$ is a conditional connective and $\neg$ is a negation connective, the axiom scheme:

• • $\neg \neg \phi \to \phi$

or the corresponding logical consequence. Notably, in intuitionistic logic, the principle fails; on the Brouwer-Heyting-Kolmogorov interpretation, that one may disprove that there is no disproof of $\phi$, this does not entail the existence of a constructive proof of $\phi$.

2. Where $\leftrightarrow$ is a biconditional connective, the scheme:

• • $\phi \leftrightarrow \neg \neg \phi$

or the logical equivalence of any two formulae $\phi$ and $\neg \neg \phi$ in a deductive system $\text{L}$.