Crisp bi-G\"{o}del modal logic and its paraconsistent expansion

TL;DR

This paper introduces a Hilbert-style axiomatisation for crisp bi-G"{o}del modal logic and its paraconsistent expansion, establishing completeness, decidability, and exploring semantic properties and frame correspondences.

Contribution

It provides the first Hilbert-style calculus for these logics, proves their completeness and decidability, and analyzes their semantic properties and frame correspondences.

Findings

Completeness of $ ext{KbiG}$ and $ ext{KG}^lacksquare$ w.r.t. crisp Kripke models.

Decidability and validity are $ ext{PSPACE}$-complete for both logics.

Glivenko theorem holds only in finitely branching frames.

Abstract

In this paper, we provide a Hilbert-style axiomatisation for the crisp bi-G\"{o}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\"{o}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\"{o}del modal logic $\KG^c$. We show that, among others, all Sahlqvist formulas and all formulas $\phi\rightarrow\chi$ where $\phi$ and $\chi$ are monotone, define the same classes of frames in $\mathbf{K}$ and $\KG^c$.