{"id":"arxiv/2607.10880","url":"https://arxiv.org/abs/2607.10880","tags":["cs.AI","math.LO"],"score":0,"title":"First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)","domain":"cs.AI","source":"arxiv","authors":["Christoph Benzmüller","Daniel Kirchner"],"reviews":0,"subject":"cs.AI","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-12","reactions":{}}