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.

带前提版本必须统一翻译前提，并区分局部与全局模态后承。不同教材也使用在所有子公式外加框、或不单独框原子的等价变体；引用定理时应先固定递归条款。

直觉

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

合取与析取不额外加框，因为其构造在当前状态已经给出；真正跨越信息增长的是原子证据的保持和蕴涵对任意未来输入的承诺。翻译因此不是统一给整式套一个方框，而是按联结词的证明含义选择位置。

T 与 4 在这幅图里各做一件事。T 让当前状态属于自己的未来，因此 $\square p$ 确实蕴含此刻的 $p$ ；4 把一次建立的必然性继续传到更高状态，形成持久链。缺少任一项，方框都不能完整模拟直觉主义信息序。翻译保留的是这种结构纪律，并不要求把 S4 的“必然”解释成某个主体的知识或物理必然。

例子与边界

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\},

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

目标不能降为 K。没有 T， $□p$ 不保证当前 $p$ ；没有 4，已经持久的事实不保证在更远未来继续持久。翻译定理也不声称 IPL 与 S4 语法相同或定理集合相等，只声称 $A\mapsto A^G$ 忠实保持并反映可证性。

推论与应用

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

该嵌入也提供反模型转移：若 $A$ 不是 IPL 定理，可把直觉主义 Kripke 反模型转换为 S4 反模型来反驳 $A^G$ 。反向得到的是翻译后公式的结论，不能任意删除方框并声称获得经典或直觉主义反模型。

双重否定翻译把经典逻辑嵌入 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。

形式陈述 ​

反向链接

形式陈述