Monadic Second-Order Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Isabelle/HOL dataset)

We develop, in Isabelle/HOL, three embeddings of monadic second-order logic (MSO) into classical higher-order logic side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation), a maximal-shallow embedding, and a minimal-shallow embedding — the last a locale parametrised by an interpretation and by first- and second-order assignments. The enabling ingredient is a two-sorted capture-avoiding substitution apparatus (predication, substitution, alphabetic renaming, and a substitution lemma, developed once for each binder namespace), in which each binder is transparent for the other. Faithfulness of all three embeddings is mechanised and automated. The central result is a fully mechanised two-sorted downward Löwenheim–Skolem theorem. Its corollary identifies range-relative validity with the general (Henkin-style) reading of MSO, while comprehension witnesses that the standard reading is strictly stronger; an elementary-substructure refinement recovers the standard reading from the minimal embedding as well, so the two readings become one device under two interpretation classes. We further exercise the embeddings on classical MSO landmarks: Boolean closure and graph operations hold under the standard (full second-order) reading and fail under the general one, making the dichotomy concrete, while reachability and 2-colorability are non-theorems, refuted throughout with nitpick countermodels.