= Gödel-Gentzen negative translation
{c}
{title2=$\varphi^N$}
= Negative interpretation
{synonym}
= Negative translation
{synonym}
For an <atomic formula> $P$ (including <logical equality>), put $P^N=\neg\neg P$, and put $\bot^N=\bot$. Preserve <logical conjunction>, <logical implication> and <universal quantification> recursively, while setting
$$
(A\lor B)^N=\neg\neg(A^N\lor B^N),\qquad (\exists x\,A)^N=\neg\neg\exists x\,A^N.
$$
<Logical negation> is <logical implication> to <logical falsity>, so $(\neg A)^N=\neg A^N$. The displayed <logical disjunction> and existence clauses are intuitionistically equivalent to the usual negative forms $\neg(\neg A^N\land\neg B^N)$ and $\neg\forall x\,\neg A^N$. Every translated <first-order formula> is stable by <stability of a formula under double negation>. In classical logic the translation is equivalent to the original <first-order formula> by <mathematical induction> and <double-negation elimination>.
Back to article page
