## Formalized Name Goedel-Gentzen Negative Translation Soundness ## Formalized Statement Fix a first-order language $\mathcal{L}$ with $\bot$, and write $\neg A$ for $A\to\bot$. Let classical logic $\mathrm{CL}$ be the natural-deduction system obtained from intuitionistic first-order logic $\mathrm{IL}$ by adding the double-negation-elimination rule. Define the Goedel-Gentzen negative translation recursively by $P^N:=\neg\neg P$ for atomic $P$, $\bot^N:=\bot$, $(A\land B)^N:=A^N\land B^N$, $(A\to B)^N:=A^N\to B^N$, $(A\lor B)^N:=\neg(\neg A^N\land\neg B^N)$, $(\forall x\,A)^N:=\forall x\,A^N$, and $(\exists x\,A)^N:=\neg\forall x\,\neg A^N$. If $\Gamma\vdash_{\mathrm{CL}} A$, then $\Gamma^N\vdash_{\mathrm{IL}} A^N$, where $\Gamma^N=\{B^N:B\in\Gamma\}$. ## Proof [proofplan] Prove the result by induction on the given classical natural-deduction derivation. First record two elementary intuitionistic facts about the translation: every translated formula is stable, and the translation validates the classical double-negation-elimination rule. Then check that each intuitionistic inference rule is preserved by the recursive clauses of the translation. [/proofplan] [step:Translated formulas are stable] For every formula $B$, intuitionistic logic proves \begin{align*} \neg\neg B^N\to B^N. \end{align*} This is a structural induction on $B$. Atomic formulas are translated as $\neg\neg P$, and intuitionistic logic proves $\neg\neg\neg\neg P\to\neg\neg P$. The clauses for $\land$, $\to$, and $\forall$ are stable by the same closure arguments used for strictly negative formulas. The translated disjunction $\neg(\neg A^N\land\neg B^N)$ and the translated existential $\neg\forall x\,\neg A^N$ are negations, hence stable because any formula of the form $\neg C$ is stable intuitionistically. [/step] [step:The classical rule is translated into an intuitionistic derivation] It remains to check the extra classical rule. Suppose a classical derivation ends by double-negation elimination, deriving $B$ from $\neg\neg B$. By the induction hypothesis applied to the premise, intuitionistic logic derives \begin{align*} (\neg\neg B)^N. \end{align*} The translation of $\neg\neg B$ is intuitionistically equivalent to $\neg\neg B^N$, since negation is implication into $\bot$ and implication is translated homomorphically. By stability of $B^N$, intuitionistic logic derives $B^N$. Therefore the translated conclusion is derivable in $\mathrm{IL}$. [/step] [step:Assumptions and intuitionistic rules are preserved] If the classical derivation uses an assumption $B\in\Gamma$, then $B^N$ is an assumption in $\Gamma^N$. The introduction and elimination rules for $\land$, $\to$, and $\forall$ translate directly because the translation commutes with those connectives. Weakening, contraction, exchange, and substitution are unchanged by the translation, since they operate on derivations rather than on the internal shape of formulas. [/step] [step:Disjunction and existential rules are preserved] For disjunction introduction, a derivation of $A^N$ gives $\neg(\neg A^N\land\neg B^N)$ by sending a pair of refutations to the contradiction obtained from its first component; the other introduction is symmetric. For disjunction elimination, assume $\neg(\neg A^N\land\neg B^N)$ and translated derivations of $C^N$ from $A^N$ and from $B^N$. To prove $C^N$, use stability of $C^N$ and prove $\neg\neg C^N$: a refutation of $C^N$ turns the two translated branch derivations into refutations of $A^N$ and $B^N$, contradicting the translated disjunction. For existential introduction, a witness $t$ and a derivation of $A(t)^N$ yield $\neg\forall x\,\neg A^N$ by specializing a hypothetical universal refutation at $t$. For existential elimination, assume $\neg\forall x\,\neg A^N$ and a translated derivation of $C^N$ from $A^N$ with the usual eigenvariable condition. Again use stability of $C^N$: a refutation of $C^N$ would turn the branch derivation into a proof of $\neg A^N$ uniformly in the eigenvariable, hence into $\forall x\,\neg A^N$, contradicting the translated existential. [/step] [step:Conclude by induction on the derivation] The previous steps cover every possible last rule in the classical derivation: assumptions, all intuitionistic first-order rules, and the added double-negation-elimination rule. Induction on the derivation therefore transforms a derivation of $A$ from $\Gamma$ in $\mathrm{CL}$ into a derivation of $A^N$ from $\Gamma^N$ in $\mathrm{IL}$. [/step] [step:Summarize the translation argument] The proof checks that each rule in the classical derivation has an intuitionistic derivation after translation. The induction on derivations then gives the translated conclusion from the translated assumptions in every case. [guided] The proof checks that each rule in the classical derivation has an intuitionistic derivation after translation. The induction on derivations then gives the translated conclusion from the translated assumptions in every case. [/guided] [/step]