= Negative translation of a classical proof
{title2=$\Gamma\vdash_{\mathrm{CL}}A\Rightarrow\Gamma^N\vdash_{\mathrm{IL}}A^N$}
The <Gödel-Gentzen negative translation> transforms $\Gamma\vdash_{\mathrm{CL}}A$ into $\Gamma^N\vdash_{\mathrm{IL}}A^N$. Induct on a <natural deduction> derivation. The translated <logical conjunction>, <logical implication> and universal rules are ordinary intuitionistic rules. <Logical disjunction> and existential introduction add double <logical negation>; their elimination rules first derive the double <logical negation> of the stable translated conclusion, then use its stability. Classical <double-negation elimination> translates precisely to stability. If <logical equality> atoms are double-negated, transport a stable translated conclusion through a <logical equality> by contradiction and then remove the resulting double <logical negation>. Original nonlogical axioms must also be translated; the result does not say arbitrary untranslated classical <first-order theories> are intuitionistically valid.
Back to article page
