Correspondence Theory for Many-valued Modal Logic

TL;DR

This paper extends Sahlqvist correspondence theory to many-valued modal logic using perfect Heyting algebras, introducing new translation methods, frame correspondences, and an adapted ALBA algorithm for effective computation.

Contribution

It generalizes classical correspondence theory to many-valued modal logic, defining new frame correspondences and adapting algorithms for effective analysis.

Findings

Effective translation between many-valued modal and first-order languages

Many-valued analogues of Sahlqvist and inductive formulas

Classical Sahlqvist formulas retain their frame correspondents in many-valued logic

Abstract

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.