A Gödel Modal Logic Over Witnessed Models

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.