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

arXiv: https://arxiv.org/abs/2609.07345 · HTML: https://mlsanity.com/paper/2609.07345/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 27 references that are in the map.
- First posted on arXiv 7 Sep 2026.

## Builds on (most cited first, 2 of 2)

- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)](https://mlsanity.com/paper/2605.27246/) (2026)

## Built on by (most cited first, 1 of 1)

- [Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology](https://mlsanity.com/paper/2610.08214/) (2026)

## Abstract (arXiv)

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.