Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)

1 Motivation and introduction

• The approach complements MSO decision procedures for fixed fragments by embedding full and general MSO in HOL for interactive proof and metatheory.The cited algorithmic line targets decidable fragments over strings and trees.Source: §1 · p. 2
• The work extends simultaneous deep-and-shallow embeddings beyond modal logic to MSO, whose two quantifiers bind variables from different namespaces.Shallow embeddings provide access to HOL automation, while deep embeddings support metalogical reasoning about syntax and substitution.Source: §1 · p. 2
• Three embeddings are developed: a deep datatype, a maximal-shallow translation with explicit parameters, and a minimal-shallow locale that fixes them.The minimal embedding collapses the formula type to bool.Source: §1 · pp. 2–3
• A two-sorted substitution apparatus handles capture avoidance, renaming, and substitution lemmas, with each binder transparent to the other namespace.Faithfulness of the embeddings is mechanised and largely automated.Source: §1 · p. 3
• A two-sorted downward Löwenheim–Skolem theorem connects the minimal embedding's range-relative validity with general Henkin-style MSO validity.The paper contrasts this with the standard reading, which validates strictly more formulas.Source: §1 · p. 3
• The paper tests the embeddings on comprehension and classical MSO landmarks, including Boolean closure, graph operations, reachability, and 2-colorability.The introduction reports that Boolean-closure and graph schemata hold under the full second-order domain but fail in the general minimal embedding, while reachability and 2-colorability are refuted throughout.Source: §1 · p. 3

2 Classical higher-order logic

• HOL is presented as a simply typed λ-calculus over truth-value and individual base types, with Henkin semantics and denotations derived from a frame and interpretation.Isabelle/HOL mechanises a fragment sufficient for the paper's development.Source: §2 · p. 3
• The MSO second-order domain is the HOL function type D ⇒ o, so monadic sets or predicates are first-class HOL objects.Source: §2 · p. 3
• The shallow embeddings inherit HOL's functional and Boolean extensionality.The cited analysis discusses extensionality's role in fixing the class of Henkin models.Source: §2 · p. 3

3 Monadic second-order logic (MSO)

• The syntax includes binary-relation atoms, monadic-predication atoms, negation, conjunction, and existential quantifiers over individuals and monadic predicates.Disjunction, implication, equivalence, and both universal quantifiers are defined by duality.Source: §3 · p. 4
• A model consists of a nonempty individual domain D, a nonempty admissible-predicate collection E, and interpretations of binary relation symbols.The two assignments map individual variables into D and monadic predicate variables into E.Source: §3 · p. 4
• Truth is evaluated recursively, with individual existentials ranging over D and monadic existentials ranging over E.Source: §3 · p. 4
• Validity quantifies over every model and assignments; setting E = P(D) gives standard semantics, while restricting E gives general Henkin readings.Comprehension holds by fiat for E = P(D) but can fail when E is restricted.Source: §3 · p. 4
• The formalisation omits primitive equality and restricts the first-order signature to binary relations, rendering unary properties as monadic predications.The authors state that this equality-free binary-relational fragment suffices for the results below.Source: §3 · p. 4

4.1 Preliminaries

• Shared preliminaries define the individual and set domains, two assignment types with update operators, and polymorphic operations used across both sorts.First-order and second-order assignments map variables to individuals and sets, respectively.Source: §4.1 · p. 5

4.2 Deep embedding

• The deep embedding represents MSO formulas as an inductive datatype and defines truth recursively over explicit individual and set domains.Its standard reading fixes both domains to their full universes.Source: §4.2 · p. 5

4.3 Maximal shallow embedding

• The maximal-shallow embedding uses formula type σ to carry the interpretation, both domains, and both assignments explicitly through each primitive.Its existential cases update the corresponding first- or second-order assignment.Source: §4.3 · p. 6, Figure 2 · p. 7

4.4 Minimal shallow embedding (locale-based)

• The minimal embedding fixes its interpretation and assignments in locale MinS, making formulas HOL propositions with native binders for both variable sorts.The HOL binders quantify over first- and second-order variable namespaces.Source: §4.4 · p. 7, Figure 3 · p. 8

