Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modal Logic for Reasoning About Uncertainty and Confusion

Marta Bílková, Thomas M. Ferguson, Daniil Kozhemiachenko

TL;DR

This work extends Gödel modal logic with an involutive negation to model qualitative uncertainty and confusion, introducing KG$_{inv}$. It develops an alternative finite-model semantics equivalent to the standard one and builds a constraint tableaux calculus that can extract finite countermodels, establishing PSPACE-completeness for KG$_{inv}$ validity. The approach enables explicit, constructive reasoning about belief degrees and ambiguity, with potential applications in uncertainty management and description logics. The paper also outlines directions for further syntactic tools and comparisons with related logics.

Abstract

We consider a modal logic that can formalise statements about uncertainty and beliefs such as `I think that my wallet is in the drawer rather than elsewhere' or `I am confused whether my appointment is on Monday or Tuesday'. To do that, we expand Gödel modal logic KG with the involutive negation ~ defined as v(~A,w)=1-v(A,w). We provide semantics with the finite model property for our new logic that we call KG_inv and show its equivalence to the standard semantics over [0,1]-valued Kripke models. Namely, we show that a formula is valid in the standard semantics of KG_inv iff it is valid in the new semantics. Using this new semantics, we construct a constraint tableaux calculus for KG_inv that allows for an explicit extraction of countermodels from complete open branches and then employ the tableaux calculus to obtain the PSPACE-completeness of the validity in KG_inv.

Modal Logic for Reasoning About Uncertainty and Confusion

TL;DR

This work extends Gödel modal logic with an involutive negation to model qualitative uncertainty and confusion, introducing KG. It develops an alternative finite-model semantics equivalent to the standard one and builds a constraint tableaux calculus that can extract finite countermodels, establishing PSPACE-completeness for KG validity. The approach enables explicit, constructive reasoning about belief degrees and ambiguity, with potential applications in uncertainty management and description logics. The paper also outlines directions for further syntactic tools and comparisons with related logics.

Abstract

We consider a modal logic that can formalise statements about uncertainty and beliefs such as `I think that my wallet is in the drawer rather than elsewhere' or `I am confused whether my appointment is on Monday or Tuesday'. To do that, we expand Gödel modal logic KG with the involutive negation ~ defined as v(~A,w)=1-v(A,w). We provide semantics with the finite model property for our new logic that we call KG_inv and show its equivalence to the standard semantics over [0,1]-valued Kripke models. Namely, we show that a formula is valid in the standard semantics of KG_inv iff it is valid in the new semantics. Using this new semantics, we construct a constraint tableaux calculus for KG_inv that allows for an explicit extraction of countermodels from complete open branches and then employ the tableaux calculus to obtain the PSPACE-completeness of the validity in KG_inv.
Paper Structure (10 sections, 8 theorems, 24 equations, 3 figures)

This paper contains 10 sections, 8 theorems, 24 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Gödel logics with involution
  3. Gödel modal logics
  4. Gödel description logics
  5. Contributions and plan of the paper
  6. Language and standard semantics
  7. Semantics for $\mathbf{K}\mathsf{G}_{\mathsf{inv}}$ with the finite model property
  8. Tableaux
  9. Complexity
  10. Conclusion

Key Result

Proposition 1

$\mathfrak{F}\models_{\mathbf{K}\mathsf{G}_{\mathsf{inv}}}\Box p\leftrightarrow{\sim}\lozenge{\sim} p$ iff $\mathfrak{F}$ is crisp.

Figures (3)

  • Figure 1: All variables have the same values as $p$.
  • Figure 2: A failed $\mathcal{T}\!(\mathbf{K}\mathsf{G}_{\mathsf{inv}})$ proof of $\Box p\rightarrow{\sim}\lozenge{\sim} p$ and a model of the open branch (marked with $\frownie$).
  • Figure 3: Building the model on the fly: red states are active; green states are safe.

Theorems & Definitions (25)

  • Definition 1: Frames
  • Definition 2: Semantics of $\mathbf{K}\mathsf{G}_{\mathsf{inv}}$
  • Example 1
  • Example 2
  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Definition 3: $\mathsf{F}$-models
  • Theorem 1
  • ...and 15 more