Gödel 翻译 | Codeboy's Blog

形式陈述

Gödel 翻译把直觉主义命题逻辑公式 $A$ 递归映为模态公式 $A^G$ ：

\begin{aligned} p^G&=\square p, & \bot^G&=\bot,\\ (A\land B)^G&=A^G\land B^G, & (A\lor B)^G&=A^G\lor B^G,\\ (A\to B)^G&=\square(A^G\to B^G). \end{aligned}

目标 S4 是正规模态逻辑：它在K 上加入

\mathbf T:\square A\to A, \qquad \mathbf4:\square A\to\square\square A,

分别对应 Kripke 关系的自反性与传递性。Gödel–McKinsey–Tarski 定理断言

\vdash_{\mathrm{IPL}}A \quad\Longleftrightarrow\quad \vdash_{\mathrm{S4}}A^G.

带前提时，先把每个假设 $B\in\Gamma$ 一并翻译为 $B^G$ ，再按所采用的局部或全局模态后承解释推导。下文使用上述递归条款。

直觉

直觉主义真理一旦在信息状态中建立，就应在所有更强状态保持。S4 的方框沿自反传递关系查看整个未来锥：给原子加 $□$ 把偶然的当前真值变成持久事实，给蕴涵加 $□$ 则要求转换在每个未来阶段继续有效。

合取与析取不额外加框，因为其构造在当前状态已经给出；真正跨越信息增长的是原子证据的保持和蕴涵对任意未来输入的承诺。这使加框的位置与各联结词在信息增长中的作用相对应。

T 与 4 在这幅图里各做一件事。T 让当前状态属于自己的未来，因此 $\square p$ 确实蕴含此刻的 $p$ ；4 把一次建立的必然性继续传到更高状态，形成持久链。缺少任一项，方框都不能完整模拟直觉主义信息序。

例子与边界

IPL 定理 $p\to p$ 翻译为

\square(\square p\to\square p),

内部是命题重言式，必然化后已在 K、因而在 S4 中可证。相比之下，排中律翻译为

\square p \lor \square(\square p\to\bot).

取自反传递两世界链 $w_0<w_1$ ，令 $p$ 只在 $w_1$ 真。在 $w_0$ ， $□p$ 因当前 $p$ 假而失败；第二个析取支也失败，因为未来 $w_1$ 满足 $□p$ 却不满足 $⊥$ 。所以该翻译不是 S4 定理，准确对应 IPL 不证明排中律。

语义证明把直觉主义持久模型与 S4 模型互相转换。由直觉主义模型出发，使用同一预序和持久赋值，可归纳证明 $w\Vdash A$ 当且仅当 $w\Vdash A^G$ ；反向从任意 S4 模型定义

V_I(p)=\{w:\mathcal M,w\Vdash\square p\},

该集合因传递性向上持久。原子与蕴涵条款中的方框正好让归纳闭合。

推论与应用

Gödel 翻译把中间逻辑问题转成 S4 扩展问题，使直觉主义 Kripke 框架、拓扑语义和模态框架理论能够互相借用。McKinsey–Tarski 的拓扑解释进一步把 $□$ 读成内部算子，并把 IPL 与适当拓扑有效式连接起来。

该嵌入也提供反模型转移：若 $A$ 不是 IPL 定理，可把直觉主义 Kripke 反模型转换为 S4 反模型来反驳 $A^G$ 。从 S4 反模型返回时，则用上述 $V_I$ 重建持久赋值，得到原公式 $A$ 的直觉主义反模型。

双重否定翻译把经典逻辑嵌入 IPL 的负片段；Gödel 翻译则把 IPL 嵌入 S4。前者新增否定以保存经典证明，后者新增方框以保存信息增长。

参考资料

Kurt Gödel, “Eine Interpretation des intuitionistischen Aussagenkalküls,” Ergebnisse eines mathematischen Kolloquiums 4, 1933, pp. 39–40。
J. C. C. McKinsey and Alfred Tarski, “Some Theorems about the Sentential Calculi of Lewis and Heyting,” Journal of Symbolic Logic 13(1), 1948, pp. 1–15。
Alexander Chagrov and Michael Zakharyaschev, Modal Logic, Oxford University Press, 1997, Chapters 2–3, intuitionistic and modal logics。