[ orcid=0000-0002-3392-3093, email=christoph.benzmueller@uni-bamberg.de]

[ orcid=0000-0001-9229-1148, email=daniel.kirchner@uni-bamberg.de]

first-order modal logic , Kripke semantics , shallow embedding , deep embedding , Isabelle/HOL , locales , elementary substructure , Löwenheim–Skolem theorem , Tarski–Vaught test , faithfulness automated

1 Motivation and Introduction↩︎

First-order modal logic (FML) sits at the intersection of two of the most pervasive sources of expressive power in symbolic logic: quantification and modality. It is a natural setting for many applications of logic in artificial intelligence, computer science, and philosophy. Embeddings into classical higher-order logic (HOL) [@Andrews02; @church1940] have repeatedly been shown to provide a fruitful host environment for such logics; see [@J48; @J75] and the references therein.

Shallow embeddings, which identify object-level formulae with HOL terms via the standard translation, give immediate access to Isabelle/HOL’s proof automation, including sledgehammer, nitpick, and auto. Deep embeddings, in which formulae are represented as elements of an inductively defined datatype, are needed for metalogical reasoning about syntax, substitution, or proof systems.

We have recently shown [@C98] that both approaches can be carried out simultaneously, in a single HOL theory, in such a way that mutual faithfulness proofs can be automated. That paper focuses on propositional modal logic (PML), where modality is the only complication. The natural next step, which we take in this paper, is to add quantification in order to move from PML to FML.

1.0.0.1 Contributions.

We contribute MinFMLinHOL,¹ an Isabelle/HOL development covering FML with binary relational atoms, propositional connectives, existential quantification, and the box modality, under constant-domain Kripke semantics.

1. We give a deep embedding (datatype \(\mathcal{F}\)) and two shallow embeddings, the maximal one carrying explicit dependencies on universe \(W\), accessibility \(R\), interpretation \(I\), domain \(D\) of individuals, variable assignment \(g\), and current world \(w\), and the minimal one carrying only the world dependency.

2. The minimal-shallow embedding is presented as an Isabelle/HOL locale MinS, parametrised by \(WW\), \(RR\), \(II\), \(gg\). Compared with the constants-only presentation of [@C98], the locale form admits a strong global faithfulness theorem FaithfulMS_all which states that quantifying over all locale interpretations recovers exactly deep validity. Locale-internal proofs transfer to deep validity by a single application of this theorem, demonstrated in §10.1.

3. We develop the substitution machinery (free/bound/fresh-variable predicates, capture-avoiding substitution, alphabetic renaming, substitutability predicate, the substitution lemma, and size-based induction principles) for the deep embedding of FML. This is new relative to [@C98], which treats only the propositional fragment and so contains no substitution machinery. The modal operator is transparent with respect to variable binding, so every free/bound/fresh predicate, every substitution and renaming function, and every induction principle extends by a single uniform Box clause.

4. We mechanise, for FML under constant-domain Kripke semantics, the (countable) downward Löwenheim–Skolem theorem: for every model and every countable initial \(D_0\sqsubseteq D\), there exists a countable elementary sub-domain \(\mathcal{N}\sqsubseteq D\) that contains \(D_0\) and through which truth in the deep embedding is preserved (theorem DownwardLowenheimSkolem). Applying this theorem to the minimal-shallow locale resolves the surjectivity problem that arises when the locale’s variable assignment \(gg : V \to D\) is forced to be surjective onto \(D\) to obtain faithfulness, which would effectively rule out uncountable domains \(D\). A refined locale MinS_surj that assumes its assignment function \(gg\) to be surjective onto an elementary sub-domain \(\mathcal{N}\) lifts faithfulness from the range of \(gg\) (i.e. from \(\mathcal{N}\)) to the full domain \(D\). Since for any formula \(\varphi\) the relevant part of any assignment function (i.e. its restriction to the free variables of \(\varphi\)) can be extended to an assignment that is surjective onto a suitable elementary sub-domain \(\mathcal{N}\), we obtain the strong faithfulness result FaithfulMS_all mentioned above.

5. We illustrate the development with experiments confirming the K-axiom, the necessitation rule, the Barcan and converse Barcan formulae (both valid here under constant domain), and frame correspondences between reflexive/transitive/symmetric frames and the T, 4, and B axiom schemata.

1.0.0.2 Organisation.

§2 fixes notation for HOL. §3 recalls FML in standard textbook form. §§4–6 present the three embeddings; the minimal embedding is given as a locale (§6), following the design principles laid down for PML in [@C98]. §7 outlines the substitution machinery, §8 mechanises the countable downward Löwenheim–Skolem theorem, and §9 establishes the faithfulness theorems. §10 reports on experiments. §11 discusses related work, and §12 concludes.

2 Classical higher-order logic↩︎

We adopt the presentation of HOL given in [@C98] without modification: simply typed \(\lambda\)-calculus over a base type \(o\) of truth values and a base type \(i\) of individuals, Henkin semantics, and the standard denotation \(\llbracket\cdot\rrbracket\) derived from a frame \(\mathcal{D}\) and an interpretation \(I\). The validity relation \(\models_{\mathrm{HOL}}\) is sound and complete for Henkin models, and Isabelle/HOL [@Isabelle] mechanises a fragment of HOL sufficient for the entire development that follows.

