Strong Completeness of Iteration-Free Coalgebraic Dynamic Logics
Helle Hvid Hansen, Clemens Kupke, R. Andres · 2014
Abstract. We present a (co)algebraic treatment of iteration-free dy-namic modal logics such as Propositional Dynamic Logic (PDL) and Game Logic (GL), both without star. The main observation is that the program/game constructs of PDL/GL arise from monad structure, and the axioms of these logics correspond to certain compatibilty re-quirements between the modalities and this monad structure. Our main contribution is a general soundness and strong completeness result for PDL-like logics for T-coalgebras where T is a monad and the ”program” constructs are given by sequential composition, test, and pointwise ex-tensions of operations of T. 1