[proofplan] We first prove two structural lemmas inside intuitionistic logic: translation commutes with capture-free substitution, and every translated formula $A^N$ is stable, meaning $\vdash_{\mathrm{IL}} \neg\neg A^N \to A^N$. We then induct on a fixed classical natural-deduction derivation, translating each open assumption $B$ into $B^N$. All intuitionistic rules are simulated directly except the negative clauses for $\lor$ and $\exists$, whose eliminations use stability of the translated conclusion; the added classical double-negation-elimination rule is handled exactly by the stability lemma. [/proofplan]

[step:Record substitution compatibility for the translation] We use the following structural fact. If $B \in \operatorname{Form}(\mathcal{L})$, $x$ is a variable, and $t$ is a term free for $x$ in $B$, then \begin{align*} (B[t/x])^N = B^N[t/x]. \end{align*} This is proved by structural induction on $B$. The atomic and $\bot$ cases follow from the definition of $N$. The clauses for $\land$, $\lor$, and $\to$ follow by applying the induction hypotheses to the immediate subformulas. For quantifiers, one first alpha-renames bound variables if necessary so that the substitution is capture-free; after this standard renaming, the clauses $(\forall y\,C)^N = \forall y\,C^N$ and $(\exists y\,C)^N = \neg\forall y\,\neg C^N$ reduce the assertion to the induction hypothesis for $C$. This proves the compatibility identity. [/step]

[step:Prove intuitionistic stability for every translated formula]We prove by structural induction on $A$ that \begin{align*} \vdash_{\mathrm{IL}} \neg\neg A^N \to A^N. \end{align*} If $A$ is atomic, then $A^N = \neg\neg A$. Given $h : \neg\neg\neg\neg A$ and $k : \neg A$, define $r : \neg\neg A \to \bot$ by $r(m) := m(k)$. Then $h(r) : \bot$, so $k \mapsto h(r)$ proves $\neg\neg A$. If $A = \bot$, then $A^N = \bot$. Given $h : \neg\neg\bot$, the map $b \mapsto b$ is a proof of $\neg\bot$, hence $h(b \mapsto b) : \bot$. If $A = B \land C$, assume $h : \neg\neg(B^N \land C^N)$. To prove $B^N$, the induction hypothesis for $B$ reduces the task to $\neg\neg B^N$. Given $u : \neg B^N$, define $v : \neg(B^N \land C^N)$ by $v(p) := u(\pi_1(p))$, where $\pi_1$ is conjunction elimination. Then $h(v) : \bot$, so $\neg\neg B^N$, hence $B^N$. The second component is obtained in the same way using the second projection and the induction hypothesis for $C$. Thus $B^N \land C^N$. If $A = B \to C$, assume $h : \neg\neg(B^N \to C^N)$ and let $b : B^N$. By the induction hypothesis for $C$, it suffices to prove $\neg\neg C^N$. Given $u : \neg C^N$, define $v : \neg(B^N \to C^N)$ by $v(f) := u(f(b))$. Then $h(v) : \bot$, hence $C^N$. Therefore $B^N \to C^N$. If $A = B \lor C$, then $A^N = \neg(\neg B^N \land \neg C^N)$. Given $h : \neg\neg\neg(\neg B^N \land \neg C^N)$ and $p : \neg B^N \land \neg C^N$, define $q : \neg\neg(\neg B^N \land \neg C^N)$ by $q(r) := r(p)$. Then $h(q) : \bot$, proving $\neg(\neg B^N \land \neg C^N)$. If $A = \forall x\,B$, assume $h : \neg\neg\forall x\,B^N$. Let $y$ be fresh for the undischarged assumptions. By the induction hypothesis for $B[y/x]$, it suffices to prove $\neg\neg B^N[y/x]$. Given $u : \neg B^N[y/x]$, define $v : \neg\forall x\,B^N$ by $v(g) := u(g(y))$. Then $h(v) : \bot$, hence $B^N[y/x]$, and universal introduction gives $\forall x\,B^N$. If $A = \exists x\,B$, then $A^N = \neg\forall x\,\neg B^N$. Given $h : \neg\neg\neg\forall x\,\neg B^N$ and $p : \forall x\,\neg B^N$, define $q : \neg\neg\forall x\,\neg B^N$ by $q(r) := r(p)$. Then $h(q) : \bot$, proving $\neg\forall x\,\neg B^N$.[/step]