3 First-order modal logic (FML)↩︎

The syntax of FML, given a (nonempty) signature \(R\) of binary relation symbols and a denumerable set \(V\) of individual variables, is fixed by the grammar \[\label{eq:syntax} \varphi,\psi := r(x,y) \mid \neg\varphi \mid \varphi\wedge\psi \mid \exists x.\varphi \mid \Box\varphi\tag{1}\] for relation symbols \(r\in R\) and individual variables \(x,y\in V\). The further connectives \(\vee\), \(\supset\), \(\forall\), \(\Diamond\) are defined as usual.

A constant-domain Kripke model is a tuple \(\langle W,R,I,D\rangle\), where \(W\) is a set of possible worlds,² \(R\) is a binary accessibility relation on \(W\), \(D\) is a fixed nonempty domain of individuals, and the interpretation \(I\) assigns to each relation symbol \(r\) from the signature and each \(w\in W\) a binary relation \(I(r)(w)\subseteq D\times D\) on the domain. A variable assignment \(g\colon V\to D\) assigns a domain element to each individual variable; \(g[x\leftarrow d]\) is the variable assignment that agrees with \(g\) except that it sends \(x\) to \(d\).

Truth in a model is given recursively at each world by \[\begin{align} \langle W,R,I,D\rangle,g,w &\models r(x,y) && \text{iff } I(r)(w)(g(x),g(y))\\ \langle W,R,I,D\rangle,g,w &\models \neg\varphi && \text{iff not } \langle W,R,I,D\rangle,g,w \models \varphi\\ \langle W,R,I,D\rangle,g,w &\models \varphi\wedge\psi && \text{iff } \langle W,R,I,D\rangle,g,w \models \varphi \text{ and } \langle W,R,I,D\rangle,g,w \models \psi\\ \langle W,R,I,D\rangle,g,w &\models \exists x.\varphi && \text{iff } \exists d\in D.\, \langle W,R,I,D\rangle,g[x\leftarrow d],w \models \varphi\\ \langle W,R,I,D\rangle,g,w &\models \Box\varphi && \text{iff } \forall v\in W.\, R(w,v) \Rightarrow \langle W,R,I,D\rangle,g,v \models \varphi \end{align}\] A formula \(\varphi\) is valid iff \(\langle W,R,I,D\rangle,g,w\models\varphi\) for every model \(\langle W,R,I,D\rangle\), every assignment \(g\) into \(D\), and every world \(w\in W\). As usual, frame conditions on the accessibility relation correspond to modal axioms: reflexivity to T, transitivity to 4, symmetry to B, and so on (see §10 for our mechanised versions). We adopt constant-domain rigid-designator semantics; two things are meant. Constant domain: one domain \(D\) is shared by all worlds, rather than a world-indexed family \((D_w)_{w\in W}\), so the same individuals exist everywhere and both Barcan formulas are valid (§10). Rigid designation: a variable denotes the same individual at every world, i.e.the assignment \(g\colon V\to D\) is world-independent (not \(g\colon V\to W\to D\)); this is why a single \(g\) threads through the truth clauses, untouched by the \(\Box\)-shift. Relaxing either is the varying-domain extension left to future work (§11).

3.0.0.1 Relation to the basic first-order modal logic of the literature.

The setting just described is the constant-domain basic first-order modal logic studied by Bräuner and Ghilardi [@BraunerGhilardi2007]. For reasons of minimality we deviate from their formulation in three respects, none of which affects the modal-logical content of the system. First, our signature contains only binary relation symbols, whereas the cited reference admits predicate symbols of arbitrary arity (including 0-place symbols, i.e.propositional letters). Predicate symbols of other arities can be encoded in our binary fragment: unary atoms \(P(x)\) via \(P'(x,x)\) or \(P'(x,d_0)\) for a fixed parameter, and \(n\)-ary atoms (\(n\geq 3\)) by standard tuple-reification techniques. We do not pursue these encodings here, since the binary fragment already exhibits all the modal-logical phenomena we are interested in. Second, we omit the primitive equality predicate \(x = y\) that the cited reference includes; equality strictly increases expressive power and is not definable from a generic binary relation symbol alone. Extending our setting with equality is routine—one adds an identity clause to the interpretation \(I\) and the obvious recursion clause \(\langle W,R,I,D\rangle,g,w\models x = y\) iff \(g(x)=g(y)\)—but nothing in the present development depends on it. Third, we take \(\exists\) and \(\Box\) as primitives and define \(\forall, \Diamond\) by duality, whereas [@BraunerGhilardi2007] proceeds with \(\forall, \Box\); this is a purely presentational choice with no semantic content. Fourth, and likewise, we take \(\neg,\wedge\) as primitive and derive \(\vee,\supset\), rather than starting from \(\supset\) and a falsum \(\bot\). As the host logic is classical HOL the Boolean base is immaterial: we verified in Isabelle/HOL that \(\neg,\wedge\) and \(\supset,\bot\) are interderivable pointwise under the deep truth predicate. The base would matter for an intuitionistic object logic, where \(\{\supset,\bot\}\) is primitive; such a logic still embeds shallowly in HOL via its (monotone) Kripke semantics [@J21], so an intuitionistic-modal variant is feasible future work rather than a mere change of connectives (cf. [@KirstShillito2025], §11).