4 Three embeddings of MSO in HOL

• The three embeddings package the same logic differently: maximal-shallow keeps dependencies explicit, while minimal-shallow hides them in a locale and reduces formulas to bool.The maximal form is the direct faithfulness bridge; the minimal form supports downstream HOL reasoning with implicit parameters.Source: §4.4 · p. 8

Two-sorted substitution machinery

• The development provides parallel first- and second-order substitution apparatuses using named variables and explicit capture-avoiding substitution.This keeps the two namespaces and their mutual transparency visible in the formalisation.Source: §5 · p. 9
• Each apparatus includes free, bound, and fresh predicates, substitution and substitutability, a substitution lemma, α-renaming, and safe substitution.The downstream lemmas show safe substitution commuting with assignment update and characterize existential quantification under surjective assignments.Source: §5 · p. 9
• A binder is transparent to machinery for the other namespace, while α-renaming prevents capture when substitution crosses a binder.For example, replacing x by z under a binder for z requires renaming that bound variable first.Source: §5 · p. 9

6 Faithfulness, automated

• Faithfulness is established in both directions, so translation preserves validity without losing or inventing theorems.The deep-to-maximal correspondence follows by induction; the deep-to-minimal proof uses safe-substitution lemmas for the existential cases.Source: §6 · pp. 9–10
• A formula holds under every minimal-locale interpretation exactly when it holds in deep models whose two domains are the assignment ranges.This all-interpretations result is proved using pointwise faithfulness.Source: §6 · p. 10
• Minimal-embedding HOL goals support direct use of sledgehammer and auto, and results transfer to deep syntax over the range-determined model class.A genuine countermodel to the minimal goal also refutes the deep formula over that class.Source: §6 · p. 10

7 The surjectivity problem, second-order

• The obstacle is that minimal-shallow assignments have countable ranges, while deep second-order quantifiers range over the full domains.Thus faithfulness against the full domains does not follow directly from the all-interpretations theorem.Source: §7 · pp. 10–11
• Range-relative validity coincides with general (Henkin-style) deep validity, making the minimal-shallow embedding faithful exactly to that reading.The equivalence is established for every formula.Source: §7 · p. 12
• A two-sorted downward Löwenheim–Skolem construction extracts a countable elementary submodel containing the assignment ranges, then reindexes variables to cover its domains.Set-witnesses remain in the admissible collection E; the construction neither assumes nor produces comprehension closure.Source: §7 · p. 12
• General validity is strictly weaker than standard validity: the diagonal comprehension instance is standard-valid but fails in a general model omitting its diagonal set.The general reading allows arbitrary admissible families E, without a closure condition.Source: §7 · pp. 11, 13
• The standard reading is also recovered from the minimal embedding by admitting only interpretations whose countable range model is elementary in the full model.The development proves that every countable nonempty seed sub-pair extends to a countable elementary substructure.Source: §7 · pp. 13–14
• The paper also reports that standard validity is not recursively enumerable, but does not formalise this classical result.The stated non-enumerability requires the standard reading and quantification over all interpretations of relation symbols.Source: §7 · p. 14

8 Experiments

• The comprehension schema is verified over the full second-order domain, where its witnessing predicate is admitted and can be written directly as a HOL predicate.The experiments also use nitpick to find finite countermodels for three invalid schemata, as exploratory results rather than stored theorems.Source: §8 · pp. 14–15, Figure 5 · p. 16

8.1 Classical MSO landmarks across the three embeddings

• The larger experiment file compares landmark truth values across five readings to display the standard-versus-general semantic dichotomy.The general readings coincide with the minimal reading, and the full readings coincide with each other.Source: §8.1 · p. 15, Table 1 · p. 17
• The six Boolean-closure and monadic graph-operation schemata hold over the full second-order domain, with each witness supplied by a single HOL existential introduction.After unfolding the deep and maximal-shallow definitions and beta-reducing, their proof scripts are structurally identical.Source: §8.1 · p. 15
• The minimal embedding refutes the Boolean-closure and graph-operation schemata because the required predicate may fall outside the range of its second-order assignment.Nitpick finds potential countermodels; the strict separation between general and standard validity is separately mechanised.Source: §8.1 · p. 15
• Reachability and 2-colorability fail across all readings, whereas reflexive reachability remains valid even in the minimal embedding.The reachability countermodel uses P-disconnected individuals; 2-colorability fails on a graph with a P-self-loop.Source: §8.1 · pp. 15–16
• A schema proved from minimal-shallow definitions inside the locale transfers to range-relative deep validity with one application of MinS to Deep.Source: §8.1 · p. 16

