A basic propositional modal fuzzy logic GK_□ is defined by combining the Kripke semantics of the modal logic K with the many-valued semantics of Godel 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.
展开▼