Proof systems for a Gödel modal logic

Abstract. A basic modal fuzzy logic GK is defined by combining the Kripke semantics of the modal logic K with the many-valued semantics of Gödel logic G. A sequent of relations calculus is introduced for GK and a constructive counter-model completeness proof is given. This calculus is used to establish completeness for a Hilbert-style axiomatization and Gentzen-style hypersequent calculus admitting cut-elimination, and to show that the logic is PSPACE-complete.