一句话:提出 dialgebra 对偶框架,将一大类模态直觉主义逻辑及其框架实例化,并给出完备性与表达性结果。
本文填补模态直觉主义逻辑缺少系统性范畴对偶处理的空白。经典模态逻辑和分配格模态逻辑可分别借助 Stone 与 Priestley 对偶,在模态代数与描述框架之间建立对偶,从而推导完备性与可定义性。作者指出,模态直觉主义逻辑并不自然表现为代数/余代数对偶,而是作为 dialgebra 出现。技术贡献是为 dialgebra 及其逻辑建立对偶理论,并证明该框架可将一大类模态直觉主义逻辑及其框架作为特例实例化,进而给出一般情形下的完备性与表达性结果,也系统化了文献中已有的模态直觉主义逻辑处理。
Duality is one of the key techniques in the categorical treatment of modal logics. From the duality between (modal) algebras and (descriptive) frames one derives e.g. completeness (via a syntactic characterisation of algebras) or definability (using a suitable version of the Goldblatt-Thomason theorem). This is by now well understood for classical modal logics and modal logics based on distributive lattices, via extensions of Stone and Priestley duality, respectively. What is conspicuously absent is a comprehensive treatment of modal intuitionistic logic. This is the gap we are closing in this paper. Our main conceptual insight is that modal intuitionistic logics do not appear as algebra/coalgebra dualities, but instead arise naturally as dialgebras. Our technical contribution is the development of dualities for dialgebras, together with their logics, that instantiate to large class of modal intuitionistic logics and their frames as special cases. We derive completeness and expressiveness results in this general case. For modal intuitionistic logic, this systematises the existing treatment in the literature.