Correspondence theory for many-valued modal logic

The aim of the present paper is to generalise Sahlqvist correspondence theory to the many-valued modal semantics defined by Fitting, assuming a perfect Heyting algebra as truth value space. We present the standard translations between many-valued modal languages and suitably defined first-order and second-order correspondence languages and prove their correctness. We introduce a notion of many-valued modal frame correspondence with a truth value parameter. Exploring the consequences of this definition, we define many-valued analogues of the syntactically specified classes of Sahlqvist and inductive formulas. We adapt the ALBA algorithm to effectively compute many-valued parameterized local frame correspondents for all many-valued Sahlqvist and inductive formulas. Lastly we prove that the many-valued frame correspondent (parameterized with any non-zero truth value) of every classical Sahlqvist formula is syntactically identical to its standard crisp frame correspondent.