发表机构
University of Bamberg; Freie Universität Berlin（班贝格大学; 柏林自由大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究在 Isabelle/HOL 中把深度和浅度嵌入方法从命题逻辑扩展到一阶模态逻辑，给出三种嵌入，通过机械化向下勒文海姆 - 斯科伦定理解决满射性问题以实现忠实性，还开发了一阶量词所需的替换机制。
AI 中文摘要
我们在 Isabelle/HOL 中将先前工作的深度和浅度嵌入方法从命题逻辑扩展到具有常域克里普克语义的一阶模态逻辑（FML）。并列提供了 FML 到经典高阶逻辑（HOL）的三种嵌入：深度嵌入、重量级最大浅度嵌入和轻量级最小浅度嵌入。最小浅度嵌入以 Isabelle/HOL 区域的形式呈现，由可达关系、世界索引解释、世界全域和变量赋值参数化；该区域形式允许一个全局忠实性定理。核心技术贡献是对常域克里普克语义下 FML 的（可数）向下勒文海姆 - 斯科伦定理的机械化，解决了个体域不可数时出现的满射性问题，从而在整个域上产生忠实性。由于先前工作仅处理命题片段，我们在此开发了一阶量词所需的替换机制。
英文摘要
We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositional to first-order modal logic (FML) with constant-domain Kripke semantics. Three embeddings of FML into classical higher-order logic (HOL) are provided side by side: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is presented as an Isabelle/HOL locale, parametrised by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; the locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is a mechanisation, for FML under constant-domain Kripke semantics, of the (countable) downward Löwenheim-Skolem theorem, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it inside an extension of the minimal-shallow locale resolves the surjectivity problem that arises against an uncountable domain of individuals -- where the locale's variable assignment, having countable domain V = nat, cannot be surjective onto the domain -- and thereby yields faithfulness over the full domain. Since prior work treats only the propositional fragment, we develop here the substitution machinery (free/bound-variable predicates, the fresh-variable function, capture-avoiding substitution, alphabetic renaming, the substitutability predicate, the substitution lemma, and size-based induction principles) needed for the first-order quantifiers.
Comments24 pages. Extended version, with a source-code appendix, of a paper accepted at ARQNL 2026 (International Workshop on Automated Reasoning in Quantified Non-Classical Logics). The full Isabelle/HOL development is included as ancillary files
