Simple tableaux for two expansions of Gödel modal logic

2024/01/27 by Marta Bílková, T. Ferguson, Bilkova, Marta +3
Computer Science · #Advanced Algebra and Logic #FOS: Mathematics #Logic (math.LO)

paper · pdf · doi:10.48550/arxiv.2401.15395

openalex publication_date 2024/01/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper considers two logics. The first one, KG_inv, is an expansion of the Gödel modal logic KG with the involutive negation ∼_i defined as v(∼_iϕ,w)=1-v(ϕ,w). The second one, KG_bl, is the expansion of KG_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 KG_inv and KG_bl are PSpace-complete.

Related

• Paraconsistent Gödel modal logic on bi-relational frames
• Bi-modal Gödel logic over [0,1]-valued Kripke frames
• Modal Logic for Reasoning About Uncertainty and Confusion
• Simplified Kripke semantics for K45-like Godel modal logics and its axiomatic extensions
• Standard Gödel modal logics are not realized by Gödel justification logics