Paraconsistent G\"{o}del modal logic

TL;DR

This paper introduces a paraconsistent G"odel modal logic that formalizes reasoning with inconsistent and incomplete information, featuring a two-dimensional semantics and a tableau calculus with decidability results.

Contribution

It presents a novel paraconsistent modal logic based on G"odel logic with coimplication, including semantics, expressiveness comparison, and a decision procedure.

Findings

$ extbf{K} extbf{G}^2$ is more expressive than classical modal logic $ extbf{K}$.

Finitely branching frames are definable within $ extbf{K} extbf{G}^2$.

A sound and complete tableau calculus for $ extbf{K} extbf{G}^2$ is established with known complexity.

Abstract

We introduce a~paraconsistent modal logic $\mathbf{K}\mathsf{G}^2$, based on G\"{o}del logic with coimplication (bi-G\"{o}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.