这篇论文用Isabelle/HOL把一阶模态逻辑的深和浅嵌入都严格形式化了，还自动化证明了忠实性，做形式化逻辑或模态逻辑验证的值得看。
论文在Isabelle/HOL中扩展了之前从命题到一阶模态逻辑（FML）的深-浅嵌入方法，提供了三种嵌入：深嵌入、weighty maximal-shallow嵌入和lightweight minimal-shallow嵌入。minimal-shallow嵌入以Isabelle/HOL locale形式呈现，参数化于可达关系、世界索引解释、世界全域和变量赋值，并证明了全局忠实性定理。核心贡献是机械化了FML在恒定域Kripke语义下的可数向下Löwenheim-Skolem定理，解决了个体域不可数时变量赋值（可数域V=nat）的满射性问题。论文还为一阶量词开发了替换机制，包括自由/约束变量谓词、新鲜变量函数、避免捕获的替换、字母重命名、可替换性谓词、替换引理和基于大小的归纳原则。
First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)
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.