Subject to these scope restrictions, the semantics adopted here—constant domains, rigid variables, a single Kripke accessibility relation, and the standard clauses for \(\exists\) and \(\Box\)—coincides with the constant-domain basic semantics of [@BraunerGhilardi2007], so the familiar frame-correspondence facts for the axioms T, 4, B and for the Barcan / converse Barcan formulas apply unchanged.

4 Deep embedding of FML in HOL↩︎

Preliminaries (Figure 1) shared by all embeddings declare the types \(D\) (individuals), \(w\) (worlds), and \(R\) (relation symbols), together with the synonyms \(V:=\mathit{nat}\) (variables, via natural numbers, with substitution and renaming developed in §7), \(\mathcal{R}:=D\Rightarrow D\Rightarrow\mathit{bool}\), \(\mathcal{W}:=w\Rightarrow\mathit{bool}\), \(\mathcal{A}:=w\Rightarrow w\Rightarrow\mathit{bool}\), \(\mathcal{I}:=R\Rightarrow w\Rightarrow\mathcal{R}\), \(\mathcal{E}:=V\Rightarrow D\), and a domain restriction \(\mathcal{D}:=D\Rightarrow\mathit{bool}\). Variable-assignment update \(g[x\leftarrow d]\) (line 16 of the figure), the bounded universal \(\forall x{:}W.\,P\,x\) (lines 27–30), and set-as-predicate operations \(\sqsubseteq\), \(\sqcup\), Range, Univ, into, onto (lines 32–37) are introduced in the theory file MinFMLinHOL_preliminaries.thy and used by all subsequent files (in particular by the Löwenheim–Skolem proof of §8).

The deep embedding is a single inductive datatype \(\mathcal{F}\) whose constructors mirror the grammar 1 (theory MinFMLinHOL_deep.thy, Figure 2, lines 4–5; derived connectives on lines 7–10). The relative-truth predicate \(\langle W,R,I,D\rangle,g,w \models^d \varphi\) is declared in mixfix-syntax and defined by primitive recursion (lines 12–17): the existential quantifier (line 16) ranges over the explicit domain \(D\) (only those \(d\) with \(D\,d\)); the box ranges over \(R\)-successors inside the universe \(W\); the rest is standard. Validity ValD (line 19) closes universally over models, over domain-respecting assignments, and over worlds of the universe.

4.0.0.1 Universe and explicit domain.

The deep embedding’s validity makes two additional parameters explicit compared to the propositional embedding in [@C98]: the universe \(W\) of worlds (present in some form in any modal embedding) and the domain \(D\) of individuals over which the existential quantifier ranges (which has no analogue in the propositional setting). Both are represented here as HOL predicates, and ValD closes universally over models, over assignments lying in the domain (g into D), and over worlds in the universe (\(\forall w{:}W\)). The minimal-shallow embedding (§6) keeps \(WW\) as an explicit locale parameter to maintain a uniform dependency across all three embeddings. This has two practical benefits: the faithfulness theorems share the same parameters across the embeddings, and counterexamples found by nitpick display the universe restriction explicitly, matching the deep embedding’s presentation.

4.0.0.2 Auxiliary full-domain validity.

