Higher-order Kripke models for intuitionistic and non-classical modal logics

以下是维克多·巴罗斯 - 纳西门托（Victor Barroso-Nascimento）的论文《直觉主义与非经典模态逻辑的高阶克里普克模型》的通俗化解释，辅以富有创意的类比。

核心思想：构建“模型的模型”

想象一下，你试图理解人们如何做出关于什么是必然（必须发生）或可能（可能发生）的决策。

在标准逻辑（经典数学中使用的逻辑）中，我们使用一种称为克里普克模型（Kripke Model）的工具。你可以把克里普克模型想象成一张不同可能世界的地图。

• 世界：一个特定的情境，其中的事实为真或为假（例如，“正在下雨”）。
• 地图：连接这些世界的网络。如果世界 A 与世界 B 相连，意味着 B 是 A 的一个“可能替代”。
• 规则：如果某件事在世界 A 中是“必然”的，那么它在所有与 A 相连的世界中都必须为真。

问题所在：
这篇论文关注的是直觉主义逻辑，这是一种不同的数学体系，其使用者认为，除非你拥有证明，否则你不能简单地说“它要么为真，要么为假”。在这种逻辑中，真理是随着时间增长的（就像数学家发现新定理一样）。

在这种“真理增长”的系统中，传统处理“可能性”的方式非常混乱。它需要一个包含两种不同且纠缠在一起的连接（关系）的模型。这就像试图同时使用两张不同的地图来导航一座城市：一张是街道图，一张是地铁图，而它们之间相互作用的规则既复杂又难以可视化。

解决方案：“嵌套”方法

作者维克多·巴罗斯 - 纳西门托提出了一种视角的根本性转变。与其将两张地图塞进一张里，他建议构建一个模型的模型。

类比：时间线图书馆
想象一个图书馆，其中的每一本书都是一位数学家一生的时间线。

• 书内（一个模型）：书中包含代表不同时间点的章节（早晨、下午、晚上）。当你从早晨走向晚上时，这位数学家证明了更多的定理。这就是标准的“克里普克模型”。
• 图书馆（新模型）：现在，想象图书馆本身就是一张地图。这张新地图中的“世界”不仅仅是时间点，而是整本书（整条时间线）。

在这个新系统中：

1. “世界”是时间线：我们不再问“早晨是否在下雨？”，而是问“在时间线 A 的早晨，这是否为真？”
2. 连接：我们在书之间画线。如果“时间线 A"与“时间线 B"相连，意味着时间线 B 是时间线 A 的一个有效替代版本。
3. 神奇之处：要决定在时间线 A 的早晨某件事是否“可能”，我们不看时间线 A 的下午，而是看时间线 B 的早晨。

为什么这更好？
在旧的混乱系统中，“可能性”的规则必须经过精心工程设计，以适配“真理增长”的规则。而在这个新的“嵌套”系统中，规则简单而自然：

• 必然性：“我是否必然在早晨证明定理 X？” -> “在每一个与我相连的替代时间线的早晨，定理 X 是否都被证明了？”
• 可能性：“我是否可能在早晨证明定理 X？” -> “是否存在至少一个替代时间线，使得我在其早晨证明了定理 X？”

作者称此为高阶克里普克模型。这就像俄罗斯套娃：

• 第 0 层：单个世界（真值赋值）。
• 第 1 层：由第 0 层世界组成的模型（标准克里普克模型）。
• 第 2 层：由第 1 层模型组成的模型（新的“高阶”模型）。

两位主角：IK 和 MK

这篇论文在两个特定的逻辑系统上测试了这个新系统，作者称之为IK和MK。

1. IK（保守派）：这种逻辑有点谨慎。要检查某事是否必然，它会查看替代时间线以及该时间线内的所有未来时刻。这就像说：“如果我在任何替代日期的早晨都无法证明 X，那么它就不是必然的。”
2. MK（大胆派）：这种逻辑更强。它只查看替代时间线中的特定时刻。它忽略了该替代时间线的“未来增长”。这就像说：“如果我在某个替代日期的早晨能证明 X，无论那天晚些时候发生什么，那么这就是可能的。”

作者证明了他新的“时间线图书馆”系统完美适用于这两种逻辑。事实上，新系统非常清晰，使得旧系统的复杂规则（“双关系”规则）自然地呈现出来，而无需强行植入。

“宏大概括”

这篇论文最激动人心的部分是最后一节。作者提出，“模型的模型”这一想法不仅仅适用于直觉主义逻辑。

他提出了一个猜想（一个需要更多证明的强烈假设）：

• 旧问题：存在一些奇怪且复杂的逻辑系统，标准的克里普克模型（第 1 层）无法完全描述它们。它们是“不完备”的。
• 新希望：如果我们继续嵌套模型（第 2 层、第 3 层等），我们或许能够描述每一个存在的逻辑系统。

这就像电子游戏的图形。

• 标准模型（第 1 层）：就像 8 位图形。它们适用于简单的游戏，但在复杂场景中会变得模糊和块状。
• 高阶模型（第 2 层、第 3 层...）：就像 4K 或 8K 图形。通过添加更多层次的细节（模型中的模型），我们可以完美地渲染任何场景，无论逻辑变得多么复杂。

总结

这篇论文认为，我们看待逻辑模型的方式错了。与其试图将两种不同的规则塞进一张地图，我们应该建立一个层级结构，让模型成为构建新模型的基石。

• 旧方式：一张混杂着两种类型道路的混乱地图。
• 新方式：一个地图图书馆，你通过在不同地图之间穿梭来理解什么是可能的。

这种方法在数学上优雅，在概念上更接近索尔·克里普克（Saul Kripke）关于“可能世界”的原始思想，并且具有足够的潜力，去解决那些困扰数学家数十年的最棘手的逻辑问题。