双重否定翻译

负翻译不要求直觉主义逻辑接受经典结论本身，而是把经典断言改写成“反驳它会导致矛盾”的稳定形式。负翻译定理保证经典证明可以转化为这一负形式的证明，即使它没有提供析取的具体分支或存在命题的见证。

翻译后的公式落在一个对双重否定封闭的片段中。经典逻辑可以消去外加否定并看回原公式，直觉主义逻辑则保留它们，准确记录哪些步骤只排除了反例、没有构造正面证据。

可以把一个反证者理解成接受 $A$ 的证据并产出矛盾的过程，即 $A\to \mathrm{\perp }$。双重否定 $\mathrm{\neg }\mathrm{\neg }A$ 不直接交付 $A$，而是说明任何这样的反证者都会失败。负翻译沿公式结构安排这类“反证者接口”，使经典推导中的排中与反证步骤可以组合，并保留了负信息与具体构造性证据的区别。

带前提的翻译同时处理假设与结论：从 $\mathrm{\Gamma }$ 推导 $A$ 的每一步，都要转换成从 ${\mathrm{\Gamma }}^N$ 推导 $A^N$ 的合法步骤。逐规则的保持证明保证了这些步骤能够接续起来。

经典双重否定消去

不是 IPL 定理。按上述递归，$p^N=\mathrm{\neg }\mathrm{\neg }p$，$(\mathrm{\neg }p{)}^N=\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }p$，从而

后式可在 IPL 中直接证明。假设四重否定，目标是 $\neg \neg p$，于是暂时假设 $\neg p$。这个假设能推出 $\neg \neg \neg p$：任何 $\neg \neg p$ 都会与它矛盾。但四重否定又与 $\neg \neg \neg p$ 矛盾，因此可以撤销临时假设 $\neg p$，得到所需的 $\neg \neg p$。

命题版 Glivenko 定理使用更简短的整体包装：若经典命题逻辑证明 $A$，则 IPL 证明 $\mathrm{\neg }\mathrm{\neg }A$。这种包装直接加在整个公式外面；Gödel–Gentzen 翻译则沿联结词递归处理，便于逐步翻译证明，并可通过增加量词条款推广到一阶逻辑。Glivenko 的整体双重否定形式不能直接推广到任意一阶公式。

负翻译也不产生经典证明中缺失的算法见证。从经典证明得到 $\mathrm{\neg }\mathrm{\neg }(A\vee B)$，不能因此在 IPL 中选择 $A$ 或 $B$。若后续程序需要构造性分支，仍需加强源证明或另给可实现内容。

双重否定翻译给出经典逻辑相对于直觉主义逻辑的保守解释：经典推理可以在负片段中模拟，而 IPL 自己的构造性规则无需改变。它也解释某些经典定理为什么能得到“否定的否定”版本，却不能得到原结论。

证明论中，负翻译可与 cut 消去、Curry–Howard 和 continuation-passing style 联系：双重否定 $\mathrm{\neg }\mathrm{\neg }A$ 具有 continuation 类型 $(A\to \mathrm{\perp })\to \mathrm{\perp }$。这条对应揭示控制算子如何表达经典推理，但具体程序语义仍需选择求值策略和答案类型，不能从逻辑公式直接读出唯一实现。

Gödel 翻译理路Gödel 翻译Gödel translation · Gödel–McKinsey–Tarski translation给原子与蕴涵加上必然算子，把直觉主义命题逻辑忠实嵌入模态逻辑 S4。连接另一对逻辑系统：它把 IPL 嵌入正规模态逻辑 S4，用方框编码持久性；负翻译则把经典逻辑送入 IPL 的稳定片段。