在Isabelle/HOL中，我们将之前的工作中关于命题逻辑的深浅嵌入方法扩展到一阶模态逻辑（FML），并采用常域Kripke语义。我们提供了三种将FML嵌入经典高阶逻辑（HOL）的方法：深嵌入、重型最大浅嵌入和轻型最小浅嵌入。最小浅嵌入被呈现为一个由可达关系、世界索引解释、世界宇宙和变量赋值参数化的Isabelle/HOL局部结构；该局部结构形式承认一个全局的忠实性定理，表明对所有最小浅解释的量化正好恢复深有效性。我们的一个核心技术贡献是机制化的（可数）向下Löwenheim-Skolem定理，这为常域Kripke语义下FML的深浅嵌入之间的忠实性证明的自动化提供了基础。将其部署在最小浅局部结构的扩展中，解决了针对不可数个体域的单射问题——该局部结构的变量赋值具有可数域V = nat，无法对域进行单射，从而在整个域上实现忠实性。由于之前的工作仅处理命题片段，我们在此开发了所需的替换机制（自由/绑定变量谓词、新变量函数、避免捕获的替换、字母重命名、可替换性谓词、替换引理和基于大小的归纳原则），以满足一阶量词的需求。
博主点评： 该研究为一阶模态逻辑的高阶逻辑嵌入提供了新的视角，通过精细的机制化定理和局部结构的构建，成功解决了变量赋值的单射问题，推动了自动化验证的前沿。这种方法不仅丰富了理论框架，还为未来的逻辑系统设计奠定了基础。