Simple tableaux for two expansions of Gödel modal logic

TL;DR

A unified tableaux calculus is defined that allows for the explicit countermodel construction and satisfiability and validity in $\mathbf{K}\mathsf{G}_\mathsf{inv$ and $\mathbf{K}\mathsf{G}_\mathsf{bl}$ are PSpace-complete.

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}}φ,w)=1-v(φ,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.

Figures (1)

• Figure 1: $[0,1]^{\Join}$

Theorems & Definitions (5)

• definition thmcounterdefinition: Frames
• definition thmcounterdefinition: $\mathbf{K}\mathsf{G}_{\mathsf{inv}}$
• definition thmcounterdefinition: Frame definability
• theorem thmcountertheorem
• proof