Faithful embeddings model monadic second order logic in hol
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
Logic in Computer ScienceArtificial Intelligence
Summary
Monadic second-order logic (MSO) is a complex system for expressing mathematical statements about objects and sets. The authors show how to represent MSO inside a proof assistant called Isabelle/HOL using three different but connected methods. They prove that these methods faithfully capture the logic's meaning, clarifying how different interpretations of MSO relate to each other. This work also establishes a key theorem within this setting and tests the methods on known logical properties, highlighting subtle differences between interpretations.
What this means in practice
- •For formal methods engineers: Ensure accurate formal reasoning about MSO properties within Isabelle/HOL for verifying software and hardware systems.
- •For automated theorem proving developers: Use the mechanised embeddings and substitution apparatus to build more reliable MSO support in automated reasoning tools.
A theory result. No direct application yet.
Authors
Christoph Benzmueller, Daniel Kirchner
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: 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 as explicit arguments; 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 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 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.