Tableaux for Epistemic Gödel Logic

Abstract

We propose a multi-agent epistemic logic capturing reasoning with degrees of plausibility that agents can assign to a given statement with 1 interpreted as ‘entirely plausible for the agent’ and 0 as ‘completely implausible’ (i.e., the agent knows that the statement is false). We formalise such reasoning in an expansion of Gödel fuzzy logic with an involutive negation and multiple S5-like modalities. As already Gödel single-modal logics are known to lack the finite model property w.r.t. their standard [0, 1]-valued Kripke semantics, we provide an alternative semantics that allows for the finite model property. For this semantics, we construct a strongly terminating tableaux calculus that allows us to produce finite counter-models of non-valid formulas. We then use the tableaux to show that the validity problem in our logic is PSpace-complete when there are two or more agents, and coNP-complete for the single-agent case.