一句话:为直觉主义交-蕴涵片段引入保交与单调模态,建立半格语义、对偶、完备性及可表达性结果。
论文研究命题直觉主义逻辑的交-蕴涵片段在加入模态算子后的逻辑性质。作者首先将交-蕴涵片段扩展为带有保交模态的模态逻辑,给出基于半格(semilattice)的语义,并建立与适当描述框架(descriptive frame)的对偶结果。由此证明该逻辑相对该语义的完备性,并识别出一大类模态直觉主义逻辑所共有的模态片段。进一步将该逻辑视为 dialgebraic logic,从而得到“expressivity-somewhere-else”性质。随后在 dialgebraic 框架内考察带单调模态的交-蕴涵片段扩展,证明其完备性并同样建立 expressivity-somewhere-else。
We extend the meet-implication fragment of propositional intuitionistic logic with a meet-preserving modality. We give semantics based on semilattices and a duality result with a suitable notion of descriptive frame. As a consequence we obtain completeness and identify a common (modal) fragment of a large class of modal intuitionistic logics. We recognise this logic as a dialgebraic logic, and as a consequence obtain expressivity-somewhere-else. Within the dialgebraic framework, we then investigate the extension of the meet-implication fragment of propositional intuitionistic logic with a monotone modality and prove completeness and expressivity-somewhere-else for it.