双重否定翻译

负翻译不要求直觉主义逻辑接受经典结论本身，而是把经典断言改写成“反驳它会导致矛盾”的稳定形式。经典证明给出的排除能力通常足以建立这一负信息，即使它没有提供析取的具体分支或存在命题的见证。

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

可以把一个反证者理解成接受 $A$ 的证据并产出矛盾的过程，即 $A\to \mathrm{\perp }$。双重否定 $\mathrm{\neg }\mathrm{\neg }A$ 不直接交付 $A$，而是说明任何这样的反证者都会失败。负翻译沿公式结构安排这类“反证者接口”，使经典推导中的排中与反证步骤可以组合，同时不假装已经获得析取分支或存在见证。

因此翻译作用于整份推导，而不只是改写最终显示的公式。前提也要一同翻译，每条推理规则都要证明在目标系统中仍可模拟；只有这样，嵌入结论才会在证明复用时保持。单看经典真值等价，无法替代这项逐规则的保持证明。

经典双重否定消去

不是 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$，与四重否定矛盾。翻译没有偷偷使用双重否定消去，而是把结论改成自身稳定的双重否定形式。

命题版 Glivenko 定理使用更简短的整体包装：若经典逻辑无前提证明 $A$，则 IPL 证明 $\mathrm{\neg }\mathrm{\neg }A$。它不等于上述逐联结词翻译；加入前提、推广到一阶量词或要求证明组合时，直接只在结论外包两层否定通常不够，必须说明采用哪种负翻译及如何处理前提和存在量词。

负翻译也不产生经典证明中缺失的算法见证。从经典证明得到 $\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 的稳定片段。两者的源、目标和新增符号都不同，不能因为都与 Gödel 名字相关而混称同一翻译。