Sahlqvist Correspondence Theory for Modal Logic with Quantification over Relations

Studies in Logic, Vol. 16, No. 6 (2023): 39–57                PII: 1674­3202(2023)­06­0039­19

Fei Liang, Zhiguang Zhao

Abstract. Lehtinen (2008) introduced a new concept of validity of modal formulas, where quantification over binary relations is allowed for the so called “helper modalities”, and the “boss modalities” are similar to ordinary modalities in modal logic in the sense that they are interpreted as a fixed binary relation in a Kripke frame. In the present paper, we study the correspondence theory for this validity notion. We define the class of Sahlqvist formulas for this validity notion, each formula of which has a first­order frame correspondent, and define the algorithm  to compute the first­order correspondents of this class.