A Gödel Modal Logic over Witnessed Crisp Models

This paper considers the bi-modal logic with both □ and ◊ arising from Kripke models with crisp accessibility whose propositions are valued over the standard Gödel algebra [0, 1]. Since this logic lacks the finite model property, we study the logic GWc relying on witnessed Kripke models where, for each modal formula, there is an assignment where the formula without the modality takes the same value as the modal one. We provide a cut-free sequent calculus and we exploit it to prove that GWc is decidable and meets the finite model property. Finally, we explore a connection between the witnessed models and the well-known bi-relational Kripke semantics.