文章背景与核心概要

本文在 Isabelle/HOL 中对一元二阶逻辑（MSO）进行了全面机械化的研究，采用了一种深层与浅层相结合的嵌入方法。作者开发了三种平行的嵌入形式——深层嵌入、最大浅层嵌入和最小浅层嵌入，并由一套新颖的双排序代入机制提供支持。

核心贡献在于机械化证明了双排序向下勒文海姆-斯科姆定理（Löwenheim-Skolem theorem），这阐明了 MSO 的一般语义（Henkin 风格）与标准语义之间的关系。这些嵌入还在经典 MSO 里程碑问题上进行了测试，展示了不同语义框架之间的实际区别。

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

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

Authors: Christoph Benzmüller, Daniel Kirchner
Submitted: 7 September 2026
Primary Subject: Logic in Computer Science (cs.LO)
arXiv: 2609.07345
Formalization: Archive of Formal Proofs

📋 Summary

📋 Summary

This paper presents a fully mechanized study of Monadic Second-Order Logic (MSO) within Isabelle/HOL, utilizing a deep-and-shallow embedding methodology. The authors develop three parallel embeddings—deep, maximal-shallow, and minimal-shallow—supported by a novel two-sorted substitution apparatus.

A central contribution is the mechanized two-sorted downward Löwenheim-Skolem theorem, which clarifies the relationship between general (Henkin-style) and standard readings of MSO. The embeddings are further tested against classical MSO landmarks, demonstrating the practical distinction between the different semantic frameworks.

🔍 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: 1. A deep embedding (an inductive datatype with an explicit satisfaction relation); 2. A maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments as explicit arguments; and 3. 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 automated.

Our central contribution is a fully mechanised two-sorted downward Löwenheim-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 is provably stronger, 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 further 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.

🛠️ Metadata & Additional Information

Category	Details
Comments	39 pages. Extended version of a contribution accepted to a Festschrift for David Basin (Springer LNCS); the proceedings version is 19 pages.
Subjects	Logic in Computer Science (cs.LO), Artificial Intelligence (cs.AI), Logic (math.LO)
MSC Classes	03B70, 03B15, 68V15
ACM Classes	F.4.1
DOI	10.48550/arXiv.2609.07345
License	Creative Commons Attribution 4.0 International