Any one of a family of translations from the language of classical logic (propositional or first-order) into itself by inserting instances of a double negation ($\neg \neg$). One of the most well-known is the Glivenko translation named for mathematician Valery Glivenko (1897–1940), which maps a propositional formula $\phi$ to the formula $\neg \neg \phi$, i.e., ${\phi }^{\tau }=\neg \neg \phi$. This translation features in Glivenko’s theorem that relates classical propositional logic with intuitionistic propositional logic. where ${\Gamma }^{\tau }$ denotes the set comprising the Glivenko translation of each formula in $\Gamma$, Glivenko’s theorem states:

• • $\Gamma {\models }_{\text{CL}}\phi$ if and only if ${\Gamma }^{\tau }{\models }_{\text{Int}}{\phi }^{\tau }$

for all sets of propositional formulae $\Gamma \cup \left\{\phi \right\}$ where ${\models }_{\text{CL}}$ and ${\models }_{\text{Int}}$ represent classical and intuitionistic validity, respectively. The most well-known of the first-order translations is the Gödel-Gentzen negative translation, named for logicians Kurt Gödel (1906–1978) and Gerhard Gentzen (1909–1945) that appends double negations to atomic formulae, disjunctions, and existentially quantified formulae.