{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2609.07345",
  "author_total": 2,
  "authors": [
    {
      "name": "Christoph Benzmueller"
    },
    {
      "name": "Daniel Kirchner"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/7561gh0gjjn13.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2609.07345",
  "fulltext_url": null,
  "id": "7561gh0gjjn13",
  "issns": [],
  "landing_url": "https://arxiv.org/abs/2609.07345",
  "language": null,
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "http://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "cs.AI"
    ],
    [
      "arxiv",
      "cs.LO"
    ],
    [
      "arxiv",
      "math.LO"
    ],
    [
      "openalex",
      "1702|Logic, programming, and type systems"
    ]
  ],
  "openalex": "W7211990927",
  "pdf_url": "https://arxiv.org/pdf/2609.07345",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-21",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/7561gh0gjjn13.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:23:43Z",
      "native_id": "2609.07345",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2609.07345"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "arxiv:math.LO",
      "subfield": "logic-foundations"
    }
  ],
  "title": "Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)",
  "title_text": "Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)",
  "type": "preprint",
  "updated_at": "2026-10-30T12:23:43Z",
  "url": "https://research.draconitic.com/paper/7561gh0gjjn13",
  "venue": "arXiv",
  "versions": []
}