Email Gateway (Jul 13 2026 at 12:39): Email Gateway (Jul 13 2026 at 12:39):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: MSO in HOL by Christoph Benzmüller and Daniel Kirchner
Dear all,
I’d like to announce another new AFP entry of today.
Monadic Second-Order Logic in HOL:
Deep and Shallow Embeddings with Automated Faithfulness
(Isabelle/HOL dataset)
by Christoph Benzmüller and Daniel Kirchner
We develop, in Isabelle/HOL, three embeddings of monadic second-order logic
(MSO) into classical higher-order logic side by side: a deep embedding (an
inductive datatype with an explicit satisfaction relation), a maximal-shallow
embedding, and a minimal-shallow embedding — the last a locale parametrised by
an interpretation and by first- and second-order assignments. The enabling
ingredient is a two-sorted capture-avoiding substitution apparatus (predication,
substitution, alphabetic renaming, and a substitution lemma, developed once for
each binder namespace), in which each binder is transparent for the other.
Faithfulness of all three embeddings is mechanised and automated. The central
result is a fully mechanised two-sorted downward Löwenheim–Skolem theorem. Its
corollary identifies range-relative validity with the general (Henkin-style)
reading of MSO, while comprehension witnesses that the standard reading is
strictly stronger; an elementary-substructure refinement recovers the standard
reading from the minimal embedding as well, so the two readings become one
device under two interpretation classes. We further exercise the embeddings on
classical MSO landmarks: Boolean closure and graph operations hold under the
standard (full second-order) reading and fail under the general one, making the
dichotomy concrete, while reachability and 2-colorability are non-theorems,
refuted throughout with nitpick countermodels.
https://isa-afp.org/entries/MSOinHOL.html
Enjoy,
René
Last updated: Jul 22 2026 at 14:00 UTC