Algorithmic correspondence for intuitionistic modal mu-calculus, Part 2

Sahlqvist-style correspondence results remain a perennial theme and an active topic of research within modal logic. Recently there has been interest in extending classical results in this area to the modal mu-calculus. We show how the `calculus of correspondence' and the ALBA algorithm (Conradie and Palmigiano, 2012) can be extended to the intuitionistic mu-calculus, and be used to derive FO+LFP frame correspondents for formulas of that logic. We define the class of recursive mu-inequalities, which we compare it with related classes in the literature including the Sahlqvist mu-formulas of van Benthem, Bezhanishvili and Hodkinson. We show that the ALBA algorithm succeeds in reducing every recursive mu-inequality, and hence that every recursive mu-inequality has a frame correspondent in FO+LFP.