= Solution
Use the <Gödel-Gentzen negative translation>, writing $A^N$ for the translated <first-order formula>. On <atomic formulas> $P$, including <logical equality>, put $P^N=\neg\neg P$, and put $\bot^N=\bot$. Extend recursively by
$$
\begin{aligned}
(A\land B)^N&=A^N\land B^N,&(A\to B)^N&=A^N\to B^N,\\
(\forall x\,A)^N&=\forall x\,A^N,&(A\lor B)^N&=\neg\neg(A^N\lor B^N),\\
(\exists x\,A)^N&=\neg\neg\exists x\,A^N.&
\end{aligned}
$$
<Logical negation> abbreviates <logical implication> to <logical falsity>, so $(\neg A)^N=\neg A^N$. The displayed <logical disjunction> and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg(\neg A^N\land\neg B^N)$ and $\neg\forall x\,\neg A^N$, respectively. Thus these clauses specify the same <negative interpretation>. Translation commutes with <capture-avoiding substitution> of terms for <free variables>.
First prove by <structural induction> the <stability of a formula under double negation>:
$$
\mathrm{IL}\vdash\neg\neg A^N\to A^N.
$$
Every double <logical negation> is stable, since <intuitionistic first-order logic> proves $\neg\neg\neg\neg C\to\neg\neg C$; <logical falsity> is stable as well. Stability passes to <logical conjunction> by obtaining double <logical negation> of each component. For a <logical implication> $C\to D$ with stable $D$, assume $\neg\neg(C\to D)$ and $C$. An assumption $\neg D$ would give $\neg(C\to D)$, a contradiction, so $\neg\neg D$ and then $D$. For a universal <first-order formula>, $\neg\neg\forall x\,C(x)$ implies $\neg\neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. <Logical disjunction> and existential translations are already double negations. This proves all cases.
Now regard classical first-order <natural deduction> as intuitionistic <natural deduction> plus unrestricted <double-negation elimination>, and induct on a classical derivation. The rules for <logical conjunction>, <logical implication>, <universal quantification> and <logical falsity> translate directly. <Logical disjunction> introduction gives $A^N\lor B^N$ and then its double <logical negation>. For <logical disjunction> elimination, the translated premise is $\neg\neg(A^N\lor B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg(A^N\lor B^N)$, which contradicts the premise. We have $\neg\neg C^N$ and remove it by stability.
Existential introduction likewise adds a double <logical negation> to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)\vdash C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\,\neg A^N(y)$ and therefore $\neg\exists y\,A^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new <free variables>.
For <logical equality>, reflexivity gives $t=t$ and then its double <logical negation>. For substitution, from $\neg\neg(s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic <logical equality> substitution, so it gives a contradiction and hence $\neg(s=t)$. The first premise contradicts this. Thus $\neg\neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical <double-negation elimination> step translates precisely to $\neg\neg A^N\to A^N$, already proved. Every rule is therefore covered, giving <negative translation of a classical proof>:
$$
\boxed{\Gamma\vdash_{\mathrm{CL}}\varphi\quad\Longrightarrow\quad\Gamma^N\vdash_{\mathrm{IL}}\varphi^N.}
$$
In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.
In classical logic, <double-negation elimination> gives $P^N\leftrightarrow P$ on atoms. <Structural induction> propagates equivalence through <logical conjunction>, <logical implication> and both quantifiers, and removes the added double negations on <logical disjunction> and existence. Therefore
$$
\boxed{\mathrm{CL}\vdash\varphi^N\leftrightarrow\varphi,\qquad\mathrm{CL}\vdash\varphi\ \Longrightarrow\ \mathrm{IL}\vdash\varphi^N.}
$$
Back to article page
