First Order Modal Logic in HOL Deep and Shallow Embeddings with Automated Faithfulness

Jul 16, 2026

Upload by Sage

The extended preprint develops, in Isabelle/HOL, deep-and-shallow embedding techniques for first-order modal logic with constant-domain Kripke semantics. Three side-by-side embeddings are provided: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is formalized as an Isabelle/HOL locale with a global faithfulness theorem showing that quantifying over all minimal-shallow interpretations exactly recovers deep validity. Faithfulness automation relies on a mechanized downward Löwenheim–Skolem theorem and new substitution machinery for first-order quantifiers.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages21

Reading Time53 min

Abstract

Motivation and Introduction

Contributions

Embeddings (Deep and Shallow)

Faithfulness via Locales

Substitution Machinery for Quantifiers

Downward Löwenheim–Skolem and Faithfulness Automation

First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint) Christoph Benzmüller1,2, * , Daniel Kirchner1 1 University of Bamberg, Bamberg, Germany 2 Freie Universität Berlin, Berlin, Germany Abstract We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositionalto first-order modal logic (FML) with constant-domain Kripke semantics. Three embeddings ofFML into classical higher-order logic (HOL) are provided side by side: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is presented as an Isabelle/HOL locale, parametrised by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; the locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is a mechanisation, for FML under constant-domain Kripke semantics, of the (countable) downward Löwenheim–Skolem theorem, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it inside an extension of the minimal-shallow locale resolves the surjectivity problem that arises against an uncountable domain of individuals —where the locale’s variable assignment, having countable domain 􀁖 = nat, cannot be surjective onto the domain — and thereby yields faithfulness over the full domain. Since prior work treats only the propositional fragment, we develop here the substitution machinery (free/bound-variable predicates, the fresh-variable function, capture-avoiding substitution, alphabetic renaming, the substitutability predicate, the substitution lemma, and size-based induction principles) needed for the first-order quantifiers. Keywords first-order modal logic, Kripke semantics, shallow embedding, deep embedding, Isabelle/HOL, locales, elementary substructure, Löwenheim–Skolem theorem, Tarski–Vaught test, faithfulness automated 1. Motivation and Introduction First-order modal logic (FML) sits at the intersection of two of the most pervasive sources of expressive power in symbolic logic: quantification and modality. It is a natural setting for many applications of logic in artificial intelligence, computer science, and philosophy. Embeddings into classical higher-order logic (HOL) [1, 2] have repeatedly been shown to provide a fruitful host environment for such logics; see [3, 4] and the references therein. Shallow embeddings, which identify object-level formulae with HOL terms via the standard translation, give immediate access to Isabelle/HOL’s proof automation, including sledgehammer, nitpick, and auto. Deep embeddings, in which formulae are represented as elements of an inductively defined datatype, are needed for metalogical reasoning about syntax, substitution, or proof systems. We have recently shown [5] that both approaches can be carried out simultaneously, in a single HOL theory, in such a way that mutual faithfulness proofs can be automated. That paper focuses on propositional modal logic (PML), where modality is the only complication. The natural next step, which we take in this paper, is to add quantification in order to move from PML to FML. ARQNL’26: International Workshop on Automated Reasoning in Quantified Non-Classical Logics, 2026 * Corresponding author. $ [christoph.benzmueller@uni-bamberg.de](christoph.benzmueller@uni-bamberg.de) (C. Benzmüller); [daniel.kirchner@uni-bamberg.de](daniel.kirchner@uni-bamberg.de) (D. Kirchner) 􀀚 0000-0002-3392-3093 (C. Benzmüller); 0000-0001-9229-1148 (D. Kirchner) © 2026 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0) . Contributions. We contribute MinFMLinHOL,1 an Isabelle/HOL development covering FML with binary relationa

FAQs

What technical results support the automated faithfulness proof?

A mechanization of the (countable) downward Löwenheim–Skolem theorem for FML under constant-domain semantics provides the key bridge between deep validity and minimal-shallow interpretations, while new first-order substitution machinery supports quantifier reasoning.

Jul 16, 2026

Upload by Sage