论文标题
Crisp bi-Gödel模态逻辑及其副暂停扩展
Crisp bi-Gödel modal logic and its paraconsistent expansion
论文作者
论文摘要
在本文中，我们为Crisp Bi-Gödel模式逻辑$ \ kbig $提供了希尔伯特风格的公理化。我们证明了它的完整性W.R.T. \ Crisp Kripke模型，其中在标准的Bi-Gödel代数上以$ [0,1] $评估了每个州的公式。我们还考虑了$ \ kbig $的旁s，de Morgan negation $ \ neg $，我们将其列为$ \ kgsquare $。我们为此逻辑设计了希尔伯特风格的演算，并作为〜con \ -se \ - Quence a保守翻译从$ \ kbig $到$ \ kgsquare $，证明其完整性W.R.T. \ Crisp Kripke Kripke型号Kripke型号具有两种佳肴，具有$ [0,1] $ connect $ \ neg $ \ neg $ \ neg $ \ neg $ \ neg $ \ neg $ \ neg $。 对于这两种逻辑，我们确定它们的可决定性和有效性为$ \ mathsf {pspace} $ - 完整。 我们还研究$ \ kbig $和$ \ kgsquare $的语义属性。特别是，我们表明Glivenko定理仅在有限的分支框架中保存。我们还探索了在$ \ mathbf {k} $（经典的模态逻辑）和CrispGödel模态逻辑$ \ kg^c $中定义相同类帧的公式类。我们表明，除其他外，所有SAHLQVIST公式和所有公式$ ϕ \rightarrowχ$其中$ ϕ $和$χ$都是单调的，在$ \ mathbf {k} $和$ \ \ kg^c $中定义了相同类别的帧。
In this paper, we provide a Hilbert-style axiomatisation for the crisp bi-Gödel modal logic $\KbiG$. We prove its completeness w.r.t.\ crisp Kripke models where formulas at each state are evaluated over the standard bi-Gödel algebra on $[0,1]$. We also consider a paraconsistent expansion of $\KbiG$ with a De Morgan negation $\neg$ which we dub $\KGsquare$. We devise a Hilbert-style calculus for this logic and, as a~con\-se\-quence of a~conservative translation from $\KbiG$ to $\KGsquare$, prove its completeness w.r.t.\ crisp Kripke models with two valuations over $[0,1]$ connected via $\neg$. For these two logics, we establish that their decidability and validity are $\mathsf{PSPACE}$-complete. We also study the semantical properties of $\KbiG$ and $\KGsquare$. In particular, we show that Glivenko theorem holds only in finitely branching frames. We also explore the classes of formulas that define the same classes of frames both in $\mathbf{K}$ (the classical modal logic) and the crisp Gödel modal logic $\KG^c$. We show that, among others, all Sahlqvist formulas and all formulas $ϕ\rightarrowχ$ where $ϕ$ and $χ$ are monotone, define the same classes of frames in $\mathbf{K}$ and $\KG^c$.
