Simple tableaux for two expansions of Gödel modal logic

Abstract

This paper considers two logics. The first one, $\mathbf{K}{\mathsf{G}}_{\mathsf{inv}}$, is an expansion of the Gödel modal logic $\mathbf{K}\mathsf{G}$ with the involutive negation ${\sim }_{\mathsf{i}}$ defined as $v({\sim }_{\mathsf{i}}\varphi ,w)=1-v(\varphi ,w)$. The second one, $\mathbf{K}{\mathsf{G}}_{\mathsf{bl}}$, is the expansion of $\mathbf{K}{\mathsf{G}}_{\mathsf{inv}}$ with the bi-lattice connectives and modalities. We explore their semantical properties w.r.t. the standard semantics on $[0,1]$-valued Kripke frames and define a unified tableaux calculus that allows for the explicit countermodel construction. For this, we use an alternative semantics with the finite model property. Using the tableaux calculus, we construct a decision algorithm and show that satisfiability and validity in $\mathbf{K}{\mathsf{G}}_{\mathsf{inv}}$ and $\mathbf{K}{\mathsf{G}}_{\mathsf{bl}}$ are PSpace-complete.