Crisp bi-Gödel modal logic and its paraconsistent expansion

Abstract

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 $\varphi \to \chi$ where $\varphi$ and $\chi$ are monotone, define the same classes of frames in $\mathbf{K}$ and $\KG^c$.

References in corpus (2)

• Time and Gödel: Fuzzy temporal reasoning in PSPACE
• Bi-intermediate logics of trees and co-trees

Cited by in corpus (2)

• Non-standard modalities in paraconsistent Gödel logic
• Fuzzy bi-Gödel modal logic and its paraconsistent relatives