First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

技术摘要：HOL 中的一阶模态逻辑：深度与浅层嵌入及其自动化忠实性

问题陈述
一阶模态逻辑（FML）结合了量化的表达能力与模态，是人工智能、计算机科学和哲学领域的重要框架。虽然命题模态逻辑（PML）向经典高阶逻辑（HOL）的嵌入已实现自动化，但将这些技术扩展到 FML 会引入显著的复杂性。具体而言，FML 需要处理变量绑定、替换以及对可能为不可数集的域进行量化。前人工作 [5] 建立了 PML 的深层与浅层嵌入方法论，但并未解决替换机制或一阶量化中固有的单射性问题。其挑战在于如何同时提供一种用于语法推理的深度嵌入（deep embedding）和一种用于自动化证明搜索的浅层嵌入（shallow embedding），并证明两者的相互忠实性，特别是在个体域为不可数集且浅层嵌入中的变量赋值被限制为可数集（例如自然数）的情况下。

方法论
作者扩展了 Isabelle/HOL 环境，以支持基于常数域 Kripke 语义的 FML。该方法采用了三种平行的嵌入方式：

1. 深度嵌入（Deep Embedding）： 公式被表示为一个归纳数据类型 $\mathcal{F}$。真值定义在模型 $\langle W, R, I, D \rangle$、赋值 $g$ 和世界 $w$ 的递归基础上。有效性（$ValD$）对所有模型、尊重域$D$ 的赋值以及世界进行全称量化。
2. 极大浅层嵌入（Maximal Shallow Embedding）： 公式被提升为显式抽象所有模型参数（$W, R, I, D, g, w$）的 $\lambda$-项。这允许直接使用 Isabelle 的自动化工具，但会导致复杂的类型。
3. 极小浅层嵌入（Minimal Shallow Embedding）： 实现为一个 Isabelle/HOL locale（MinS），该方法将静态参数（$I, R, W, g$）提升为 locale 参数，从而将公式类型简化为 $w \Rightarrow bool$。至关重要的是，存在量词使用 Isabelle 原生的元级绑定器进行编码，而模态算子则移动世界参数。

为了弥合深度嵌入与极小浅层嵌入之间的差距，作者开发了一套全面的替换机制（包括自由/约束变量谓词、避免捕获的替换、字母重命名），这是处理一阶量词所必需的，而在之前的命题逻辑工作中是缺失的。

一个核心的技术创新是实现了一阶模态逻辑的可数下降 Löwenheim–Skolem 定理的机械化。该定理保证了对于任何模型和任何可数初始子域 $D_0$，都存在一个保持真值的可数初等子域 $\mathcal{N}$。这被用于解决单射问题：由于极小浅层赋值 $g: V \to D$（其中 $V = \mathbb{N}$）无法对不可数集 $D$ 实现满射，因此直接的忠实性会失效。通过构造一个 $g$ 可以满射至其上的可数初等子域 $\mathcal{N}$，并证明在 $D$ 中的真值与在 $\mathcal{N}$ 中的真值一致，作者恢复了全域上的忠实性。

主要贡献

1. MinFMLinHOL 开发： 一个完整的 Isabelle/HOL 理论，涵盖了具有二元关系原语、命题连接词、存在量化以及常数域语义下方盒（box）模态的一阶模态逻辑。
2. 三种嵌入： 提供了深度嵌入、极大浅层嵌入以及轻量级的极小浅层嵌入（以 locale 形式封装）。
3. 全局忠实性定理： 引入了 MinS locale，使得能够提出一个强全局定理 FaithfulMS_all，即通过对所有极小浅层解释进行量化可以精确恢复深度有效性。
4. 替换机制： 为深度嵌入的 FML 开发了必要的语法工具（替换引理、重命名、基于规模的归纳），扩展了之前的命题逻辑工作。
5. 机械化的 Löwenheim–Skolem 定理： 实现了常数域 Kripke 语义下的下降 Löwenheim–Skolem 定理，这为证明深度嵌入与极小浅层嵌入之间忠实性的自动化奠定了基础。
6. 单射性解决： 设计了一个精炼的 locale MinS_surj，该 locale 假设赋值是对某个初等子域的满射，从而将忠实性从赋值的值域提升到全域 $D$。

结果
该开发通过以下实验进行了验证：

• 公理验证： 确认了 K-公理、必然化规则，以及 Barcan 公理和逆 Barcan 公式的有效性（这两者在常数域语义下成立）。
• 框架对应关系： 自动验证了反射、传递和对称框架与 T、4 和 B 公理模式之间的对应关系。
• 自动化： 展示了对 sledgehammer 和 nitpick 工具的使用。极小浅层嵌入允许 sledgehammer 将一阶模态目标视为普通的 HOL 目标，而 nitpick 可以通过缩小域类型来寻找反例，从而有效地绕过显式的域守卫。

意义
本文声称，这项工作是先前命题嵌入方法论向一阶情况发展的自然延伸。其主要意义在于证明了深度嵌入与浅层嵌入可以在同一个 HOL 理论中并存，并具备自动化的忠实性证明，即使在一阶量化和不可数域存在的情况下也是如此。通过利用 locale 机制和 Löwenheim–Skolem 定理，作者克服了变量赋值单射性的技术障碍，使得在不牺牲深度语法表示严谨性的前提下，能够使用强大的 HOL 自动化工具处理一阶模态逻辑。该工作为未来的扩展（如变化域语义或包含等价关系）奠定了基础，尽管目前侧重于最小的常数域片段。