• The development shows that deep-and-shallow embedding scales to MSO with two binders over different sorts.Its new ingredients include two-sorted substitution and a locale-based minimal embedding with an all-interpretations faithfulness theorem.Source: §9 · p. 17
• A mechanised two-sorted downward Löwenheim–Skolem theorem identifies range-relative validity with the general Henkin-style reading of MSO.The construction takes set witnesses from the model’s admissible collection E.Source: §9 · p. 17
• The standard reading validates strictly more formulas than the general reading, but is captured by the minimal embedding over elementary interpretations.The general reading instead uses all interpretations.Source: §9 · p. 17
• The development is presented as teaching material for exploring the standard/general distinction with Isabelle/HOL proof automation and finite-countermodel search.Source: §9 · p. 18
• The full development is available as the Archive of Formal Proofs entry MSOinHOL and was checked in Isabelle2025-2.Source: §9 · p. 18

A The converse of FaithfulMS all: range vs. general (Henkin-style) validity

• The setup treats MSO as two-sorted first-order satisfaction, with individuals and admissible predicates as separate sorts and no closure imposed on E.Source: A The converse of FaithfulMS all:… · p. 20
• Coincidence transfers the counterexample to those reindexed assignments, whose ranges now define the model’s two domains.This establishes the converse direction for range-relative validity.Source: A The converse of FaithfulMS all:… · p. 20
• From a counterexample to deep validity, the construction closes the assignment ranges under first- and second-order existential witnesses to obtain countable subdomains.The set witnesses come from E itself, so the construction stays within the general class and uses no comprehension.Source: A The converse of FaithfulMS all:… · p. 20
• Reindexing assignments makes their ranges equal to the countable subdomains while preserving values on the formula’s free variables.The construction relies on the two variable namespaces being infinite and only finitely many variables occurring free in the formula.Source: A The converse of FaithfulMS all:… · p. 20
• Together with the downward Löwenheim–Skolem result, the construction makes general validity coincide with the minimal embedding over all interpretations.Every countable nonempty seed sub-pair extends to a countable elementary substructure; for the standard reading, the minimal embedding instead ranges over elementary interpretations of the full model.Source: A The converse of FaithfulMS all:… · pp. 20–21

Remark (why the standard reading is excluded by L¨owenheim–

• The diagonal comprehension instance is valid under full semantics but can fail in a general model whose E omits the diagonal predicate.Thus range-relative validity cannot bridge general and standard validity, and the elementary restriction cannot be dropped.Source: Remark (why the standard reading is… · p. 21

• Long theory listings are split into consecutive parts of at most eighty lines, with continuous line numbering, and loaded in dependency order by the full session.Source: B Rendered Isabelle/HOL sources · p. 21
• The preliminaries define shared types and two assignment-update operators, with companion lemmas and bounded quantifiers.Source: Figure 6 · p. 22
• The sources also include faithfulness and classical-landmark experiments, plus transfer to the minimal embedding’s elementary interpretations.Source: Figure 8 · p. 23, Figure 14 · p. 28, Figure 15 · p. 29
• The substitution listings cover first- and second-order variables, including substitution lemmas and explicit rename-evaluation lemmas.Source: Figure 9 · p. 24, Figure 10 · p. 25, Figure 11 · p. 26
• The Löwenheim–Skolem listings develop the countable construction through witness closure, stage lemmas, and reindexing.Source: Figure 16 · p. 30, Figure 17 · p. 31, Figure 18 · p. 32
• The minimal elementary presentation establishes a global interpretation and validity-transfer lemmas; the corresponding experiments leave reachability and 2-colorability as open goals there.Source: Figure 22 · p. 36, Figure 24 · p. 38