Paraconsistent Gödel modal logic

Abstract

We introduce a~paraconsistent modal logic $\mathbf{K}{\mathsf{G}}^2$, based on Gödel logic with coimplication (bi-Gödel logic) expanded with a De Morgan negation $\neg$. We use the logic to formalise reasoning with graded, incomplete and inconsistent information. Semantics of $\mathbf{K}{\mathsf{G}}^2$ is two-dimensional: we interpret $\mathbf{K}{\mathsf{G}}^2$ on crisp frames with two valuations $v_1$ and $v_2$, connected via $\neg$, that assign to each formula two values from the real-valued interval $[0,1]$. The first (resp., second) valuation encodes the positive (resp., negative) information the state gives to a~statement. We obtain that $\mathbf{K}{\mathsf{G}}^2$ is strictly more expressive than the classical modal logic $\mathbf{K}$ by proving that finitely branching frames are definable and by establishing a faithful embedding of $\mathbf{K}$ into $\mathbf{K}{\mathsf{G}}^2$. We also construct a~constraint tableau calculus for $\mathbf{K}{\mathsf{G}}^2$ over finitely branching frames, establish its decidability and provide a~complexity evaluation.

References in corpus (1)

• Towards a Proof Theory of Gödel Modal Logics