Algorithmic correspondence for intuitionistic modal mu-caculus

In the present paper, the algorithmic correspondence theory developed in Conradie and Palmigiano [9] is extended to mu-calculi with a non-classical base. We focus in particular on the language of bi-intuitionistic modal mu-calculus. We enhance the algorithm ALBA introduced in Conradie and Palmigiano [9] so as to guarantee its success on the class of recursive mu-inequalities, which we introduce in this paper. Key to the soundness of this enhancement are the order-theoretic properties of the algebraic interpretation of the fixed point operators. We show that, when restricted to the Boolean setting, the recursive mu-inequalities coincide with the “Sahlqvist mu-formulas” defined in van Benthem, Bezhanishvili and Hodkinson [22].