Algorithmic Correspondence Theory for Sabotage Modal Logic

Studies in Logic, Vol. 15, No. 6 (2022): 66–92   PII: 1674­3202(2022)­06­0066­27

Zhiguang Zhao

Abstract.

Sabotage modal logic (SML) is a kind of dynamic logic. It extends static modal logic with a dynamic modality which is interpreted as “after deleting an arrow in the frame, the formula is true”. In the present paper, we are aiming at solving an open problem stated in Aucher, van Benthem and Grossi (2018), namely giving a Sahlqvist­type correspondence theorem (Sahlqvist 1975) for sabotage modal logic. In this paper, we define sabotage Sahlqvist formulas and give an algorithm to compute the first­order correspondents of sabotage Sahlqvist formulas. We give some remarks and future directions at the end of the paper.