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

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 as explicit arguments; 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 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 is provably stronger, 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 further 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.

39 pages. Extended version -- with the full two-sorted Loewenheim-Skolem proof (Appendix A) and the rendered Isabelle/HOL theory sources (Appendix B) -- of a contribution accepted to a Festschrift for David Basin (Springer LNCS); the proceedings version is 19 pages. The Isabelle/HOL formalisation is published in the Archive of Formal Proofs: this https URL

Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Logic (math.LO)

arXiv:2609.07345 [cs.LO]

(or arXiv:2609.07345v1 [cs.LO] for this version)

https://doi.org/10.48550/arXiv.2609.07345 arXiv-issued DOI via DataCite (pending registration)