HOL中的一阶模态逻辑：具有自动化可靠性的深层与浅层嵌入（扩展预印本）

我们在Isabelle/HOL中，将我们先前工作的深层与浅层嵌入方法从命题逻辑扩展到具有常域Kripke语义的一阶模态逻辑（FML）。我们并排提供了三种将FML嵌入经典高阶逻辑（HOL）的方法：深层嵌入、重量级最大浅层嵌入和轻量级最小浅层嵌入。最小浅层嵌入以Isabelle/HOL区域（locale）的形式呈现，由可达关系、世界索引解释、世界宇宙和变量赋值参数化；该区域形式允许一个全局可靠性定理，该定理指出对所有最小浅层解释进行量化恰好恢复深层有效性。一个核心的技术贡献是，针对常域Kripke语义下的FML，机械化证明了（可数的）向下Löwenheim-Skolem定理，该定理支撑了我们深层与最小浅层嵌入之间可靠性证明的自动化。将其部署在最小浅层区域的扩展内部，解决了在不可数的个体域上出现的满射性问题——其中区域的变量赋值，具有可数域V = nat，不能满射到该域上——从而在完整域上产生可靠性。由于先前的工作仅处理命题片段，我们在此开发了处理一阶量词所需的替换机制（自由/约束变量谓词、新变量函数、避免捕获的替换、字母重命名、可替换性谓词、替换引理和基于大小的归纳原理）。