Metraipolis › archive › dc_be2cda561cfb

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

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.07345
License (as archived): CC0-1.0
Archived: 2026-10-16T15:02:15.947Z
SHA-256 of the archived text: 8c3176afd262a79625f582e1d4be324814352e456b5c709e0ddbd01c09382100
Stable URL of this page: https://metraipolis.com/documento/dc_be2cda561cfb

How to cite

Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint) — arXiv:2609.07345 — arXiv (en), https://arxiv.org/abs/2609.07345 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_be2cda561cfb (Metraipolis archive dc_be2cda561cfb, sha256 8c3176afd262a79625f582e1d4be324814352e456b5c709e0ddbd01c09382100)

BibTeX

@misc{dcbe2cda561cfb,
  title = {Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint) — arXiv:2609.07345},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.07345},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_be2cda561cfb; sha256 8c3176afd262a79625f582e1d4be324814352e456b5c709e0ddbd01c09382100},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.07345. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-09-09 in math.LO).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Artificial Intelligence (cs.AI); Logic (math.LO).
Pagina del lavoro: https://arxiv.org/abs/2609.07345 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-16T14:49:02.656Z dalla pagina https://arxiv.org/catchup/math.LO/2026-09-09?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).