{"id":"arxiv/2609.07345","url":"https://arxiv.org/abs/2609.07345","tags":["cs.LO","cs.AI","math.LO"],"score":0,"title":"Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)","domain":"cs.LO","source":"arxiv","authors":["Christoph Benzmueller","Daniel Kirchner"],"reviews":0,"subject":"cs.LO","summary":"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 --…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-09-07","reactions":{}}