面向经典模态逻辑研究者的直觉主义与构造性模态逻辑
Intuitionistic and Constructive Modal Logics for Classical Modal Logicians
浏览论文内容
中文总结 AI 辅助
本文面向经典模态逻辑研究者，综述直觉主义框架下的两类命题模态逻辑，研究介于两者间的新逻辑$\textbf{KI}$并证其完备性，还指出$\textbf{CK}$语义缺陷并证明$\textbf{CK}$、$\textbf{WK}$的Lyndon插值定理。
中文摘要 AI 辅助
本文对直觉主义框架下的命题模态逻辑展开综述。主要面向已熟悉经典模态逻辑的读者，探讨了两类主流的直觉主义模态逻辑——直觉主义模态逻辑（IMLs）与构造性模态逻辑（CMLs）的分类成因、研究动机及相互比较。此外，本文深入研究了介于CML与IML传统之间的逻辑，包括新提出的逻辑$\textbf{KI}$并证明其完备性，同时综述了各类扩展及不含$\text{Diamond}$/$\boxed{}$的片段。本文还记录了若干文献中隐含或缺失的观察结果：指出$\textbf{CK}$原有语义中的一处小缺陷，并证明了$\textbf{CK}$与$\textbf{WK}$的Lyndon插值定理。
英文摘要
This paper gives a survey of propositional modal logic in an intuitionistic setting. Mainly intended for readers already familiar with classical modal logic, we discuss why there are two prominent families of such logics, intuitionistic modal logics (IMLs) and constructive modal logics (CMLs), what motivates their study, and how they compare with each other. Moreover, we take a deeper look at the logics lying between the CML and IML traditions, including a new logic $\textbf{KI}$ for which we prove completeness, and survey various extensions and $\Diamond$/$\Box$-free fragments. We further record several observations which seem to be implicit or absent in the literature; we point out a small defect in the original semantics for $\textbf{CK}$ and prove Lyndon interpolation theorems for $\textbf{CK}$ and $\textbf{WK}$.