A second validity definition \(\models^{d'}\) restricts to variable assignments ranging over the universal domain Univ (the predicate \(\lambda x.\,\mathit{True}\), see Fig. 1, line 37) on the type \(D\) of individuals. This seems a convenience for nitpick, which apparently handles the trivial Univ predicate more efficiently than a guarded \(D\,x\) side condition on every binder. Since \(\models^d\varphi\) implies \(\models^{d'}\varphi\), any counterexample found by nitpick for \(\models^{d'}\) refutes \(\models^d\) as well. Moreover, the apparent restriction to \(D = \mathtt{Univ}\) does not weaken nitpick’s countermodel-finding power: nitpick is free to choose any concrete finite domain for the type of individuals, so a counterexample at some smaller predicate \(D\) can equivalently be found by shrinking the type and using the unguarded \(\mathtt{Univ}\) on it.

5 Maximal shallow embedding↩︎

The maximal shallow embedding lifts every primitive of FML to a \(\lambda\)-term abstracted over the explicit dependencies \(W\), \(R\), \(I\), \(D\), \(g\), \(w\). The type of formulae is \(\sigma := \mathcal{W}\Rightarrow\mathcal{A}\Rightarrow \mathcal{I}\Rightarrow\mathcal{D}\Rightarrow\mathcal{E}\Rightarrow w\Rightarrow\mathit{bool}\) (theory MinFMLinHOL_shallow.thy, Figure 3, line 4). Atoms consult the world-indexed interpretation (line 6), the existential introduces a meta-level HOL existential paired with a variable-assignment update (line 9), and the box is implemented by meta-level HOL universal quantification over accessibility-successors inside \(W\) (line 10). Derived connectives are on lines 12–15; relative truth and validity on lines 17–19. The pattern is identical to that of [@C98] for PML; the only difference is that the formula type \(\sigma\) is more complex, because both quantifier binding and the modal world-shift must be accommodated, and because the explicit domain \(D\) has been threaded through.

6 Minimal shallow embedding (locale-based)↩︎

The maximal shallow type carries every dependency, but only \(g\) (at the existential) and \(w\) (at the box) ever change during recursion. Following the design principle of [@C98], we promote four of the five static parameters (\(W\), \(R\), \(I\), \(g\)) to constants of the meta-logic (resp. to locale parameters). The domain of individuals arises implicitly as the range of the assignment function \(g\); the connection to explicit domains \(D\) is deferred to the refinement of §8. Promoting \(g\) to a static parameter is possible because the minimal-shallow existential is encoded directly by HOL’s own binder (ExM, line 12 of Fig. 4); the variable-assignment update therefore happens at the meta-level rather than via a recursive call with an updated \(g\), and \(gg\) need only interpret the free variables of the input formula.

In contrast to [@C98], however, we package the minimal embedding as an Isabelle/HOL locale [@ballarin2014].³ The locale form has two advantages:

• different minimal interpretations can coexist within a single theory, since the four parameters \((WW, RR, II, gg)\) are first-class arguments rather than fixed constants;

• it admits a strong global theorem, FaithfulMS_all (§9), stating that quantifying over all locale interpretations recovers exactly deep validity.

The locale MinS (theory MinFMLinHOL_shallow_minimal_locale.thy, Figure 4, line 4) fixes the four parameters and reduces the formula type to \(w\Rightarrow\mathit{bool}\) (line 7). The five primitive cases are on lines 9–13 (AtmM, NegM, AndM, ExM, BoxM), the derived connectives on lines 15–18, and relative truth and validity on lines 20–21.

Two design choices in this minimal-embedding setup are worth highlighting.

6.0.0.1 Binder for ExM.

ExM (and the derived AllM) is declared as a HOL binder over the variable type \(V\). This lets sledgehammer treat first-order modal goals as ordinary HOL goals: bound variables under ExM are HOL-level bound variables, so the external first-order provers behind sledgehammer can reason about them directly without needing to unfold the deep-embedding syntax. In the deep embedding, by contrast, ExD carries the variable name explicitly as part of the syntax tree (a named-variable binder, names encoded as natural numbers); the bridge between the two styles is built inside the deep-to-minimal translation DpToShM of §9 (see lines 8–9 of Fig. 6) via the safe-substitution operation \([v\!\leftarrow_r\!d](\varphi)\).

6.0.0.2 Constants vs.locale parameters.

For practical experimentation, the locale needs to be instantiated once at the global level for nitpick to construct usable countermodels: nitpick handles uninterpreted constants more reliably than locale parameters. The sibling theory MinFMLinHOL_shallow_minimal.thy (Figure 5) introduces uninterpreted constants RR, II, WW, gg (line 4) and performs a global_interpretation with them (line 5); this is the standard “constants-only” presentation of the minimal embedding, as in [@C98]. The locale formulation in MinFMLinHOL_shallow_minimal_locale.thy remains the single source of all theorems; the global interpretation propagates them to the constants automatically, without proof duplication.

7 Substitution machinery↩︎

The substitution lemma is necessary for the deep\(\leftrightarrow\)minimal-shallow faithfulness proof to handle the existential case. Since [@C98] treats only propositional modal logic, no substitution machinery is provided there; we develop one here, in the theory MinFMLinHOL_deep_subst_lemma.thy (Figures 10–11 in the appendix). The components are standard for first-order languages: a free-variable predicate is_free (Fig. 10, lines 4–10), a bound-variable predicate is_bound (lines 11–19), a fresh-variable function fresh (lines 21–26) with consequence lemmata L5–L11 (lines 27–33), the irrelevance lemma L12 (line 35), variable-for-variable substitution Subst written \([x{\leftarrow}z](\varphi)\) (lines 38–47), the substitutability predicate is_subst_for (Fig. 11, lines 67–72), the SubstitutionLemma itself (lines 74–77), the alphabetic-renaming function ren_for_subst (lines 79–87), and the safe-substitution operation ren_subst, written \([x\!\leftarrow_r\!z](\varphi)\) (line 103). Two size-based induction principles SInduct and QInduct (Fig. 11, lines 49–65) drive the trickier inductions.

Compared to plain first-order logic, every recursive definition and every inductive lemma in the chain is uniformly extended with a clause for the box modality. Because the \(\Box\) operator binds no variable but merely shifts the world, the box case is in every instance a single line of the same structurally trivial form: it descends transparently, just like the negation case (see e.g. Fig. 10, lines 9, 16, 26, 43, and Fig. 11, lines 72, 87), and is dispatched in every lemma between L5 and L29 by the same auto/force combinations. The two key outcomes are the substitution lemma SubstitutionLemma (Fig. 11, lines 74–77) and its safe-substitution form L27 (Fig. 11, lines 104–105); the latter is what the existential case of the faithfulness proof eventually invokes.

7.0.0.1 Coincidence-of-variable-assignments lemma.

A simple but useful consequence is that relative truth depends only on the values of the variable assignment on free variables (lemma L1 of MinFMLinHOL_ElementarySubstructure.thy, Fig. 12, lines 10–11), proved by induction.

8 The countable downward Löwenheim–Skolem theorem↩︎

The main result of this section is a mechanization of the (countable) downward Löwenheim–Skolem theorem for FML under constant-domain Kripke semantics (theory MinFMLinHOL_ElementarySubstructure.thy, full code in Figs. 12–14). It is used to resolve the surjectivity problem that arises when relating the deep and minimal-shallow embeddings over an arbitrary domain \(D\). Given this goal, we restrict our attention to the domain of individuals and simplify the construction by assuming that the domain of possible worlds is countable, as discussed in more detail below. We leave an extension to arbitrary domains of worlds open for future work.

8.0.0.1 The theorem.

For every constant-domain Kripke model \(\langle W,R,I,D\rangle\) and every countable initial sub-domain \(D_0\sqsubseteq D\), there exists a countable elementary sub-domain \(\mathcal{N}\sqsubseteq D\) that contains \(D_0\) and through which truth in the deep embedding is preserved.⁴ Theorem DownwardLowenheimSkolem (Fig. 13, lines 106–110) states that there exists a sub-predicate \(N\) with \(D_0\sqsubseteq N\sqsubseteq D\), with \(N\) countable, and with \(\langle W,R,I,D\rangle,g,w\models^d\varphi =\langle W,R,I,N\rangle,g,w\models^d\varphi\) for every \(g\) ranging into \(N\), every formula \(\varphi\), and every world \(w\). The proof is a single metis invocation that combines four ingredients: \(\mathcal{N}\sqsubseteq D\) (N_subset, line 66), \(\textsf{countable}(\mathcal{N})\) (countable_N, line 67), \(D_0\sqsubseteq\mathcal{N}\) (D0_in_N, line 69), and the pointwise core \(\mathcal{N}\_valid\) (lines 84–104). The witness sub-domain \(N\) is the elementary substructure \(\mathcal{N}\) constructed below.

8.0.0.2 Why this resolves the surjectivity problem.

In the minimal-shallow embedding the variable assignment \(gg : V \to D\) has \(V = \mathit{nat}\), so its image is countable. The deep embedding, however, lets the existential range over the entire domain \(D\). When \(D\) is uncountable, no variable assignment of this form can be surjective onto \(D\); consequently faithfulness over the full domain \(D\) does not follow immediately from FaithfulMDlem, whose statement is restricted to Range gg.⁵ The Löwenheim–Skolem theorem lets us replace \(D\) by a countable elementary sub-domain \(N\) onto which \(gg\) can be made surjective; faithfulness against \(D\) is then recovered by transferring truth between \(D\) and \(N\) via DownwardLowenheimSkolem. This transfer is supplied by the lemma \(\mathcal{N}\_valid\_surj\) (Fig. 14, lines 119–120; introduced under Locale-level packaging below) and applied in §9.

8.0.0.3 Construction.

By the Tarski–Vaught test — a sub-domain \(D'\sqsubseteq D\) is elementary iff every existential satisfied by an assignment into \(D'\) has a witness in \(D'\) — it suffices to construct a countable \(\mathcal{N}\sqsubseteq D\) in which witnesses for all such existentials are present. The construction proceeds in three steps.

8.0.0.3.1 (i) Witness collection.

Given a sub-domain \(S\) (which will be instantiated stage-by-stage in step (ii)), the set witnesses S W R I D (Fig. 12, lines 33–35) collects, via Hilbert’s choice, an existential witness in \(D\) for every existential \(\exists y . \varphi\) satisfied at a world \(w\) under an assignment of the free variables of \(\varphi\) to values that lie in \(S\). The auxiliary restricted_assigns (Fig. 12, lines 13–14) encodes partial maps from the free variables of \(\varphi\) to \(S\) as map_of applied to finite lists, and is chosen so as to inherit countability from \(S\): \(\textsf{countable}(S)\Rightarrow \textsf{countable}(\texttt{witnesses}\,S\,W\,R\,I\,D)\) (lemma countable_witnesses, line 41).⁶

8.0.0.3.2 (ii) Stage-wise saturation.

The elementary substructure is the limit of an iterated witness collection seeded by \(D_0\). The stages \(\mathcal{N}_i\) are defined by primitive recursion on the stage index (Fig. 13, lines 52–53); the limit \(\mathcal{N}\) is the predicate-level union over all stages (line 65). Each stage adds witnesses for existentials satisfied at assignments ranging into the previous stage. By induction on the stage index, every stage is countable whenever \(D_0\) is (lemma countable_N_i, lines 55–56), and \(\mathcal{N}\) is countable as a countable union of countable sets (countable_N, line 67). The lemma N_subset (line 66) shows \(\mathcal{N}\sqsubseteq D_0\sqcup D\) unconditionally; under the hypothesis \(D_0\sqsubseteq D\) this collapses to \(\mathcal{N}\sqsubseteq D\), so the construction stays inside the original domain.

8.0.0.3.3 (iii) Tarski–Vaught test.

The theorem \(\mathcal{N}\_valid\) (Fig. 13, lines 84–104) states that truth in the substructure agrees with truth in the full domain or, equivalently, that \(\mathcal{N}\) is an elementary sub-domain of \(D\). Its proof relies on the auxiliary lemma TarskiVaught (lines 72–77), which is derived by induction on \(\varphi\). In the proof of \(\mathcal{N}\_valid\), the witness condition of Tarski–Vaught is satisfied by construction: the witness produced by Hilbert’s choice in the definition of witnesses is collected into the next stage by the recursive case of \(\mathcal{N}_i\) (line 53), and hence into \(\mathcal{N}\). While the witness is constructed relative to a finite restriction of the assignment \(g'\) to the free variables of \(\varphi\), i.e. the auxiliary restrict_assign/unrestrict pair (lines 16–31), it follows by the coincidence-of-assignments lemma L1 (lines 10–11) that it is also a witness relative to the full variable assignment \(g'\).

8.0.0.4 The countable-worlds assumption.

To satisfy the condition of the Tarski-Vaught test, we construct witnesses for every world. However, since the countability argument requires the witness set at each stage to be countable, this in turn requires us to assume that type w of worlds itself is countable. While this additional assumption simplifies the construction, future work can generalize this by also constructing modal witnesses besides the existential witnesses and thereby also constructing a suitable countable subset of worlds, which will make the assumption unnecessary. Since our primary goal is to avoid the surjectivity problem in preserving validity between the minimal shallow and deep embedding while using substitution in the translation of the existential, for now, we forgo this additional complication and focus on the domain of individuals only. Therefore, we axiomatically impose that the domain of worlds is countable (countable_worlds, Fig. 12, lines 5–7).

8.0.0.5 Locale-level packaging.

With \(\mathcal{N}\) available, we extend the minimal-shallow locale. The locale MinS_surj (Fig. 14, lines 114–121) extends MinS with a domain predicate \(DD\), an initial sub-domain \(DD_0\sqsubseteq DD\), and the assumption that \(gg\) is surjective onto the elementary substructure \(\mathcal{N}\,DD_0\,WW\,RR\,II\,DD\). The lemma \(\mathcal{N}\_valid\_surj\) (lines 119–120) is the operational reading of the Löwenheim–Skolem theorem inside the locale: under the surjectivity hypothesis, truth at the full domain \(DD\) coincides with truth restricted to Range gg. This lifts the deep\(\leftrightarrow\)minimal-shallow faithfulness proof, whose natural statement is in terms of Range gg, to the full domain \(DD\). Lemma gg_ex (lines 123–127) establishes that, for any nonempty countable \(D_0\), there exists a variable assignment surjective onto the elementary substructure \(\mathcal{N}\,D_0\,W\,R\,I\,D\). A further locale MinS_specific (lines 130–152) packages a particular case useful for transferring truth at a given assignment \(g_0\) to a constructed surjective \(gg\) that agrees with \(g_0\) on the free variables of a target formula; the lemma \(\mathcal{N}\_valid\_specific\) (lines 150–151) transfers truth from \(\langle WW,RR,II,DD\rangle,g_0,w\models^d\varphi\) to the constructed setting. This in turn powers theorem FaithfulMS_all of §9.

9 Faithfulness, automated↩︎

Two mappings translate deep formulae into shallow ones (theory MinFMLinHOL_faithfulness_locale.thy, Fig. 6): DpToShS, written \(\llbracket\cdot\rrbracket\), on lines 5–6, and DpToShM, written \((\!\lvert\cdot\rvert\!)\), on lines 8–9. The first recurses transparently through every primitive of FML, since both source and target use named-variable existentials. The second, DpToShM, is declared inside the locale MinS; its existential clause (line 9) inserts a safe substitution \([v\!\leftarrow_{r}\!d](\varphi)\) that replaces the named variable \(v\) in \(\varphi\) with the HOL-bound \(d\), bridging ExD’s named-variable representation and ExM’s HOL-binder representation.

9.0.0.1 Pointwise lemmata.

The deep\(\leftrightarrow\)maximal-shallow correspondence (theorem FaithfulSDlem, Fig. 6, lines 11–12) is derived by induction on \(\varphi\) with auto simp: DefS DefD; the global form FaithfulSD (line 13) follows from ValD_def and ValS_def. Similarly, the deep\(\leftrightarrow\)minimal-shallow correspondence is first shown in the pointwise formulation FaithfulMDlem (Fig. 6, lines 17–18). The proof is a single induct on \(\varphi\) with rule QInduct (arbitrary in \(w\)), with simp add: DefD DefM discharging the propositional and box cases, and a final blast dispatching the existential case. The global form then follows from ValM_def.

9.0.0.2 Lifted faithfulness.

Inside MinS_surj, the additional fact \(\mathcal{N}\_valid\_surj\) replaces Range gg by \(DD\) in FaithfulMDlem, yielding theorem FaithfulMD_surj (Fig. 6, lines 32–33): deep\(\leftrightarrow\)minimal-shallow faithfulness against the full domain \(DD\), even when \(DD\) is uncountable.

9.0.0.3 Global faithfulness across all locale interpretations.

The locale form admits a strong global theorem, FaithfulMS_all: a deep validity is precisely a validity that holds against every concrete model, and quantifying over all locale interpretations of MinS captures exactly that notion (Fig. 6, lines 40–42). The proof uses the MinS_specific locale: the right-to-left direction follows by unfolding deep validity and applying FaithfulMD; the left-to-right direction unfolds deep validity at an arbitrary model \(\langle WW,RR,II,DD\rangle,g_0,w\), instantiates MinS_specific for that model and the target formula, applies \(\mathcal{N}\_valid\_specific\) to transfer truth to a constructed surjective \(gg\), and invokes FaithfulMD. In Isabelle this collapses to two short tactic invocations. The operational meaning is that any statement provable inside the locale—i.e.from purely minimal-shallow infrastructure—transfers directly to deep validity. We illustrate this in §10.1.

9.0.0.4 Global instance.

For convenience, the theory MinFMLinHOL_faithfulness.thy (Figure 7) also performs a concrete global_interpretation of MinS_surj with initial domain \(DD_0 := \{\textit{undefined}\}\) (line 15) and full domain Univ (line 17), using specification (line 16) to introduce a concrete gg that is surjective onto an elementary sub-domain. All the locale-level faithfulness theorems are then re-issued at the global level against the full domain (lines 5–11, 19–21).

10 Experiments↩︎

We illustrate the development with the test file MinFMLinHOL_experiments.thy (Figure 9 in the appendix). The propositional tautologies (lines 7–12) and the K axiom (lines 14–16) are dispatched by auto after unfolding DefD, DefS, or DefM; the necessitation rule (lines 18–20) is similarly automatic. Throughout MinFMLinHOL_experiments.thy every example theorem is stated and proved in all three embedding variants (with the \(d\), \(s\), and \(m\) superscripts), to demonstrate that the alignment between the embeddings is operational.

10.0.0.1 Barcan and converse Barcan.

Both BF and CBF are valid in our constant-domain semantics; following the d/s/m discipline, each is proved in the three embedding variants with the uniform tactic unfolding DefD/DefS/DefM by auto (Fig. 9, lines 26–31). The CBF analogues are proved with the same one-line tactics. In a varying-domain semantics, neither BF nor CBF would be HOL-derivable without further side conditions. The \(\Diamond/\exists\) versions (lines 33–38) are equally automatic, illustrating that under constant domain \(\Diamond\exists x\) and \(\exists x\Diamond\) coincide.

10.0.0.2 Disproofs by nitpick.

nitpick reliably finds finite countermodels for invalid schemata (Fig. 9, lines 40–48). The schema \(\varphi\supset\Box\varphi\) (modal collapse, lines 44–45) fails by a 2-world model in which \(P\) holds at the start world but not at its \(R\)-successor. The schema \(\Box\varphi\supset\varphi\) (lines 47–48) fails on a model with no reflexive edges, illustrating the correspondence with the T axiom. Several such disproofs use the auxiliary full-domain relation \(\models^{d'}\), marked “Note:needs full domain \(D\)”.

10.1 Locale-based transfer in action↩︎

A short demonstration of FaithfulMS_all is given in MinFMLinHOL_experiments_locale.thy (Figure 8). The K-axiom is first proved purely from minimal-shallow definitions, inside the locale (lemma K_MinS, line 11), and transfer to deep validity is then a single line (line 13), where MinS_to_Deep (line 6) is the directional reading of FaithfulMS_all. This is the operational pay-off of the locale design: the user proves once in the simplest setting, and the strong faithfulness theorem ports the result to the syntactic deep embedding.

10.1.0.1 Auxiliary locale-level rewrites.

The mapping DpToShM is defined only on the primitive cases of the deep embedding. Defined connectives such as \(\supset^d\) and \(\vee^d\) are unfolded at the top of the deep embedding before DpToShM is applied; for the experiments we add two locale-level rewrite rules (Fig. 8, lines 8–9) to the DefM bag, namely OrM_simp and ImpM_simp. These rewrites are entirely cosmetic but smooth the locale-level proofs above.

11 Related work and discussion↩︎

The shallow-embedding approach to FML in HOL has a long history. Benzmüller and Paulson [@J21; @J23] introduced a minimal shallow embedding of higher-order modal logic in HOL targeting computational metaphysics; that work, however, did not maintain a corresponding deep embedding, and its faithfulness was not mechanised within HOL. Recent work by Benzmüller and Reiche [@C90] on public announcement logic shows the necessity of explicit dependencies on evaluation domains in a heavyweight shallow embedding; our maximal shallow embedding can be seen as a propositional skeleton of that construction. Other deep embeddings of FML or related logics in proof assistants typically target metalogical results (e.g. completeness, cut-elimination) rather than mutual faithfulness with shallow embeddings, and so do not lend themselves to the same automated proof-and-disproof dialogue as ours.

11.0.0.1 First-order constant-domain mechanisations.

Closest in subject matter is Kirst and Shillito [@KirstShillito2025], who give a Coq-verified completeness proof for first-order bi-intuitionistic logic with constant domains. Their aim is complementary to ours: a syntactic metatheorem (completeness of a calculus) for an intuitionistic object logic, versus our semantic bridge (machine-checked deep\(\leftrightarrow\)shallow faithfulness with automated proof and nitpick disproof) for a classical modal one. Where they preserve constant domains through a completeness construction, we must instead reconcile the deep embedding’s quantification over an arbitrary domain with the countable assignment of the minimal-shallow locale — precisely what the Löwenheim–Skolem step of §8 does.

11.0.0.2 Novelty and outlook.

Kripke-semantics mechanisations are by now common, and we claim none as such. New, to our knowledge, is their combination in one first-order modal HOL theory: a deep and two shallow embeddings kept in machine-checked mutual faithfulness, the locale-based global theorem FaithfulMS_all, and a constant-domain downward Löwenheim–Skolem theorem deployed to defuse the surjectivity obstacle against uncountable domains. For the LogiKEy methodology [@J48] this matters concretely: it supplies, for the quantified modal case, both the syntactic deep embedding hitherto lacking and a machine-checked guarantee that shallow-level automation stays faithful to it.

11.0.0.3 Locales for shallow embeddings.

Locales [@ballarin2014] have been used widely in Isabelle to parametrise algebraic structures, but their use to package shallow embeddings of object logics, with a global faithfulness theorem quantifying over all interpretations, appears to be new. Each locale parameter corresponds to a degree of semantic dependency that the user is free to fix or to leave open. The strong global faithfulness theorem FaithfulMS_all is the technical pay-off and is, to our knowledge, novel.

11.0.0.4 The Löwenheim–Skolem theorem in HOL.

Within Isabelle, formalisations of the Löwenheim–Skolem theorem exist for first-order logic (e.g. the AFP entry for first-order logic, and [@From2022]), but to our knowledge none has previously been formulated in the constant-domain Kripke-semantics setting of FML, nor deployed to bridge a deep and a minimal-shallow embedding. The mechanisation in §8 is fairly self-contained (\(\sim 200\) lines including all auxiliary lemmata) and could be reused for other shallow embeddings of quantified non-classical logics that face the same surjectivity obstacle. Avoiding the restriction to a countable domain of possible worlds remains a subject for future work.

11.0.0.5 Availability.

The full Isabelle/HOL development is bundled with this arXiv version as ancillary files (see the “Ancillary files” listing on the abstract page) and consists of eleven theory files: preliminaries, deep, deep-substitution-lemma, maximal-shallow, minimal-shallow locale and global instance, faithfulness locale and global instance, elementary-substructure, experiments and locale-based experiments, together with an Isabelle ROOT session file. It loads cleanly in the latest versions of Isabelle/HOL [@Isabelle].

11.0.0.6 Future work.

The natural next step is to extend the present constant-domain treatment to varying-domain semantics, which requires replacing the rigid \(\mathcal{E}:=V\Rightarrow D\) by a world-indexed variable assignment \(\mathcal{E}:=V\Rightarrow w\Rightarrow D\) and adjusting the existential cases of all three embeddings simultaneously. The infrastructure we have built — bag-based simplifier rule sets, pointwise faithfulness lemmata, the size-based induction principle QInduct, and the elementary-substructure construction — carries over without conceptual modification, although the elementary-substructure construction must then iterate over both the domain dimension and the world dimension. A second direction is to generalise the box modality to multimodal accessibility relations and to inflationary/non-normal modalities, where the only change is in the box clause of every relevant function and the corresponding clause of the substitution machinery.

12 Conclusion↩︎

MinFMLinHOL demonstrates that the deep-and-shallow methodology of [@C98] scales smoothly to logics with both binding and modality. The new ingredients are a locale-based formulation of the minimal embedding, a corresponding strong global faithfulness theorem, and a Tarski–Vaught-style mechanisation of the (countable) downward Löwenheim–Skolem theorem that resolves the surjectivity problem against arbitrary domains of individuals. All faithfulness proofs are mechanised, with pointwise lemmata and the substitution machinery carrying virtually all of the work.

12.0.0.1 Disclosure on the use of generative AI.

The authors used generative AI assistants (Anthropic’s Claude family of models) during the preparation of this manuscript: to draft initial prose for several sections, to suggest reformulations and shortenings, and to mechanise the bookkeeping of cross-references between the LaTeX source and the Isabelle/HOL files. The mathematical content, the Isabelle/HOL theory development, and the specific design choices (notably the locale-based packaging of the minimal embedding, the formulation of FaithfulMS_all, and the elementary-substructure construction) are due to the authors. All text and all Isabelle/HOL proofs in the final manuscript and Archive have been read, verified, and edited by the authors; the authors take full responsibility for the content.

13 Appendix↩︎

The following figures show the rendered Isabelle/HOL source files that supplement the body of the paper. Line numbers refer to the positions in the corresponding theory file.

---

1. The Min prefix stands for minimal; the reasons will become clear below.↩︎

2. Textbook presentations usually require \(W\) nonempty; our mechanisation need not. The universe \(W\) is a predicate over a nonempty world type \(w\), and validity closes over all such predicates: the empty one contributes only the vacuously true \(\forall w{\in}\emptyset.(\cdots)\), so it neither trivialises validity nor need be excluded. We checked in Isabelle/HOL that adding a nonemptiness premise on \(W\) (or on \(D\), where the guard \(g\,\mathtt{into}\,D\) already voids the empty case) leaves validity unchanged—which is why the issue never arose.↩︎

3. A locale in Isabelle/HOL is a named context that fixes typed parameters and (optionally) assumes axioms about them; theorems proved inside the locale automatically apply to every instantiation of the parameters that satisfies the assumptions.↩︎

4. We write \(\mathcal{N}\) short for \(\mathcal{N}(D_0,\,W,\,R,\,I,\,D)\).↩︎

5. The restriction is due to the use of substitution for the translation of the existential, which is necessary since the assignment \(gg\) is a fixed parameter.↩︎

6. Since we construct witnesses for every world \(w\), countability only follows if the domain of worlds itself is countable, which is discussed in more detail below.↩︎