Bi-modal G\"odel logic over [0,1]-valued Kripke frames

We consider the Gödel bimodal logic determined by fuzzy Kripke models where both the propositions and the accessibility relation are infinitely valued over the standard Gödel algebra[0,1] and prove strong completeness of Fischer Servi intuitionistic modal logic IK plus the prelinearity axiom with respect to this semantics. We axiomatize also the bimodal analogues of T, S4, and S5 obtained by restricting to models over frames satisfying the [0,1]-valued versions of the structural properties which characterize these logics. As application of the completeness theorems we obtain a representation theorem for bimodal Gödel algebras. In a previous paper [6], we have considered a semantics for Gödel modal logic based on fuzzy Kripke models where both the propositions and the accessibility relation take values in the standard Gödel algebra [0,1], we call these Gödel-Kripke models, and we have provided strongly complete axiomatizations for the unimodal fragments of this logic with respect to validity and semantic entailment from countable theories. Similar results were obtained for the unimodal Gödel analogues of the classical modal logics T and S4 determined by Gödel-Kripke models over frames satisfying, respectively, the [0,1]-valued version of reflexivity, or reflexivity and transitivity. The axiomatization of the unimodal Gödel analogues of S5 remains open.