[guided]The reason for proving stability first is that the translation deliberately turns the classically problematic connectives into negative formulas. We prove, entirely in intuitionistic logic, that every formula produced by the translation satisfies double-negation elimination. For an atomic formula $P$, the translation is $P^N = \neg\neg P$. Thus stability says $\neg\neg\neg\neg P \to \neg\neg P$. Assume $h : \neg\neg\neg\neg P$. To prove $\neg\neg P$, assume $k : \neg P$. From $k$ define $r : \neg\neg P \to \bot$ by $r(m) := m(k)$ for each $m : \neg\neg P$. Since $h$ refutes every refutation of $\neg\neg P$, $h(r) : \bot$. Therefore $k \mapsto h(r)$ is a proof of $\neg\neg P$. For $\bot$, stability is $\neg\neg\bot \to \bot$. If $h : \neg\neg\bot$, then the identity map $b \mapsto b$ has type $\bot \to \bot$, which is $\neg\bot$. Applying $h$ to this map gives $\bot$. For conjunction, suppose $h : \neg\neg(B^N \land C^N)$. We need both components. To obtain $B^N$, the induction hypothesis for $B$ says that it is enough to construct $\neg\neg B^N$. So assume $u : \neg B^N$. Any pair $p : B^N \land C^N$ has first projection $\pi_1(p) : B^N$, and $u(\pi_1(p)) : \bot$. Hence $p \mapsto u(\pi_1(p))$ refutes $B^N \land C^N$, contradicting $h$. This proves $\neg\neg B^N$, hence $B^N$. The second component is identical with the second projection and the induction hypothesis for $C$, giving $C^N$. Conjunction introduction gives $B^N \land C^N$. For implication, suppose $h : \neg\neg(B^N \to C^N)$ and fix $b : B^N$. We must produce $C^N$. The induction hypothesis for $C$ reduces this to $\neg\neg C^N$. Assume $u : \neg C^N$. Every function $f : B^N \to C^N$ produces $f(b) : C^N$, and $u(f(b)) : \bot$. Thus $f \mapsto u(f(b))$ is a refutation of $B^N \to C^N$, contradicting $h$. Therefore $\neg\neg C^N$, and stability of $C^N$ gives $C^N$. For disjunction, the translated formula is not $B^N \lor C^N$ but $\neg(\neg B^N \land \neg C^N)$. Assume $h : \neg\neg\neg(\neg B^N \land \neg C^N)$ and assume $p : \neg B^N \land \neg C^N$. From $p$ define $q : \neg\neg(\neg B^N \land \neg C^N)$ by $q(r) := r(p)$. Then $h(q) : \bot$. Since this derives $\bot$ from arbitrary $p$, we have $\neg(\neg B^N \land \neg C^N)$. For the universal quantifier, suppose $h : \neg\neg\forall x\,B^N$. Let $y$ be a fresh variable satisfying the eigenvariable condition. We prove $B^N[y/x]$ and then introduce $\forall x$. By the induction hypothesis for $B[y/x]$, it is enough to prove $\neg\neg B^N[y/x]$. If $u : \neg B^N[y/x]$, then every $g : \forall x\,B^N$ gives $g(y) : B^N[y/x]$, so $u(g(y)) : \bot$. Thus $g \mapsto u(g(y))$ refutes $\forall x\,B^N$, contradicting $h$. Hence $B^N[y/x]$, and universal introduction gives $\forall x\,B^N$. For the existential quantifier, the translated formula is $\neg\forall x\,\neg B^N$. Assume $h : \neg\neg\neg\forall x\,\neg B^N$ and $p : \forall x\,\neg B^N$. Define $q : \neg\neg\forall x\,\neg B^N$ by $q(r) := r(p)$. Then $h(q) : \bot$. Since $p$ was arbitrary, this proves $\neg\forall x\,\neg B^N$.[/guided]

[step:Translate assumptions and manage open contexts] Let $\mathcal{D}$ be a classical derivation of $\Gamma \vdash_{\mathrm{CL}} A$. More generally, for every subderivation of $\mathcal{D}$ with open assumptions contained in a finite set $\Delta \subseteq \Gamma \cup \Sigma$, where $\Sigma$ consists of the temporary assumptions introduced by natural-deduction introduction or elimination rules, we prove that the translated conclusion is derivable from the translated open assumptions. At each rule application, if a premise is derived from a smaller translated context, intuitionistic weakening embeds it into the larger translated context needed for the rule. Exchange and contraction are harmless because contexts are treated as finite multisets, and assumption discharge is preserved by replacing the discharged formula $B$ with $B^N$. If the last line of a subderivation is an undischarged assumption $B$, then the translated last line is $B^N$, which is one of the open translated assumptions. This proves the base case of the induction on the height of $\mathcal{D}$. [/step]

