Algorithmic Correspondence and Canonicity for Possibility Semantics

The present paper develops a unified correspondence treatment of the Sahlqvist theory for possibility semantics, extending the results in \cite{Ya16} from Sahlqvist formulas to the strictly larger class of inductive formulas, and from the full possibility frames to filter-descriptive possibility frames. Specifically, we define the possibility semantics version of the algorithm ALBA, and an adapted interpretation of the expanded modal language used in the algorithm. We prove the soundness of the algorithm with respect to both (the dual algebras of) full possibility frames and (the dual algebras of) filter-descriptive possibility frames. We make some comparisons among different semantic settings in the design of the algorithms, and fit possibility semantics into this broader picture. One notable feature of the adaptation of ALBA to possibility frames setting is that the so-called nominal variables, which are interpreted as complete join-irreducibles in the standard setting, are interpreted as regular open closures of "singletons" in the present setting.