Paper deep dive
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
Christoph Benzmueller, Daniel Kirchner
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 9/11/2026, 3:38:13 AM
Summary
This paper presents a formalization of Monadic Second-Order Logic (MSO) within Isabelle/HOL, introducing three distinct embeddings: a deep embedding using an inductive datatype, a maximal-shallow embedding with explicit semantic parameters, and a minimal-shallow embedding using Isabelle locales to collapse formula types to bool. A key technical contribution is a two-sorted substitution apparatus that handles capture-avoiding substitution and renaming for both first- and second-order variables. The authors prove the automated faithfulness of all three embeddings and demonstrate a mechanized two-sorted downward Löwenheim–Skolem theorem, showing that the minimal embedding recovers general (Henkin-style) MSO validity relative to countable assignment ranges, while distinguishing it from the standard full-domain reading. Experiments on classical MSO landmarks like Boolean closure and reachability validate the theoretical distinctions between the embeddings.
Entities (10)
Relation Signals (9)
MSOinHOL → uses → Isabelle/HOL
confidence 100% · In Isabelle/HOL, we apply the deep-and-shallow embedding methodology... We contribute MSOinHOL, an Isabelle/HOL development
Christoph Benzmüller → authored → MSOinHOL
confidence 95% · Christoph Benzmüller... Daniel Kirchner... We contribute MSOinHOL
Daniel Kirchner → authored → MSOinHOL
confidence 95% · Christoph Benzmüller... Daniel Kirchner... We contribute MSOinHOL
MSOinHOL → implements → Monadic Second-Order Logic
confidence 95% · We contribute MSOinHOL, an Isabelle/HOL development of MSO with binary relational atoms...
MSOinHOL → includes → Minimal Shallow Embedding
confidence 95% · Three embeddings are developed side by side: ... a minimal-shallow embedding
MSOinHOL → includes → Maximal-Shallow Embedding
confidence 95% · Three embeddings are developed side by side: ... a maximal-shallow embedding... and a minimal-shallow embedding
MSOinHOL → includes → Deep Embedding
confidence 95% · Three embeddings are developed side by side: a deep embedding... a maximal-shallow embedding... and a minimal-shallow embedding
MSOinHOL → proves → Löwenheim–Skolem Theorem
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation); a maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments explicitly; and a minimal-shallow embedding -- a locale that fixes those parameters, collapsing the formula type to bool. The enabling new ingredient is a two-sorted substitution apparatus -- capture-avoiding substitution, renaming, and a substitution lemma per namespace -- in which each binder is transparent for the other; faithfulness of all three embeddings is mechanised and largely automated. Our central contribution is a fully mechanised two-sorted downward Loewenheim-Skolem theorem: the minimal embedding recovers deep validity relative to the (countable) assignment ranges, and this range-relative reading is shown to coincide with the general (Henkin-style) reading of MSO, whereas the standard reading validates strictly more formulas, witnessed by comprehension. Both readings are nonetheless recovered from the minimal embedding, differing only in the admitted interpretations: all of them for the general reading, only the elementary substructures of the full model for the standard. We exercise the embeddings on classical MSO landmarks: the Boolean-closure and graph schemata hold under the full second-order domain yet fail in the minimal embedding, making the dichotomy concrete, while reachability and 2-colorability are refuted throughout.
Tags
Links
- Source: https://arxiv.org/abs/2609.07345v2
- Canonical: https://arxiv.org/abs/2609.07345v2
Trouble viewing inline? Open PDF directly →
Full Text
68,686 characters extracted from source content.
Expand or collapse full text
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint) Christoph Benzmüller[0000-0002-3392-3093]^[ 0000-0002-3392-3093] †thanks: Dedicated to David Basin, whom I first met in Saarbrücken in the mid-1990s, over a shared enthusiasm for automated reasoning, formal methods, and expressive logics. Affiliation: University of Bamberg, Bamberg, Germany , E-mail christoph.benzmueller@uni-bamberg.de Affiliation: Freie Universität Berlin, Berlin, Germany Daniel Kirchner[0000-0001-9229-1148]^[ 0000-0001-9229-1148] E-mail daniel.kirchner@uni-bamberg.de Affiliation: University of Bamberg, Bamberg, Germany , E-mail christoph.benzmueller@uni-bamberg.de Abstract In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation); a maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments explicitly; and a minimal-shallow embedding — a locale that fixes those parameters, collapsing the formula type to bool. The enabling new ingredient is a two-sorted substitution apparatus — capture-avoiding substitution, renaming, and a substitution lemma per namespace — in which each binder is transparent for the other; faithfulness of all three embeddings is mechanised and largely automated. Our central contribution is a fully mechanised two-sorted downward Löwenheim–Skolem theorem: the minimal embedding recovers deep validity relative to the (countable) assignment ranges, and this range-relative reading is shown to coincide with the general (Henkin-style) reading of MSO, whereas the standard reading validates strictly more formulas, witnessed by comprehension. Both readings are nonetheless recovered from the minimal embedding, differing only in the admitted interpretations: all of them for the general reading, only the elementary substructures of the full model for the standard. We exercise the embeddings on classical MSO landmarks: the Boolean-closure and graph schemata hold under the full second-order domain yet fail in the minimal embedding, making the dichotomy concrete, while reachability and 22-colorability are refuted throughout. Keywords: Monadic second-order logic Deep and shallow embedding Isabelle/HOL Henkin semantics Automated faithfulness 1 Motivation and Introduction Monadic second-order logic (MSO) sits at the heart of a body of results connecting logic, automata, and graph/tree structure theory [14, 21, 16]. It extends first-order relational logic with a single, but powerful, additional resource: quantification over monadic predicates, i.e. over sets of individuals. On the algorithmic side, a substantial line of work led by David Basin approaches MSO through automata and decision procedures: Basin and Klarlund use the weak monadic second-order theory of one successor (WS1S) and canonical string automata to specify and verify hardware, obtaining a decision procedure with counter-model generation [3, 4], and Ayari and Basin develop bounded model construction for monadic second-order logics [1]. That line targets decidable fragments over strings and trees; the present work is complementary — it embeds full and general (Henkin-style) MSO into classical higher-order logic for interactive proof and metatheory, rather than deciding a fixed fragment. Embeddings in classical higher-order logic (HOL) [15] are a versatile host for non-classical and expressive logics: treating HOL as a universal meta-logic, a wide range of object logics — modal, deontic, epistemic, and others — inherit its semantic infrastructure and proof automation. This is the basis of LogiKEy [8, 9], a logic-pluralistic knowledge representation methodology in HOL, from computational metaphysics to ethical and legal reasoning; it grew out of the early modal-logic embeddings developed together with Paulson [10, 11]. Shallow embeddings, which represent object-level formulae directly as HOL terms (for MSO, by the standard translation of connectives and quantifiers), give immediate access to Isabelle/HOL’s proof automation — the prover sledgehammer, the finite-countermodel finder nitpick, and auto. Deep embeddings, in which formulae are elements of an inductively defined datatype, are needed for metalogical reasoning about syntax, substitution, or proof systems. Shallow semantical embeddings of propositional and quantified modal logics in HOL were developed by Benzmüller and Paulson [10, 11], initially without a deep embedding or a mechanised faithfulness proof. We have recently shown [12] that both embeddings can be carried out simultaneously, in a single HOL theory, with mutual faithfulness proofs automated. That development, however, only treats propositional modal logic, whose binders are modal operators carrying no variable binding. The same methodology now spans a range of logics; we develop it here for monadic second-order logic (MSO). We take up MSO not for expressive strength but for the phenomena of its second-order quantifier — above all the standard-versus-general (Henkin) distinction behind our central result — and, on the technical side, for its two-sorted binding: quantifying over individuals and sets of individuals at once, MSO’s first- and second-order existentials are the two binders our apparatus must handle. Contributions. We contribute MSOinHOL, an Isabelle/HOL development of MSO with binary relational atoms (no primitive equality), monadic predication atoms, the propositional connectives, a first-order existential quantifier, and a monadic second-order existential quantifier. The particular contributions include: 1. A deep embedding (datatype ℱF) and two shallow ones: a maximal embedding carrying explicit dependencies on the interpretation, the two domains, and the two assignments; and a minimal embedding that fixes the interpretation and assignments as locale parameters, collapsing the formula type to bool. 2. The minimal embedding is an Isabelle/HOL locale MinS; it admits a faithfulness theorem FaithfulMS_all stating that quantifying over all locale interpretations recovers exactly deep validity relative to the assignment ranges. Faithfulness of the maximal-shallow embedding with respect to the deep one (FaithfulSD) is likewise established and automated. 3. A two-sorted substitution apparatus for the deep embedding — free/bound/fresh predicates, capture-avoiding substitution, alphabetic renaming, the substitution lemma, and size-based induction — developed once per variable namespace, with each binder transparent for the other. 4. Experiments confirming tautologies, the monadic comprehension schema (proved for an arbitrary formula, generalising two ad-hoc instances), and nitpick countermodels for invalid schemata. 5. A suite of classical MSO landmarks — Boolean closure [14, 21], monadic graph operations [16], reachability [3], and 22-colorability [21] — across all three embeddings: the closure and graph schemata hold under the full second-order domain but fail in the general minimal embedding (recovered by its elementary refinement), while reachability and 22-colorability are refuted throughout. 6. The converse: range-relative validity coincides with general (Henkin-style) MSO validity, by a two-sorted Löwenheim–Skolem construction, while the standard reading validates strictly more formulas — all formally proved. Organisation. §2 fixes notation for HOL and §3 recalls MSO. §4 presents the three embeddings – deep, maximal-shallow, and the locale-based minimal-shallow (§4.4). §5 outlines the two-sorted substitution machinery, §6 the faithfulness theorems, and §7 the surjectivity problem. §8 reports experiments and §9 concludes and discusses related work. The complete formal development is published as the Archive of Formal Proofs entry MSOinHOL [6]. Rendered theory sources appear in App. 0.B and the full two-sorted Löwenheim–Skolem proof in App. 0.A. 2 Classical higher-order logic We adopt the presentation of HOL given in [12] without modification: simply typed λ-calculus over base types o (truth values) and D (individuals), Henkin semantics, and the standard denotation ⟦⋅⟧ · derived from a frame D and an interpretation I. The validity relation ⊧HOL _HOL is sound and complete for Henkin models [17],11 1 The landscape of standard models, Henkin models, and Andrews’ weaker v-complexes, and the role of extensionality in fixing the class of Henkin models, is analysed by Benzmüller, Brown, and Kohlhase [5]; the shallow embeddings below inherit HOL’s functional and Boolean extensionality. and Isabelle/HOL [19] mechanises a fragment of HOL sufficient for all that follows. In particular, the second-order domain of MSO is the HOL function type D⇒oD o, so monadic sets (resp. predicates) are first-class HOL objects. 3 Monadic second-order logic (MSO) The syntax of MSO, given a (nonempty) signature R of binary relation symbols, a denumerable set V of individual (first-order) variables, and a denumerable set V2V_2 of monadic (second-order) variables, is fixed by the grammar φ,ψ:=r(x,y)∣X(x)∣¬φ∣φ∧ψ∣∃x.φ∣∃X.φ ,ψ:=r(x,y) X(x) ψ ∃ x. ∃ X. (1) for relation symbols r∈Rr∈ R, individual variables x,y∈Vx,y∈ V, and monadic predicate variables X∈V2X∈ V_2; the atom X(x)X(x) asserts that the monadic predicate X holds of the individual x (extensionally, that x lies in the set denoted by X). The further connectives ∨ , ⊃, ↔ , the first-order universal ∀x∀ x, and the second-order universal ∀X∀ X are defined as usual by duality. A model is a tuple ⟨I,D,E⟩ I,D,E , where D is a nonempty domain of individuals, E is a nonempty collection of admissible monadic predicates over D (the second-order domain; extensionally a family E⊆(D)E (D) of subsets), and the interpretation I assigns to each relation symbol r a binary relation I(r)⊆D×DI(r) D× D. A first-order assignment g:V→Dg V→ D maps each individual variable to a domain element, and a second-order assignment G:V2→EG V_2→ E maps each monadic predicate variable to an admissible predicate in E; g[x←d]g[x← d] and G⟨X←S⟩G X← S denote the obvious updates. Truth in a model is given recursively by ⟨I,D,E⟩,g,G I,D,E ,g,G ⊧r(x,y) r(x,y) iff I(r)(g(x),g(y)) I(r)(g(x),g(y)) ⟨I,D,E⟩,g,G I,D,E ,g,G ⊧X(x) X(x) iff G(X)holds ofg(x) G(X)\ holds of\ g(x) ⟨I,D,E⟩,g,G I,D,E ,g,G ⊧¬φ iff not ⟨I,D,E⟩,g,G⊧φ not I,D,E ,g,G ⟨I,D,E⟩,g,G I,D,E ,g,G ⊧φ∧ψ ψ iff ⟨I,D,E⟩,g,G⊧φ and ⟨I,D,E⟩,g,G⊧ψ I,D,E ,g,G and I,D,E ,g,G ψ ⟨I,D,E⟩,g,G I,D,E ,g,G ⊧∃x.φ ∃ x. iff ∃d∈D.⟨I,D,E⟩,g[x←d],G⊧φ ∃ d∈ D.\, I,D,E ,g[x← d],G ⟨I,D,E⟩,g,G I,D,E ,g,G ⊧∃X.φ ∃ X. iff ∃S∈E.⟨I,D,E⟩,g,G[X←S]⊧φ ∃ S∈ E.\, I,D,E ,g,G[X← S] A formula φ is valid iff ⟨I,D,E⟩,g,G⊧φ I,D,E ,g,G for every model, every g into D, and every G into E. When E=(D)E=P(D) (every monadic predicate is admissible) the second-order quantifier is the standard (full) one; restricting E yields the various general (Henkin-style) readings. The principle bridging the two is comprehension — that every property definable by a formula determines an admissible set; it holds by fiat when E=(D)E=P(D) but can fail once E is restricted. This is the monadic fragment: only monadic predicate variables (not relation variables) may be quantified, and a unary property of individuals is rendered directly as a monadic predicate applied to its argument. Scope. For minimality we restrict the first-order signature to binary relation symbols and omit primitive equality; unary properties are rendered directly as monadic predications X(x)X(x). Thus the formalisation covers the equality-free binary-relational fragment of MSO, which suffices for all results below. 4 Three embeddings of MSO in HOL We now present the three embeddings side by side, after fixing the preliminaries shared by all of them. 4.1 Preliminaries Preliminaries shared by all embeddings (theory MSOinHOL_preliminaries.thy, Fig. 6) declare the type D (individuals) and the type synonyms R:=R:=nat (relation symbols), V:=V:=nat (first-order variables), V2:=V_2:=nat (second-order variables), together with ℛR, ℐI, the first-order assignment type ℰ:=V⇒DE:=V D, the second-order assignment type :=V2⇒(D⇒)G:=V_2 (D ), and the two domain-restriction types :=D⇒D:=D and :=(D⇒)⇒P:=(D ) . Two variable-assignment update operators are introduced: g[x←d]g[x← d] for the first-order assignment and G⟨X←S⟩G X← S for the second-order one, each with its companion lemmata (L1–L4 and M1–M4). The set-as-predicate operations ⊑ , ⊔ , Range, Univ, into, onto are polymorphic and hence shared between both sorts. 4.2 Deep embedding The deep embedding (theory MSOinHOL_deep.thy, Fig. 1) is a single inductive datatype ℱF whose constructors mirror the grammar (1): AtmD (relational atom rd(x,y)r^d(x,y)), PrdD (monadic predication atom Xd(x)X^d(x)), NegD, AndD, the first-order ExD (∃dx.φ∃^dx. ), and the second-order ExD2 (∃2dX.φ∃^d_2X. ). The relative-truth predicate ⟨I,D,E⟩,g,G⊧dφ I,D,E ,g,G ^d is declared in mixfix syntax and defined by primitive recursion: the predication clause evaluates the monadic predicate G(X)G(X) at the individual g(x)g(x); the first-order existential ranges over the explicit domain D; the second-order existential ranges over the explicit collection E of admissible sets; the rest is standard. Validity ValD closes universally over models, over domain-respecting first-order assignments (g into D), and over domain-respecting second-order assignments (G into E). An auxiliary full-domain notion ⊧d′ ^d fixes D=D= Univ and E=E= Univ and is a convenience for nitpick; since ⊧dφ ^d implies ⊧d′φ ^d , any counterexample for ⊧d′ ^d refutes ⊧d ^d as well. Reading the clauses. The two existential clauses are the only places where the model is consulted nontrivially: each quantifies a witness over its domain (d over D, S over E) and re-evaluates under the corresponding assignment update. All remaining connectives (∨ , ⊃, ↔ , and the two universals) are definitional abbreviations, unfolded automatically through the rewrite bag DefD; the same discipline (DefS, DefM) governs the two shallow embeddings, so the three notions of validity differ only in their primitives. Figure 1: Deep embedding of MSO in HOL: the datatype ℱF with the predication atom and the two binders, the derived connectives, the relative-truth predicate RelativeTruthD, and the validity definitions ValD, ValD’. 4.3 Maximal shallow embedding The maximal shallow embedding (theory MSOinHOL_shallow.thy, Fig. 2) lifts every primitive of MSO to a λ-term abstracted over the explicit dependencies I, D, E, g, G. The type of formulae is σ:=ℐ⇒ℰ⇒σ:=I . Atoms consult the interpretation; the predication case applies the second-order assignment; the first-order existential pairs a meta-level HOL existential with a first-order assignment update; and the second-order existential pairs a meta-level HOL existential with a second-order assignment update. The pattern is identical to that of [12]; the only difference is that the formula type σ carries two assignments and two domain restrictions, because both the first-order (individual) and the second-order (set) quantifier must be accommodated. We write ⊧s ^s for the resulting validity and ⊧s′ ^s for its full-domain variant (D=D= Univ and E=E= Univ), the maximal-shallow analogues of ⊧d ^d and ⊧d′ ^d . Figure 2: Maximal shallow embedding (MSOinHOL_shallow.thy): the formula type σ, the six primitive cases (the two existentials thread g and G respectively), the derived connectives, and validity. 4.4 Minimal shallow embedding (locale-based) The maximal-shallow type carries every dependency as an explicit argument, threaded throughout because each quantifier updates an assignment in its recursive call (g[x←d]g[x← d] for ∃x∃ x, G⟨X←S⟩G X← S for ∃X∃ X). The minimal embedding avoids this: each MSO existential is encoded by HOL’s own binder over the matching variable namespace (V, V2V_2), and atoms read their variables’ denotations from the assignment (Xm(x)X^m(x) is (GGX)(ggx)(G\,X)(g\,x)), so a bound variable is a symbol looked up in the assignment rather than a witness installed into an updated one. The recursion therefore never changes II, gg, or GG; this, with the absence of any world dependency, lets us promote them to locale parameters, and the formula type reduces to bool. We package the minimal embedding as an Isabelle/HOL locale MinS [2] (theory MSOinHOL_shallow_minimal_locale.thy, Fig. 3), fixing (II,gg,GG)(I,g,G). The six primitive cases are AtmM, PrdM (predication Xm(x)X^m(x) defined as (GGX)(ggx)(G\,X)(g\,x)), NegM, AndM, the first-order binder ExM over V, and the second-order binder ExM2 over V2V_2. As the formula type is bool, relative truth and validity ValM (written ⊧m ^m) are the identity. Both binders are declared as HOL binders, so that sledgehammer treats second-order MSO goals as ordinary HOL goals: bound first- and second-order variables become HOL-level bound variables of types V and V2V_2, and the external provers reason about them directly without unfolding the deep-embedding syntax. For practical experimentation the locale is also instantiated once at the global level (theory MSOinHOL_shallow_minimal.thy, Fig. 7): three uninterpreted constants I, g, G are introduced and a global_interpretation re-issues the locale notation at the global level. The locale formulation remains the single source of all theorems; the global interpretation propagates them to the constants without proof duplication. Figure 3: The locale MinS (MSOinHOL_shallow_minimal_locale.thy) packaging the minimal shallow embedding: parameters II, gg, GG; the six primitive cases including the HOL binders ExM (over V) and ExM2 (over V2V_2); the derived connectives; and validity. Maximal vs. minimal: the trade-off. The two shallow embeddings encode the same object logic but package the semantic parameters oppositely. The maximal embedding keeps the interpretation and both assignments explicit in each translated formula (type σ): the parameters are under direct control and the translation lines up term-for-term with the deep embedding, which makes it the natural faithfulness bridge (FaithfulSD) and the place to express the full-domain standard readings ⊧s ^s, ⊧s′ ^s ; the price is weight, as every subterm threads I,D,E,g,GI,D,E,g,G. The minimal embedding hides those parameters in the locale MinS, so a translated formula becomes an ordinary HOL proposition of type bool with each MSO binder a native HOL binder: sledgehammer and nitpick act on it directly, which makes it the convenient vehicle for downstream reasoning and for comparing classes of interpretations — general vs. standard (§7) — at the cost of leaving the semantic parameters implicit. 5 Two-sorted substitution machinery Substitution lemmas are needed for the deep↔ -shallow faithfulness proof, to handle the two existential-quantifier cases. Since MSO has two variable namespaces, we develop two parallel substitution apparatuses, Part A (first-order) and Part B (second-order), in theory MSOinHOL_deep_subst_lemma.thy (Figs. 9–11). We use named variables and explicit capture-avoiding substitution rather than a nominal or de Bruijn infrastructure, keeping the two namespaces and their mutual transparency visible in the formal text. The two apparatuses. Each part provides the standard components — free/bound/fresh predicates, a variable-for-variable substitution Subst (written [x←z](φ)[x←z]( ); second-order Subst2), a substitutability predicate, the SubstitutionLemma (resp. SubstitutionLemma2, whose semantic side is the update G⟨X←GZ⟩G X← G\,Z ), and an α-renaming ren_for_subst composing into the safe substitution ren_subst, written [x←rz](φ)[x\! _r\!z]( ). The size-based induction principles SInduct and QInduct recurse on both binders. The outcomes used downstream are L27/N27 (safe substitution commutes with assignment update) and L29/N29, which re-express a deep existential as a HOL existential over a fresh symbol — exactly the equation the minimal translation needs. Transparency across namespaces. A binder of one sort contributes nothing to the machinery of the other: binding no variable of that namespace, it descends through every predicate, substitution, renaming, and induction by a single uniform clause, structurally identical to the negation clause and dispatched by the same auto/simp. This holds twice over — the second-order binder ExD2 is transparent for Part A and the first-order ExD for Part B — the only genuinely new leaf being the predication atom X(x)X(x), which contributes a free first-order occurrence (x) to Part A and a free second-order one (X) to Part B. The α-renaming is what keeps substitution sound across a binder: replacing x by z in ∃dz.rd(x,z)∃^dz.\,r^d(x,z) would capture the free z, which ren_subst prevents by first renaming the bound z to a fresh symbol. We additionally isolate the single-binder semantic core as rename_eval/rename_eval2 (theory MSOinHOL_subst_extras.thy, Fig. 12). 6 Faithfulness, automated An embedding is faithful when validity transfers in both directions — a formula is valid in MSO exactly when its HOL translation is — so the embedding neither loses nor invents theorems; we establish this, automatically, for all three. Two mappings translate deep formulae into shallow ones (theory MSOinHOL_faithfulness_locale.thy, Fig. 4): DpToShS (deep to maximal-shallow), written ⟦⋅⟧ · , and DpToShM (deep to minimal-shallow), written (|⋅|)(\! · \!). The first recurses transparently through every primitive, since both source and target use named-variable binders for both sorts. The second, declared inside the locale MinS, bridges the two named-variable binders of the deep embedding to the two HOL binders of the minimal embedding: its first-order existential clause inserts a first-order safe substitution [v←rd](φ)[v\! _r\!d]( ), and its second-order existential clause inserts a second-order safe substitution [V←r2D](φ)[V\! _r2\!D]( ). Pointwise and validity-level theorems. The deep↔ -shallow correspondence FaithfulSDlem is derived by a single induction on φ with auto simp: DefS DefD; its validity-level form FaithfulSD – the statement for closed validity rather than for a fixed model and assignment – then follows by unfolding the two validity definitions ValD_def and ValS_def. The deep↔ -shallow correspondence is first shown pointwise, FaithfulMDlem, by a single induct with rule QInduct: simp add: DefD DefM discharges the propositional and atomic cases, and the two existential cases are closed by blast after the safe-substitution lemmata L27 and N27 rewrite the translated binders. As the minimal validity ValM is the identity, FaithfulMD coincides with FaithfulMDlem, and FaithfulMS follows by composition with FaithfulSDlem. Faithfulness across all locale interpretations. The locale form admits the all-interpretations theorem FaithfulMS_all: a formula holds in the minimal embedding under every interpretation (II,gg,GG)(I,g,G) of MinS iff it holds, in the deep embedding, in every model whose first- and second-order domains are exactly the ranges of the assignments, (∀IIggGG.⊧m(|φ|))=(∀IgG.⟨I,Rangeg,RangeG⟩,g,G⊧dφ). (∀ I\,g\,G.\ ^m(\! \!) )\;=\; (∀ I\,g\,G.\ I,Range\,g,Range\,G ,g,G ^d ). The proof is a single simp with FaithfulMD. The forward direction toward full deep validity, Deep_to_MinS, holds outright: a deep-valid formula transfers to every minimal interpretation. The converse is exactly the surjectivity problem — whether the countable assignment ranges can be made to exhaust the full second-order domain — to which we now turn. Figure 4: Faithfulness: the translations ⟦⋅⟧ · and (|⋅|)(\! · \!) (the latter bridging both binders via the two safe substitutions), the deep↔ -shallow theorems, the locale-based deep↔ -shallow correspondences, the all-interpretations theorem FaithfulMS_all, and the one-directional bridge Deep_to_MinS. What FaithfulMS_all buys. FaithfulMS_all makes the minimal embedding a proof device, not merely a definitional convenience. To establish a deep validity one discharges the corresponding goal in the minimal embedding — a plain HOL formula with two ordinary binders, on which sledgehammer and auto operate directly — and the theorem transports the result to the deep syntax over the range-determined model class; conversely, any nitpick countermodel refutes the deep formula. The only gap is the passage from the range-determined model class to the full general (Henkin-style) class, which §7 closes; for the standard reading it shows that unrestricted all-interpretations faithfulness is impossible, while an elementary-substructure restriction recovers it exactly. 7 The surjectivity problem, second-order In the minimal-shallow embedding the first-order binder ranges over the namespace V=V=nat through gg:V→Dgg V→ D, with effective range RangeggRange\,g; the second-order binder ranges over V2=V_2=nat through GG:V2→(D⇒)G V_2→(D ), with effective range RangeGGRange\,G. Both ranges are countable, whereas the deep embedding lets the existentials range over the full domains D and E, so faithfulness against the full domains does not follow from FaithfulMD. By FaithfulMS_all the missing converse is precisely (∀IgG.⟨I,Rangeg,RangeG⟩,g,G⊧dφ)⟹⊧dφ. (∀ I\,g\,G.\ I,Range\,g,Range\,G ,g,G ^d )\ \ ^d . The decisive observation is that the general validity ⊧d ^d imposes no closure on the admissible collection E: it quantifies over arbitrary families with GEG\ into\ E. That is exactly the general (Henkin-style) reading of MSO,22 2 The reading ⊧d ^d is the class of structures ⟨I,D,E⟩ I,D,E with an arbitrary admissible family E⊆(D)E (D) and no closure condition; terminology for it is not uniform. Shapiro [20] calls these Henkin models, reserving faithful Henkin model for one that additionally satisfies comprehension and choice, and full model for the standard case E=(D)E=P(D). Henkin [17], Vänänen [22], and Manzano [18] instead call the comprehension-closed structures Henkin models and the unrestricted ones general models. We write “general (Henkin-style)” for ⊧d ^d to stay neutral: it is Shapiro’s Henkin class and Vänänen’s general class. On either convention the levels nest as full/standard ⊆ comprehension-closed (faithful Henkin/Henkin) ⊆ general, with ⊧d ^d the widest; the diagonal comprehension instance separates ⊧d ^d from the comprehension-closed level, while the categoricity phenomenon separates that level from the full one. Via the reduction of this semantics to many-sorted first-order logic (Shapiro [20, Thm. 3.5]; Manzano [18]), ⊧d ^d inherits the downward Löwenheim–Skolem theorem directly. which is nothing but two-sorted first-order logic over the structure with individuals as one sort, the admissible sets as a second sort, the relation symbols as binary relations on the first sort, and a membership relation d∈S⇔S(d)d∈ S S(d) between the sorts. First-order logic has the downward Löwenheim–Skolem property; the apparent “second-order” difficulty is an artefact of conflating ⊧d ^d with the standard reading ⊧d′ ^d treated below. The converse (range-relative ⇒ deep validity) holds, for the general reading. Together with Deep_to_MinS, this gives the following exact characterisation of range-relative validity. Theorem 7.1 For every formula φ , range-relative validity coincides with general (Henkin-style) deep validity: (∀IgG.⟨I,Rangeg,RangeG⟩,g,G⊧dφ)⟺⊧dφ. (∀ I\,g\,G.\ I,Range\,g,Range\,G ,g,G ^d ) ^d . Equivalently, via FaithfulMS_all, the minimal-shallow embedding is faithful exactly to general (Henkin-style) MSO validity. The proof (App. 0.A) is a two-sorted downward Löwenheim–Skolem construction. From a countermodel one extracts a countable elementary sub-model — one satisfying exactly the same formulae — containing the assignment ranges by the Tarski–Vaught test (a witness-reflection criterion that guarantees elementarity), drawing set-witnesses honestly from E — so that no comprehension is assumed and the sub-model stays inside the general class — and then reindexes the countably many variables to surject onto the countable sub-domains while fixing the finitely many free variables of φ , using a coincidence lemma. The second-order domain E is never replaced by a powerset; being “comprehension-closed” is a property the hull enjoys, not a hypothesis it requires. Unrestricted minimal interpretations do not capture the standard reading. No Löwenheim–Skolem argument can strengthen this to the standard validity ⊧d′ ^d (where E=(D)E=P(D)), because the two notions genuinely differ. Writing ⊧dr ^d_r for range-relative validity — the left-hand side of Theorem 7.1, there identified with ⊧d ^d — we have ⊧dr=⊧d⊊⊧d′. ^d_r\;=\; ^d\; \; ^d . The inclusion ⊧d⊆⊧d′ ^d ^d is immediate – the standard model is itself one of the general models quantified over by ⊧d ^d, which is the content of the lemma we name Val – while its strictness is witnessed by comprehension: the instance ∃X.∀x.(X(x)↔P(x,x))∃ X.\,∀ x.\,(X(x) P(x,x)) is ⊧d′ ^d -valid (comprehension_atom) but not ⊧d ^d-valid, as the nitpick countermodels of §8, over a restricted E that omits the diagonal set d:P(d,d)\d:P(d,d)\, show. In the three-level hierarchy of Footnote 2, this instance separates the general reading ⊧d ^d from the comprehension-closed Henkin reading, and hence a fortiori from the full reading ⊧d′ ^d ; the residual gap, between the Henkin and the full reading, reflects the familiar categoricity phenomenon for second-order logic — the full reading pinning models down up to isomorphism. We do not formalise this second gap; our machine-checked results concern the embeddings, their faithfulness, and the Löwenheim–Skolem connection between the range-relative and general readings, while the separation ⊧d⊊⊧d′ ^d ^d from the standard reading is witnessed here by the simpler diagonal comprehension instance above. The analysis thus resolves into a dichotomy: the converse is a theorem for the general (Henkin-style) reading and a provable non-reduction for the standard reading. The supplementary theories MSOinHOL_lowenheim_skolem_lemmas.thy and MSOinHOL_lowenheim_skolem.thy carry this out — the coincidence lemma coincidence, the surjective reindexing reindex, the assembled converse RangeValid_imp_ValD (with corollaries RangeValid_iff_ValD and Faithful_to_Henkin), the negative Standard_strictly_stronger with its explicit diagonal countermodel, and the two-sorted elementary-substructure hull ls_hull, a countable Tarski–Vaught hull skolem_hull whose truth-preservation lemma truth_pres drives the two-sorted construction — and, built on the same hull, the elementary-substructure relation ElementarySubstructure, the first-class downward Löwenheim–Skolem theorem DownwardLowenheimSkolem, and the standard-reading characterisation Deep’_to_MinS. All are complete structured proofs, machine-checked under Isabelle2025-2; the construction is given in App. 0.A. The standard reading, captured exactly by elementary interpretations. The non-reduction says only that no range-relative — equivalently, all-interpretations — faithfulness can reach ⊧d′ ^d . It does not say the standard reading escapes the minimal embedding: it does not. Writing ⟨I′,D′,E′⟩⊆E⟨I,D,E⟩ I ,D ,E _\!E I,D,E for the two-sorted elementary substructure relation ElementarySubstructure (D′⊑D D, E′⊑E E, and the two models satisfy the same formulae under every assignment landing in the smaller pair), the development now isolates the Tarski–Vaught hull as a first-class downward Löwenheim–Skolem theorem DownwardLowenheimSkolem: every countable nonempty seed sub-pair of a model extends to a countable elementary substructure. Using it, the strongest faithfulness theorem Deep’_to_MinS characterises the standard reading exactly, ⊧d′φ⟺∀IIggGG.⟨I,Rangegg,RangeGG⟩⊆E⟨I,Univ,Univ⟩⟶⊧m(|φ|), ^d \ \ ∀ I\,g\,G.\\ I,Range\,g,Range\,G _\!E I,Univ,Univ \ \ ^m(\! \!), where ⟨II,Univ,Univ⟩ I,Univ,Univ is the full model (E=(D)E=P(D)). Both readings of MSO are therefore recovered from the minimal embedding, differing only in the admissible interpretations: ⊧d ^d quantifies over all minimal interpretations (Theorem 7.1, via FaithfulMS_all), whereas ⊧d′ ^d quantifies over the elementary ones — those whose countable range model is an elementary substructure of the full model. The strict inclusion ⊧d⊊⊧d′ ^d ^d is exactly the statement that this elementary restriction cannot be dropped, the diagonal comprehension instance witnessing it. Concretely, the nitpick countermodels to the closure schemas in the minimal embedding (§8) are necessarily non-elementary interpretations: their countable range omits a set the schema needs, so they refute it; on the elementary interpretations the same schemas become provable, in agreement with their ⊧d′ ^d -validity. (They are thus not genuine counterexamples to the standard reading, but artefacts of admitting non-elementary ranges; under the elementary-substructure restriction (the locale MinS_ES_Univ) each would be a theorem.) A recursion-theoretic strengthening. The non-reduction just established is model-theoretic: the failure of downward Löwenheim–Skolem shows that the full MSO models — those with E=(D)E=P(D) — do not form an elementary class. A complementary, recursion-theoretic obstruction is that standard validity ⊧d′ ^d is not recursively enumerable — a classical consequence of the expressive strength of standard second-order logic (cf. Shapiro [20], Vänänen [22]), which we do not formalise here — so it is the consequence set of no recursively axiomatisable first-order theory. This non-enumerability reflects quantification over all interpretations of the relation symbols, not the standard reading as such: restricting to a fixed structure or class of structures — (ℕ,<)(N,<), the infinite binary tree, or finite words and trees — makes standard MSO decidable, hence complete and enumerable [14, 21, 16]. 8 Experiments We illustrate the development with two test files. The core file MSOinHOL_experiments.thy (Fig. 5) collects tautologies, comprehension, and nitpick disproofs; the larger file MSOinHOL_experiments_classic.thy replicates a suite of classical MSO landmarks across all three embeddings (§8.1). Propositional tautologies (proved in all three embeddings with the d/s/m discipline), first-order tautologies such as (∀x.P(x,x))⊃(∃x.P(x,x))(∀ x.\,P(x,x))⊃(∃ x.\,P(x,x)), and the predication tautology ∀x.(X(x)⊃X(x))∀ x.\,(X(x)⊃ X(x)) are dispatched by simp or auto after unfolding DefD, DefS, or DefM. Monadic comprehension. The principal second-order validity we verify is monadic comprehension, stated over the full second-order domain (⊧d′ ^d , E=E= Univ). In its general form it is a schema, parametric in an arbitrary formula φ in which the comprehension variable X does not occur free: ⊧∃d′X.∀x.(X(x)↔φ). ^d \ ∃ X.\,∀ x.\,(X(x) ). The witnessing set is exactly the property defined by φ , namely the HOL predicate λd.⟨I,,⟩,g[x←d],G⊧dφλ d.\, I, Univ, Univ ,g[x←d],G ^d ; it always lies in E because E=(D)E=P(D) in the standard semantics, and the side condition on X lets the second-order irrelevance lemma discharge the X-slot inside φ . We record this as the theorem comprehension_schema (supplementary theory MSOinHOL_comprehension.thy, Fig. 13); the two instances proved directly in MSOinHOL_experiments.thy — the set of P-self-related individuals, ∃X.∀x.(X(x)↔P(x,x))∃ X.\,∀ x.\,(X(x) P(x,x)), with witness λd.Pddλ d.\,P\,d\,d, and the universally-true predicate ∃X.∀x.X(x)∃ X.\,∀ x.\,X(x), with witness λd.λ d.\,True — are its corollaries. No second-order search is required, because the comprehension term is itself an ordinary HOL predicate. Disproofs by nitpick. nitpick finds finite countermodels for the invalid schemata considered here; these are exploratory searches, terminated with oops rather than stored as theorems. “Every monadic predicate holds somewhere”, ∀X.∃x.X(x)∀ X.\,∃ x.\,X(x), fails by the empty predicate; the comprehension instance asking for a predicate that both holds and fails of every individual, ∃X.∀x.(X(x)∧¬X(x))∃ X.\,∀ x.\,(X(x) X(x)), is unsatisfiable hence invalid; and symmetry of P, ∀x∀y.(P(x,y)⊃P(y,x))∀ x\,∀ y.\,(P(x,y)⊃ P(y,x)), fails by a two-element model. Each disproof uses the full-domain relation ⊧d′ ^d . Figure 5: Experiments: propositional and first-order tautologies in all three embeddings, the predication tautology, monadic comprehension and the universal-predicate validity over the full second-order domain, and nitpick disproofs of “every predicate holds somewhere”, a self-contradictory predicate, and symmetry of P. 8.1 Classical MSO landmarks across the three embeddings A second, larger experiment file (MSOinHOL_experiments_classic.thy, Fig. 14) revisits a sequence of textbook MSO constructions and runs each one through all three embeddings. The point is not the individual validities — they are folklore — but the pattern of their truth values across the five readings ⊧d ^d, ⊧d′ ^d , ⊧s ^s, ⊧s′ ^s , ⊧m ^m, which is the operational face of the standard-vs-general dichotomy of §7. Table 1 collects the outcomes. Table 1: Classical MSO landmarks across the five readings. In the full-domain columns ⊧d′,⊧s′ ^d , ^s (E=E= Univ) and the minimal column ⊧m ^m, ✓ is a validity proof (an explicit second-order witness for ⊧d′/⊧s′ ^d / ^s ), × a nitpick-found countermodel, and “–” a case not separately tested (failing as complement/intersection do). The general readings ⊧d,⊧s ^d, ^s are not tested independently: they coincide with ⊧m ^m by FaithfulSD (⊧s=⊧d ^s= ^d) and Theorem 7.1 (⊧d ^d is the minimal embedding over all interpretations); the full readings likewise agree, ⊧d′=⊧s′ ^d = ^s . Schema (and witness, where valid) ⊧d ^d ⊧d′ ^d ⊧s ^s ⊧s′ ^s ⊧m ^m Complement λd.¬S(d)λ d.\, S(d) × ✓ × ✓ × Intersection λd.S1(d)∧S2(d)λ d.\,S_1(d) S_2(d) × ✓ × ✓ × Union λd.S1(d)∨S2(d)λ d.\,S_1(d) S_2(d) – ✓ – ✓ – Separation λd.S(d)∧I(P)(d,d)λ d.\,S(d) I(P)(d,d) – ✓ – ✓ – P-image λd.∃e.S(e)∧I(P)(e,d)λ d.\,∃ e.\,S(e) I(P)(e,d) – ✓ – ✓ – P-preimage λd.∃e.I(P)(d,e)∧S(e)λ d.\,∃ e.\,I(P)(d,e) S(e) – ✓ – ✓ – Reachability x↝yx\! \!y × × × × × Reflexive reachability x↝x\! \!x ✓ ✓ ✓ ✓ ✓ 22-colorability × × × × × Boolean closure and graph operations. The first six rows are instances of the comprehension schema above: each asserts the set defined by a formula φ , i.e. ∃X.∀d.(X(d)↔φ(d))∃ X.\,∀ d.\,(X(d) (d)), with witness λd.φ(d)λ d.\, (d) (the predicate shown in the table). Over the full second-order domain (⊧d′/⊧s′ ^d / ^s , E=(D)E=P(D)) each witness is an ordinary HOL predicate supplied by a single exI: the Boolean cases [14, 21] use λd.¬S(d)λ d.\, S(d), λd.S1(d)∧S2(d)λ d.\,S_1(d) S_2(d), λd.S1(d)∨S2(d)λ d.\,S_1(d) S_2(d), and the monadic graph operations [16] the witnesses shown in the table. After unfolding DefD (resp. DefS) and β-reducing, the deep and maximal-shallow goals are HOL-identical, so the two proof scripts are line-for-line the same — the d/s alignment made visible on non-trivial second-order content. In the minimal embedding ∃2m∃^m_2 ranges over V2=V_2=nat through GG, so the required predicate need not lie in RangeGGRange\,G and nitpick refutes complement and intersection (the remaining four fail for the same reason). Reachability and colorability. Reachability and 22-colorability are genuinely invalid in MSO, independently of the standard/general choice, and fail in all columns: reachability [3] — “if Z contains x and is closed under P-successors then Z contains y” — has a nitpick countermodel with x,yx,y P-disconnected; its reflexive variant (conclusion Z(x)Z(x)) follows from the first conjunct alone, needs no witness, and so survives even the minimal embedding; 22-colorability [21] fails on an odd cycle (K3K_3). The overall pattern — closure rows valid under the full readings ⊧d′/⊧s′ ^d / ^s but refuted under the general ⊧d/⊧s/⊧m ^d/ ^s/ ^m, reachability and 22-colorability uniformly refuted — is exactly the inclusion ⊧d⊊⊧d′ ^d ^d of §7 read off machine-checked outcomes: faithful to the general (Henkin-style) reading, the minimal embedding refutes precisely the principles that separate the standard reading from the general one, while reflexive reachability, needing no set witness, holds across the board. Locale-based transfer. A short demonstration (theory MSOinHOL_experiments_locale.thy, Fig. 15) proves a schema purely from minimal-shallow definitions, inside the locale, and transfers it to the range-relative deep embedding by a single application of MinS_to_Deep, 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. 9 Conclusion MSOinHOL demonstrates that the deep-and-shallow methodology of [12] scales to a setting with two binders over different sorts. The new ingredients are a two-sorted substitution apparatus, in which each binder is transparent for the other namespace, and a locale-based minimal embedding with two HOL binders and an all-interpretations faithfulness theorem. The powerset character of the second-order domain turns the surjectivity problem into a clean dichotomy. On one side, range-relative validity coincides with the general (Henkin-style) reading of MSO — a two-sorted Löwenheim–Skolem theorem (§7). On the other, the standard reading validates strictly more formulas, yet it too is captured exactly by the minimal embedding once one restricts to elementary interpretations (Deep’_to_MinS). The two readings are thus one and the same translation, differing only in the class of interpretations over which validity is quantified. The whole construction — coincidence, the two-sorted elementary-substructure hull, reindexing, the assembled converse, and the negative result — is machine-checked. A suite of classical MSO landmarks — Boolean closure, graph operations, reachability, 22-colorability — replicated across the three embeddings turns this dichotomy into a table of validity proofs, nitpick-found countermodels, and entailed cases: the closure principles are valid under the full second-order domain and refuted by the general minimal embedding. The ingredients are individually classical: downward Löwenheim–Skolem has been formalised in Isabelle for first-order logic [13]; the distinction between the standard and the general (Henkin-style) reading of second-order semantics is textbook [22]; and the general reading is known to be, in effect, a two-sorted first-order theory [18]. What is new here, to our knowledge, is to carry a mechanised downward Löwenheim–Skolem theorem all the way through to monadic second-order validity. The construction is a two-sorted elementary-substructure argument that, at each step, takes the set it needs as a witness from the model’s own admissible collection E rather than forming it as an arbitrary subset — and that is exactly what keeps the result inside the general (Henkin-style) class, where such sets need not exist in advance. Use in teaching. Beyond its metatheoretic interest, the development doubles as teaching material for logic at the graduate and even undergraduate level. Because the shallow embeddings turn MSO formulae into ordinary Isabelle/HOL goals, the precise difference between the standard and the general (Henkin-style) reading — and its consequences for MSO — becomes something students can explore hands-on and around the clock, through interactive proof and with sledgehammer and nitpick. A principle that holds under the full second-order domain yet fails in the minimal, range-restricted embedding makes the standard-vs-general gap immediately tangible: a machine-checked proof in one column and an explicit countermodel in another. Availability. The full Isabelle/HOL development is published as the Archive of Formal Proofs entry MSOinHOL [6]: seventeen theory files (the ten core theories together with seven supplementary ones — subst_extras, comprehension, experiments_classic, the elementary minimal interpretation shallow_minimal_elementary and its experiments experiments_classic_elementary, and the two-sorted Löwenheim–Skolem development split into lowenheim_skolem_lemmas and lowenheim_skolem), loaded in dependency order by the session ROOT; the published entry adds one further experiments theory (experiments_extra) not required for the results reported here. The development has been checked in Isabelle2025-2 on a MacBook Air (Apple M3, 16 GB). An extended version of this paper, with the full two-sorted Löwenheim–Skolem proof and the rendered Isabelle/HOL theory sources as appendices, is available on arXiv [7]. Disclosure on the use of generative AI. The authors used generative AI assistants (Anthropic’s Claude family of models) to draft and shorten prose, to propose and shorten some proofs (in particular parts of the two-sorted Löwenheim–Skolem construction), and to maintain cross-references between the LaTeX source and the Isabelle/HOL files. The mathematical content, the theory development, and the design choices are the authors’; all text and proofs in the final manuscript have been verified by the authors, who take full responsibility for the content. References [1] Ayari, A., Basin, D.A.: Bounded model construction for monadic second-order logics. In: Computer Aided Verification (CAV 2000). Lecture Notes in Computer Science, vol. 1855, p. 99–112. Springer (2000). https://doi.org/10.1007/10722167_11 [2] Ballarin, C.: Locales: A module system for mathematical theories. Journal of Automated Reasoning 52(2), 123–153 (2014). https://doi.org/10.1007/s10817-013-9284-7 [3] Basin, D.A., Klarlund, N.: Hardware verification using monadic second-order logic. In: Computer Aided Verification (CAV 1995). Lecture Notes in Computer Science, vol. 939, p. 31–41. Springer (1995). https://doi.org/10.1007/3-540-60045-0_38 [4] Basin, D.A., Klarlund, N.: Automata based symbolic reasoning in hardware verification. Formal Methods in System Design 13(3), 255–288 (1998) [5] Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. Journal of Symbolic Logic 69(4), 1027–1088 (2004). https://doi.org/10.2178/jsl/1102022211 [6] Benzmüller, C., Kirchner, D.: Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness. Archive of Formal Proofs (2026), formal proof development, https://isa-afp.org/entries/MSOinHOL.html [7] Benzmüller, C., Kirchner, D.: Monadic second-order logic in HOL: Deep and shallow with automated faithfulness (extended preprint). arXiv:2609.07345 (2026). https://doi.org/10.48550/arXiv.2609.07345, extended version, with the full Löwenheim–Skolem proof and the rendered Isabelle/HOL theory sources as appendices [8] Benzmüller, C., Kirchner, D., Pasetto, L.: Many logics, one methodology: A plea for logical pluralism in formalised reasoning. arXiv:2605.27246 (2026). https://doi.org/10.48550/arXiv.2605.27246 [9] Benzmüller, C., Parent, X., van der Torre, L.: Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artificial Intelligence 287, 103348 (2020). https://doi.org/10.1016/j.artint.2020.103348 [10] Benzmüller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. The Logic Journal of the IGPL 18(6), 881–892 (2010). https://doi.org/10.1093/jigpal/jzp080 [11] Benzmüller, C., Paulson, L.C.: Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics) 7(1), 7–20 (2013). https://doi.org/10.1007/s11787-012-0052-y [12] Benzmüller, C.: Faithful logic embeddings in HOL — deep and shallow. In: Barrett, C., Waldmann, U. (eds.) Automated Deduction – CADE-30 – 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings. Lecture Notes in Computer Science, vol. 15943, p. 280–302. Springer (2025). https://doi.org/10.1007/978-3-031-99984-0_16 [13] Berghofer, S.: First-order logic according to Fitting. Archive of Formal Proofs (2007), formal proof development, https://isa-afp.org/entries/FOL-Fitting.html [14] Büchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 6(1–6), 66–92 (1960). https://doi.org/10.1002/malq.19600060105 [15] Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5(2), 56–68 (1940). https://doi.org/10.2307/2266170 [16] Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications, vol. 138. Cambridge University Press (2012). https://doi.org/10.1017/CBO9780511977619 [17] Henkin, L.: Completeness in the theory of types. Journal of Symbolic Logic 15(2), 81–91 (1950). https://doi.org/10.2307/2266967 [18] Manzano, M.: Extensions of First-Order Logic, Cambridge Tracts in Theoretical Computer Science, vol. 19. Cambridge University Press (1996) [19] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002). https://doi.org/10.1007/3-540-45949-9 [20] Shapiro, S.: Foundations without Foundationalism: A Case for Second-Order Logic, Oxford Logic Guides, vol. 17. Oxford University Press (1991) [21] Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, Vol. 3: Beyond Words, p. 389–455. Springer (1997). https://doi.org/10.1007/978-3-642-59126-6_7 [22] Vänänen, J.: Models and Games, Cambridge Studies in Advanced Mathematics, vol. 132. Cambridge University Press (2011) Appendix 0.A The converse of FaithfulMS_all: range vs. general (Henkin-style) validity We prove Theorem 7.1. Write ⊧drφ ^d_r for range-relative validity, ⊧rdφ≡∀IgG.⟨I,Rangeg,RangeG⟩,g,G⊧dφ. ^d_r \ ≡\ ∀ I\,g\,G.\ I,Range\,g,Range\,G ,g,G ^d . The forward direction ⊧dφ⇒⊧drφ ^d \; ^d_r is immediate (it is Deep_to_MinS: g maps into RangegRange\,g and G into RangeGRange\,G, so both are admissible). We prove the converse. Setup. A model ⟨I,D,E⟩ I,D,E is read as a two-sorted first-order structure over the fixed individual type: sort 11 is d:Dd\d:D\,d\, sort 22 is S:ES\S:E\,S\, each relation symbol r denotes the binary relation IrI\,r on sort 11, and a single membership relation is defined by mem(d,S)⇔S(d)mem(d,S) S(d). Under this reading ⟨I,D,E⟩,g,G⊧dφ I,D,E ,g,G ^d is ordinary two-sorted FO satisfaction, with ∃dx∃^dx ranging over sort 11 and ∃2dX∃^d_2X over sort 22; no closure on E is imposed. Coincidence (generalising L12/N12). By induction on φ : if g,g′g,g agree on every first-order variable free in φ and G,G′G,G agree on every second-order variable free in φ , then ⟨I,D,E⟩,g,G⊧dφ⇔⟨I,D,E⟩,g′,G′⊧dφ I,D,E ,g,G ^d I,D,E ,g ,G ^d . The binder cases use that an update g[y←d]g[y\!←\!d] (resp. G⟨Y←S⟩G Y\!←\!S ) preserves agreement on the free variables of the body. Proof Converse of Theorem 7.1, contrapositively. Suppose ⊧̸dφ ^d . Then there are I,D,E,g,GI,D,E,g,G with g into D, G into E, and ⟨I,D,E⟩,g,G⊧̸dφ I,D,E ,g,G ^d . Step 1 (downward Löwenheim–Skolem). Build sub-predicates D0⊑D_0 D and E0⊑E_0 E by closing Rangeg∪RangeGRange\,g \,G under Tarski–Vaught witnesses for the existential subformulae of φ : whenever a sort-11 existential has a witness in D for a parameter tuple drawn from the current stage, add one to D0D_0; whenever a sort-22 existential has a witness S∈ES∈ E, add that S to E0E_0. Iterating ω times yields D0,E0D_0,E_0 that are countable (the language and the two ranges are countable, and each stage adds only countably many witnesses) and elementary for φ . By the Tarski–Vaught test, ⟨I,D0,E0⟩,g,G⊧dψ⇔⟨I,D,E⟩,g,G⊧dψ I,D_0,E_0 ,g,G ^dψ I,D,E ,g,G ^dψ for every subformula ψ of φ ; in particular ⟨I,D0,E0⟩,g,G⊧̸dφ I,D_0,E_0 ,g,G ^d . The set-witnesses are honest elements of E, so E0⊑E_0 E: no comprehension is used. Step 2 (reindexing). D0D_0 and E0E_0 are countable and nonempty (they contain the nonempty ranges RangegRange\,g, RangeGRange\,G). Since V=V2=V=V_2=nat are infinite and only finitely many variables occur free in φ , choose g′g agreeing with g on the free first-order variables of φ with Rangeg′=D0Range\,g =D_0, and G′G agreeing with G on the free second-order variables with RangeG′=E0Range\,G =E_0 — fix the finitely many free slots, and let the cofinitely many remaining slots enumerate the countable target. Step 3 (conclude). By Coincidence, ⟨I,D0,E0⟩,g′,G′⊧̸dφ I,D_0,E_0 ,g ,G ^d . But D0=Rangeg′D_0=Range\,g and E0=RangeG′E_0=Range\,G , hence ⟨I,Rangeg′,RangeG′⟩,g′,G′⊧̸dφ I,Range\,g ,Range\,G ,g ,G ^d , i.e. ⊧̸drφ ^d_r , as required. Remark (the standard reading, exactly). The hull above is not only the engine of the converse; packaged with its truth-preservation it is a self-contained downward Löwenheim–Skolem theorem DownwardLowenheimSkolem — every countable nonempty seed sub-pair extends to a countable elementary substructure ⟨I,N,M⟩⊆E⟨I,D,E⟩ I,N,M _\!E I,D,E . Applied to the full model and combined with FaithfulMD and the surjective reindexing, it yields the strongest faithfulness theorem Deep’_to_MinS: ⊧d′φ ^d iff ⊧m(|φ|) ^m(\! \!) holds for every minimal interpretation whose range model is an elementary substructure of the full model (locale MinS_ES_Univ). The general reading is thus captured by the minimal embedding over all interpretations, the standard reading over the elementary ones; the gap between them is exactly the comprehension instance below. Remark (why the standard reading is excluded by Löwenheim–Skolem). The construction stays within the general class precisely because the sort-22 witnesses are taken from the given E. It cannot reach the standard reading ⊧d′ ^d (E=(D)E=P(D)) by an all-interpretations argument: by comprehension_atom the formula ∃X.∀x.(X(x)↔P(x,x))∃ X.\,∀ x.\,(X(x) P(x,x)) is ⊧d′ ^d -valid, yet a general model whose E omits the diagonal d:P(d,d)\d:P(d,d)\ refutes it, so it is not ⊧d ^d-valid. Thus ⊧d⊊⊧d′ ^d ^d , and no range-relative Löwenheim–Skolem argument can bridge the two; the elementary restriction of Deep’_to_MinS cannot be relaxed to all interpretations. A structured Isabelle development of the argument above is provided as MSOinHOL_lowenheim_skolem.thy: the coincidence and reindexing lemmas, the two-sorted hull ls_hull (with its countable Tarski–Vaught construction skolem_hull and the truth preservation truth_pres it yields), the assembled converse, the elementary-substructure relation ⊆E _\!E with DownwardLowenheimSkolem and Deep’_to_MinS, and this non-reduction remark are written out in full and machine-checked under Isabelle2025-2. Appendix 0.B Rendered Isabelle/HOL sources For completeness every theory file of the development is rendered here as a syntax-highlighted source figure (the five theories already presented in the body — the deep embedding, the maximal- and minimal-shallow embeddings, faithfulness, and the experiments — are not repeated here). Long theories are split into consecutive parts of at most eighty lines; the line-number gutter is continuous, so the parts read as one listing. The full session (file ROOT) loads all theories in dependency order. Figure 6: Theory MSOinHOL_preliminaries.thy: the shared type declarations, the two variable-assignment update operators g[x←d]g[x←d] and G⟨X←S⟩G X←S with their companion lemmata, the bounded quantifiers, and the polymorphic set-as-predicate operations. Figure 7: Theory MSOinHOL_shallow_minimal.thy: the constants-only global_interpretation of MinS that re-issues the locale notation at the level of three uninterpreted constants I,g,G. Figure 8: Theory MSOinHOL_faithfulness.thy: the locale faithfulness theorems re-issued at the constants level (deep↔ - and deep↔ -shallow correspondences, the all-interpretations theorem, and the one-directional bridge to deep validity). Figure 9: Theory MSOinHOL_deep_subst_lemma.thy (Part 1 of 3): Part A (first-order variables) — is_free, is_bound, fresh with their consequence lemmata, the irrelevance lemma L12, variable-for-variable substitution, and the size-based induction principles SInduct/QInduct. Figure 10: Theory MSOinHOL_deep_subst_lemma.thy (Part 2 of 3): the substitutability predicate, SubstitutionLemma, alphabetic renaming ren_for_subst, safe substitution ren_subst, and L17–L29 (Part A concluded); then the start of Part B (second-order variables) — is_free2, is_bound2, fresh2, and N5–N11. Figure 11: Theory MSOinHOL_deep_subst_lemma.thy (Part 3 of 3): Part B (second-order variables) concluded — the irrelevance lemma N12, second-order substitution Subst2, SubstitutionLemma2, renaming ren_for_subst2/ren_subst2, and N17–N29. Figure 12: Theory MSOinHOL_subst_extras.thy: the explicit rename-evaluation lemmas rename_eval (first-order) and rename_eval2 (second-order). Figure 13: Theory MSOinHOL_comprehension.thy: the general monadic comprehension_schema over the full second-order domain with its witness, the corollary comprehension_atom, and the discussion relating comprehension to standard vs. general (Henkin-style) semantics. Figure 14: Theory MSOinHOL_experiments_classic.thy: the classical MSO landmarks in the deep and maximal-shallow embeddings — Boolean closure (complement, intersection, union), monadic graph operations (separation, P-image, P-preimage), reachability, and 22-colorability — each with an explicit second-order witness via exI; and the minimal embedding, where Boolean closure and reachability fail by nitpick while reflexive reachability remains valid. Figure 15: Theory MSOinHOL_experiments_locale.thy: locale-based transfer to the deep embedding — the directional reading MinS_to_Deep of FaithfulMS_all, two cosmetic rewrite rules, a schema proved inside the locale, and its one-line transfer. Figure 16: Theory MSOinHOL_lowenheim_skolem_lemmas.thy (Part 1 of 4): the supporting machinery for the Löwenheim–Skolem construction — the coincidence lemma coincidence (a two-sorted generalisation of L12/N12), the padding maps padA/padB, the Skolem-witness operators wF/wS with their membership lemmas, the ω-stage operator stage, the stage-introduction lemmas fst_stage_Suc_intro/snd_stage_Suc_intro, and the padding-truth lemmas pad_truth_eq_FO/pad_truth_eq_SO. Figure 17: Theory MSOinHOL_lowenheim_skolem_lemmas.thy (Part 2 of 4): the witness-realisation lemmas wF_realizes/wS_realizes, the per-step Skolem closure skolem_step_FO/skolem_step_SO, the subset bookkeeping fst_stage_Suc_subset/snd_stage_Suc_subset, the stage monotonicity fst_stage_mono/snd_stage_mono, and the common-stage lemma common_stage_lifted. Figure 18: Theory MSOinHOL_lowenheim_skolem_lemmas.thy (Part 3 of 4): the ω-union membership lemmas wF_in_omega_union/wS_in_omega_union, the first- and second-order Tarski–Vaught closures stage_TV_FO/stage_TV_SO, the inductive countability step cntDE_step, the carriers-stay-inside lemmas fst_stage_subD/snd_stage_subE, stage-wise and ω-countability stage_countable/stage_omega_countable, and the surjective reindexing reindex_one. Figure 19: Theory MSOinHOL_lowenheim_skolem_lemmas.thy (Part 4 of 4): the conclusion of reindex_one, the surjective reindexing reindex, and the combined reindex_coincide lemma. Figure 20: Theory MSOinHOL_lowenheim_skolem.thy (Part 1 of 2): the elementary-substructure layer — the relation ElementarySubstructure (⊆E _\!E) and the locales MinS_ES/MinS_ES_Univ — range-relative validity RangeValid, the easy direction ValD_imp_RangeValid, truth preservation truth_pres for a Tarski–Vaught-closed sub-pair, the countable seed hull skolem_hull, and the first-class downward Löwenheim–Skolem theorem DownwardLowenheimSkolem. Figure 21: Theory MSOinHOL_lowenheim_skolem.thy (Part 2 of 2): the strongest faithfulness theorem Deep’_to_MinS (standard validity ⇔ minimal validity over elementary interpretations) with its corollary Faithful_to_Standard; then the earlier general-reading route, derived in one step from DownwardLowenheimSkolem — the assembled elementary-substructure hull ls_hull, the range reduction Range_reduction, the main theorem RangeValid_imp_ValD with corollaries RangeValid_iff_ValD/Faithful_to_Henkin, and the negative result Standard_strictly_stronger with its explicit diagonal countermodel. Figure 22: Theory MSOinHOL_shallow_minimal_elementary.thy: an elementary constants-only presentation of the minimal shallow embedding — four DpToShS simplification lemmas for the derived quantifiers and connectives (DpToShS_All, DpToShS_All2, DpToShS_Equiv, DpToShS_Imp), the three uninterpreted constants I, g, G, a specification establishing the existence of a global interpretation that forms a MinS_ES_Univ elementary substructure (with existence justified by Deep’_to_MinS), the corresponding global_interpretation re-issuing the locale notation at the constants level, and the inheritance lemmas FaithfulMD_ES (faithfulness under universal carriers) and ValidM_if_ValidD’ (standard validity lifts to minimal validity). Figure 23: Theory MSOinHOL_experiments_classic_elementary.thy (Part 1 of 2): additional simplification rules for the derived second-order quantifier and equivalence (ren_for_subst2_simp_All, subst2_all, free2_in_equiv, free2_in_all, free2_in_all2), the convenient variable abbreviations, and the full set of deep-embedding classical MSO landmarks — Boolean closure (complement_d, intersection_d/intersection_d’, union_d), monadic graph operations (separation_d, image_d, preimage_d), reachability (reachability_not_valid_d, reachability_reflexive_d), and 22-colorability (two_colorability_not_valid_d). Figure 24: Theory MSOinHOL_experiments_classic_elementary.thy (Part 2 of 2): the same landmarks in the maximal-shallow embedding (the deep↔ -shallow scripts are line-for-line identical because the goals are HOL-equal after unfolding), and their lifts to the elementary global interpretation — the DpToShS-normal-form lemmas (compl_m_DpToSh, inters_m_DpToSh’, intersect_m_DpToSh), the helper combinators (DpToSh_alleqI, all_m_eqI, DpToSh_simps), and the ValidM_if_ValidD’-style validity transfers (compl_m_valid, intersection_m_valid); reachability and 22-colorability remain refuted in the elementary minimal embedding as expected.