Ultraproducts and possible worlds semantics in institutions (Q2373712)

The theory of institutions [\textit{J. A. Goguen} and \textit{R. M. Burstall}, J. Assoc. Comput. Mach. 39, No. 1, 95--146 (1992; Zbl 0799.68134)] is a categorical abstract model theory which formalizes the intuitive notion of logical system, including syntax, semantics, and the satisfaction between them. In this paper the authors develop possible worlds (Kripke) semantics at the categorical abstract model-theoretic level provided by institutions. The general abstract modal logic framework provides a method for semantic Kripke semantics extensions of logical systems from computing science and logic. Also, they extend the institution-independent method of ultraproducts of \textit{R. Diaconescu} [Fundam. Inform. 55, No. 3--4, 321--348 (2003; Zbl 1036.03055)] to possible worlds semantics and prove a fundamental preservation result for abstract modal satisfaction. As a consequence, they develop a generic compactness result for possible worlds semantics.