AI 中文总结
研究直觉模态逻辑的语义问题，提出关系覆盖语义的保守扩展，减轻限制便于模型构建，通过在Agda中形式化语义并建设性证明完备性，为直觉模态逻辑研究提供新方法。
AI 中文摘要
直觉模态逻辑（IML）在编程语言的多个发展中得到应用，如用于分期的模态类型系统、计算效应和基于语言的安全性。IML通常使用克里普克风格的关系语义进行研究，它便于构建模型以简化元理论性质的证明，但依赖经典推理原则。Goldblatt通过扩展直觉命题逻辑的贝思 - 克里普克 - 乔亚尔风格的“覆盖”语义并添加关系来支持模态，为IML提供了替代语义。不过其“关系覆盖”语义存在新限制。本文提出了关系覆盖语义的保守扩展，减轻了该限制，便于更简单和标准的模型构建技术。我们在Agda中形式化语义，并以评估规范化的风格建设性地证明了各种具有独立盒式和菱形模态的IML的完备性。
英文摘要
Intuitionistic modal logic (IML) has inspired several developments in programming languages including modal type systems for staging, computational effects and language-based security. IMLs are typically studied using Kripke-style relational semantics, which simplifies proofs of meta-theoretic properties, such as completeness and consistency, by making it easy to construct models. Kripke-style relational semantics, however, relies upon classical reasoning principles, which makes it unappealing from a computational perspective and unsuitable for formalization in a constructive type theory. Goldblatt provides an alternative semantics for IMLs by extending Beth-Kripke-Joyal-style "cover" semantics for intuitionistic propositional logic with relations to support modalities. Goldblatt's "relational cover" semantics overcomes classical reasoning but introduces a new limitation: it relies upon a "modal localization" condition that restricts the class of models and complicates model construction. Goldblatt bypasses this restriction by using intricate order-theoretic completion arguments to prove completeness. In this article, we present a conservative extension of relational cover semantics that alleviates this restriction and is amenable to simpler and standard model construction techniques. We formalize our semantics in Agda and prove completeness constructively in the style of Normalization by Evaluation for a variety of IMLs featuring independent box and diamond modalities.
CommentsPresented at MFPS 2026
