严格正模态逻辑在带算子的交半格上的 Kripke 完备性
计算机科学中的逻辑
2026-01-21 v3
摘要
我们关注 spi-逻辑的完备性问题，即由命题变量、合取和模态菱形算子构建的严格正公式之间的蕴涵集合。spi-逻辑起源于逻辑、代数和计算机科学，具有两种自然语义：提供 Birkhoff 风格演算的带单调算子的交半格，以及在应用中常作为预期结构的第一阶关系结构（又称 Kripke 框架）。在此，我们为完备性理论奠定基础，旨在回答这两种语义对于给定的 spi-逻辑是否定义了相同的后承关系的问题。
引用
@article{arxiv.1708.03403,
title = {Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators},
author = {Stanislav Kikot and Agi Kurucz and Yoshihito Tanaka and Frank Wolter and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:1708.03403},
year = {2026}
}