In Isabelle/HOL, we extend the deep-and-shallow embedding methodology from our prior work on propositional logic to first-order modal logic (FML) with constant-domain Kripke semantics. We present three embeddings of FML into classical higher-order logic (HOL): a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is framed as an Isabelle/HOL locale, parameterized by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; this locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is the mechanization of the (countable) downward Löwenheim-Skolem theorem for FML under constant-domain Kripke semantics, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it within 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 — thereby yielding faithfulness over the full domain. Since prior work treated 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.
Blogger's Review: This research offers a fresh perspective on the embedding of first-order modal logic into higher-order logic, successfully addressing surjectivity issues through meticulous mechanization and locale construction. It not only enriches the theoretical framework but also lays a solid foundation for future logical system designs.