[step:Translate conjunction and implication rules componentwise] Conjunction introduction, conjunction elimination, implication introduction, and implication elimination are translated by the corresponding intuitionistic rules. For example, from translated premises deriving $B^N$ and $C^N$ in a common translated context, conjunction introduction derives $B^N \land C^N = (B \land C)^N$. If a derivation of $C$ under an auxiliary assumption $B$ is translated as $\Delta^N, B^N \vdash_{\mathrm{IL}} C^N$, implication introduction gives $\Delta^N \vdash_{\mathrm{IL}} B^N \to C^N = (B \to C)^N$. Implication elimination is ordinary modus ponens applied to translated derivations of $B^N \to C^N$ and $B^N$. [/step]

[step:Translate disjunction rules through the negative disjunction clause]For left disjunction introduction, suppose the induction hypothesis gives a derivation of $B^N$ from a translated context $\Delta^N$. To derive $(B \lor C)^N = \neg(\neg B^N \land \neg C^N)$, assume $p : \neg B^N \land \neg C^N$. The first projection gives $\pi_1(p) : \neg B^N$, and applying it to the derived $B^N$ gives $\bot$. This discharges $p$ and proves the translated disjunction. The right introduction case uses the second projection. For disjunction elimination, suppose the last classical rule has premises deriving $B \lor C$, deriving $D$ from auxiliary assumption $B$, and deriving $D$ from auxiliary assumption $C$. After translating premises and weakening to a common context $\Delta^N$, we have \begin{align*} \Delta^N \vdash_{\mathrm{IL}} \neg(\neg B^N \land \neg C^N), \end{align*} \begin{align*} \Delta^N, B^N \vdash_{\mathrm{IL}} D^N, \end{align*} and \begin{align*} \Delta^N, C^N \vdash_{\mathrm{IL}} D^N. \end{align*} By stability of $D^N$, it suffices to derive $\neg\neg D^N$. Assume $k : \neg D^N$. Define $u : \neg B^N$ by sending $b : B^N$ to $k(d_B(b))$, where $d_B(b)$ denotes the result of the translated left branch applied under the temporary assumption $b$. Define $v : \neg C^N$ by $v(c) := k(d_C(c))$ using the translated right branch. Then $u \land v$ has type $\neg B^N \land \neg C^N$, contradicting the translated proof of $B \lor C$. Hence $\neg\neg D^N$, and stability gives $D^N$.[/step]

[guided]The introduction rules for disjunction are easy because the translated disjunction is a refutation of the possibility that both disjuncts are false. If we have $B^N$ and assume $p : \neg B^N \land \neg C^N$, then the first component of $p$ refutes $B^N$. This contradiction proves $\neg(\neg B^N \land \neg C^N)$. The right introduction rule is the same argument with $C^N$ and the second projection. The elimination rule is the delicate part. In classical natural deduction, from $B \lor C$, a derivation of $D$ from $B$, and a derivation of $D$ from $C$, one concludes $D$. After translation we do not have $B^N \lor C^N$; we have \begin{align*} \neg(\neg B^N \land \neg C^N). \end{align*} Thus we prove $D^N$ indirectly, using the stability already established for translated formulas. By stability, it is enough to prove $\neg\neg D^N$. Assume $k : \neg D^N$. The translated left branch turns any temporary proof $b : B^N$ into a proof $d_B(b) : D^N$. Composing with $k$ gives $k(d_B(b)) : \bot$, so $b \mapsto k(d_B(b))$ is a proof $u : \neg B^N$. Similarly, the translated right branch gives $v : \neg C^N$ by $v(c) := k(d_C(c))$. Therefore $u \land v$ proves $\neg B^N \land \neg C^N$. This contradicts the translated disjunction premise, which refutes such a pair. Hence $k$ leads to $\bot$, so $\neg\neg D^N$. Applying stability of $D^N$ gives the required conclusion $D^N$.[/guided]

[step:Translate universal quantifier rules with substitution compatibility] For universal introduction, suppose the original rule derives $\forall x\,B$ from a derivation of $B$, with $x$ not free in any undischarged assumption on which the conclusion depends. Translation preserves free variables, so $x$ is not free in the translated open assumptions. The induction hypothesis gives $B^N$, and intuitionistic universal introduction gives $\forall x\,B^N = (\forall x\,B)^N$. For universal elimination, suppose the original rule derives $B[t/x]$ from $\forall x\,B$, with $t$ free for $x$ in $B$. The induction hypothesis gives $\forall x\,B^N$. Intuitionistic universal elimination gives $B^N[t/x]$, and substitution compatibility gives $B^N[t/x] = (B[t/x])^N$. [/step]

