清晰双Gödel模态逻辑及其次协调扩张

本文为清晰双Gödel模态逻辑$\KbiG$提供了Hilbert式公理化，并证明了其关于清晰Kripke模型的完备性，其中每个状态上的公式在$[0,1]$上的标准双Gödel代数上求值。我们还考虑了$\KbiG$带De Morgan否定$\neg$的次协调扩张，称之为$\KGsquare$。我们为该逻辑设计了Hilbert式演算，并作为从$\KbiG$到$\KGsquare$保守翻译的推论，证明了其关于带两个经$\neg$关联的$[0,1]$上赋值的清晰Kripke模型的完备性。对这两种逻辑，我们确立了其可判定性与有效性为$\mathsf{PSPACE}$-完全。我们还研究了$\KbiG$与$\KGsquare$的语义性质。特别地，我们证明Glivenko定理仅在有限分支框架中成立。我们也探讨了在经典模态逻辑$\mathbf{K}$与清晰Gödel模态逻辑$\KG^c$中定义相同框架类的公式类。我们表明，除其他外，所有Sahlqvist公式及所有$\phi\rightarrow\chi$型公式（其中$\phi$与$\chi$为单调的）在$\mathbf{K}$与$\KG^c$中定义相同的框架类。