Priestley Duality, a Sahlqvist Theorem and a Goldblatt-Thomason Theorem for Positive Modal Logic
Priestley Duality, a Sahlqvist Theorem and a Goldblatt-Thomason Theorem for Positive Modal Logic
复制标题
正模态逻辑的 Priestley 对偶性、Sahlqvist 定理和 Goldblatt-Thomason 定理
作者：
S. Celani;R. Jansana
在文献[12]中，正模式逻辑(PML)的研究开始于标准的Klipke语义，并引入了正模式代数(一类具有模式算子的有界分配格)。正模态逻辑的最小系统是由所有∧，∨模型类定义的局部因果关系的(⊥，2，3，Krpke，>；)-片段。它可以用一个序列演算来公理化，并可以通过添加序列作为新的公理来得到它的推广。在[6]中，为了克服[12]中讨论的框架不完备性问题，提出了一种新的PML语义。该语义的框架由一组索引、索引上的准序和可达性关系组成。这些模型是通过使用相对于框架的准序递增的估值来获得的。这一语义与本课题或本论文通过发展正模代数的Priestley对偶而得到的对偶结构是一致的，并且也可以被看作是源于适用于直觉主义模逻辑的Kriske语义。本文研究了上述对偶性，证明了一些d-持久化结果，证明了关于序列的Sahlqvist定理和[6]中提出的语义。还证明了GoldblattThomason定理，它刻画了可由序列集定义的该语义的框架的初等类。
In [12] the study of Positive Modal Logic (PML) is initiated using standard Kripke semantics and the positive modal algebras (a class of bounded distributive lattices with modal operators) are introduced. The minimum system of Positive Modal Logic is the (∧,∨, 2, 3,⊥,>)-fragment of the local consequence relation defined by the class of all Kripke models. It can be axiomatized by a sequent calculus and extensions of it can be obtained by adding sequents as new axioms. In [6] a new semantics for PML is proposed to overcome some frame incompleteness problems discussed in [12]. The frames of this semantics consists of a set of indexes, a quasi-order on them and an accessibility relation. The models are obtained by using increasing valuations relatively to the quasiorder of the frame. This semantics is coherent with the dual structures obtained by developing the Priestley duality for positive modal algebras, one of the topics or the present paper, and can be seen also as arising from the Kripke semantics for a suitable intuitionistic modal logic. The present paper is devoted to the study of the mentioned duality as well as to proving some d-persistency results as well as a Sahlqvist Theorem for sequents and the semantics proposed in [6]. Also a GoldblattThomason theorem that characterizes the elementary classes of frames of that semantics that are definable by sets of sequents is proved.