HOL中的一元二阶逻辑：深度与浅层嵌入及自动化忠实性（扩展预印本）
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
查看机构详情
- University of Bamberg（班贝格大学）
- Freie Universität Berlin（柏林自由大学）
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
在Isabelle/HOL中为MSO开发三种嵌入，提出两类替换机制实现自动化忠实性，并机械化证明向下Loewenheim-Skolem定理，区分一般与标准解释，通过经典例子展示差异。
中文摘要 AI 辅助
在Isabelle/HOL中，我们将先前工作中的深度与浅层嵌入方法论应用于一元二阶逻辑（MSO）。我们并排开发了三种嵌入：深度嵌入（一个带有显式满足关系的归纳数据类型）；最大浅层嵌入，将连接词和量词直接翻译成HOL，将解释和两个赋值作为显式参数携带；以及最小浅层嵌入——一个固定这些参数的locale，将公式类型折叠为bool。新的关键要素是一个两类的替换机制——避免捕获的替换、重命名以及每个命名空间一个替换引理——其中每个绑定器对另一个是透明的；所有三种嵌入的忠实性都被机械化并自动化。我们的核心贡献是一个完全机械化的两类向下Loewenheim-Skolem定理：最小嵌入相对于（可数的）赋值范围恢复了深度有效性，并且这种范围相对的解释被证明与MSO的一般（Henkin风格）解释一致，而标准解释被证明更强，由理解公理见证。尽管如此，两种解释都从最小嵌入中恢复，仅在允许的解释上有所不同：一般解释允许所有解释，标准解释只允许完整模型的初等子结构。我们进一步在经典的MSO里程碑上测试这些嵌入：布尔闭包和图模式在完整的二阶域下成立，但在最小嵌入中失败，使这种二分法具体化，而可达性和2-可着色性在所有嵌入中都被反驳。
英文摘要
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.
