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

Abstract

In this paper, we provide a Hilbert-style axiomatization 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 ¬, which we dub KG2. We devise a Hilbert-style calculus for this logic and, as a consequence of a conservative translation from KbiG to KG2, prove its completeness w.r.t. crisp Kripke models with two valuations over [0, 1] connected via ¬. For these two logics, we establish that their decidability and validity are PSPACE-complete. We also study the semantical properties of KbiG and KG2. In particular, we show that Glivenko’s theorem holds only in finitely branching frames. We also explore the classes of formulas that define the same classes of frames both in K (the classical modal logic) and the crisp Gödel modal logic BKc. We show that, among others, all Sahlqvist formulas and all formulas ϕ → χ where ϕ and χ are monotone define the same classes of frames in K and BKc.