[step:Translate existential rules through the negative existential clause]For existential introduction, suppose the original rule derives $\exists x\,B$ from $B[t/x]$, where $t$ is free for $x$ in $B$. The induction hypothesis and substitution compatibility give $B^N[t/x]$. To prove $(\exists x\,B)^N = \neg\forall x\,\neg B^N$, assume $q : \forall x\,\neg B^N$. Universal elimination gives $q(t) : \neg B^N[t/x]$, contradicting the derived proof of $B^N[t/x]$. Therefore $\neg\forall x\,\neg B^N$. For existential elimination, suppose the original rule uses a derivation of $\exists x\,B$ and a derivation of $D$ from the auxiliary assumption $B[y/x]$, where $y$ is fresh for $D$ and for every undischarged assumption except the discharged auxiliary assumption. Since translation preserves free variables, $y$ is fresh for $D^N$ and for the translated undischarged assumptions. After translation, we have \begin{align*} \Delta^N \vdash_{\mathrm{IL}} \neg\forall x\,\neg B^N \end{align*} and \begin{align*} \Delta^N, B^N[y/x] \vdash_{\mathrm{IL}} D^N. \end{align*} By stability of $D^N$, it suffices to prove $\neg\neg D^N$. Assume $k : \neg D^N$. To construct $\forall x\,\neg B^N$, let $y$ be fresh also for the temporary assumption $k$. Given $b : B^N[y/x]$, the translated auxiliary derivation gives $d_y(b) : D^N$, and $k(d_y(b)) : \bot$. Thus $b \mapsto k(d_y(b))$ proves $\neg B^N[y/x]$. Universal introduction, justified by the stated freshness of $y$, gives $\forall x\,\neg B^N$, contradicting the translated existential premise. Hence $\neg\neg D^N$, and stability gives $D^N$.[/step]

[guided]Existential introduction works because the negative translation of $\exists x\,B$ says that not every instance of $B^N$ is impossible. If we already have an instance $B^N[t/x]$, then any assumed $q : \forall x\,\neg B^N$ gives $q(t) : \neg B^N[t/x]$, contradicting that instance. Therefore $q$ is impossible, which is exactly $\neg\forall x\,\neg B^N$. Existential elimination requires more bookkeeping. The original rule has an auxiliary variable $y$ and an auxiliary assumption $B[y/x]$. Its eigenvariable condition says that $y$ is fresh for the conclusion $D$ and for all undischarged assumptions except $B[y/x]$. Because the translation does not introduce new free variables, the same freshness condition holds for $D^N$ and the translated assumptions. After translating, the existential premise gives \begin{align*} \neg\forall x\,\neg B^N. \end{align*} The translated auxiliary derivation says that from a temporary proof $b : B^N[y/x]$ we can derive $d_y(b) : D^N$. Since the translated existential premise is negative, we again use stability of the desired conclusion. It is enough to prove $\neg\neg D^N$. Assume $k : \neg D^N$. We build a contradiction to the translated existential premise by proving $\forall x\,\neg B^N$. Let $y$ be fresh not only for the translated open assumptions and $D^N$, but also for the temporary assumption $k : \neg D^N$. Given $b : B^N[y/x]$, the auxiliary derivation gives $d_y(b) : D^N$, and applying $k$ gives $\bot$. Hence $b \mapsto k(d_y(b))$ proves $\neg B^N[y/x]$. Since $y$ satisfies the eigenvariable condition, universal introduction gives $\forall x\,\neg B^N$. This contradicts $\neg\forall x\,\neg B^N$. Therefore $\neg\neg D^N$, and stability yields $D^N$.[/guided]

[step:Translate absurdity and the classical double-negation-elimination rule] Absurdity elimination is preserved because $\bot^N = \bot$. If the original rule derives $B$ from $\bot$, the induction hypothesis gives $\bot$, and intuitionistic absurdity elimination gives $B^N$. It remains to translate the only rule of $\mathrm{CL}$ not already in $\mathrm{IL}$. Suppose the last rule derives $B$ from $\neg\neg B$. The induction hypothesis applied to the premise gives \begin{align*} \Delta^N \vdash_{\mathrm{IL}} (\neg\neg B)^N. \end{align*} Since $\neg\neg B$ abbreviates $(B \to \bot) \to \bot$, the definition of $N$ gives \begin{align*} (\neg\neg B)^N = (B^N \to \bot) \to \bot = \neg\neg B^N. \end{align*} The stability lemma gives $\vdash_{\mathrm{IL}} \neg\neg B^N \to B^N$, so intuitionistic implication elimination yields $\Delta^N \vdash_{\mathrm{IL}} B^N$. [/step]

[step:Conclude the induction on the classical derivation] The preceding cases cover every possible last rule of the classical natural-deduction derivation: assumptions, structural rules, intuitionistic logical rules, and the added double-negation-elimination rule. Therefore the induction on derivation height proves that every classical derivation of $\Gamma \vdash_{\mathrm{CL}} A$ translates into an intuitionistic derivation of $\Gamma^N \vdash_{\mathrm{IL}} A^N$. This is the asserted Gödel-Gentzen negative translation theorem. [/step]