Monadic second order logic embedded and analyzed inside proof assistant 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 powerful way to describe properties about sets and elements, often used in computer science and mathematics. The authors show how to represent MSO inside a proof system called Isabelle/HOL using three related but different methods, each balancing complexity and detail differently. They develop a new tool to handle substitutions in this logic carefully and prove that these methods are faithful, meaning they correctly capture the logic’s meaning. They also mechanize an important theorem about models of this logic and explore how different versions of MSO behave inside their framework.
Monadic second-order logicIsabelle/HOLdeep embeddingshallow embeddingcapture-avoiding substitutionLoewenheim-Skolem theoremHenkin semanticsformal verificationlogic in computer sciencemodel theory
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.