A Gödel Modal Logic Over Witnessed Models
For researchers in non-classical logics, this work offers a more constructive semantic framework for Gödel modal logics, though it is incremental as it adapts existing techniques to a new semantics.
The paper introduces GW, a Gödel modal logic with witnessed semantics that avoids limit-based phenomena, and provides a sound and complete refutation calculus with a terminating proof-search procedure, establishing the finite model property.
We introduce GW, a Gödel modal logic based on Kripke models in which the value of each modal formula is witnessed by an accessible world. This witnessed semantics eliminates the limit-based phenomena that preclude the finite model property in the usual Kripke semantics for Gödel modal logics, thereby yielding a more constructive semantic framework. We present a sound and complete refutation calculus for GW and design a terminating backward proof-search procedure with countermodel generation. As a direct consequence of this procedure, GW enjoys the finite model property.