Coalgebraic Dynamic Logic: Basic Completeness Results

I will present a coalgebraic generalisation of Fischer and Ladner’s Propositional Dynamic Logic (PDL) and Parikh’s Game Logic (GL). The basic observation is that programs (or games) are coalgebras for a monad T, the program constructs arise from Kleisli composition and algebraic structure on T, and the axioms of these logics correspond to certain compatibility requirements between the modalities and this structure. This setup allows us to prove two general completeness results: strong completeness without iteration, and (weak) completeness with iteration and "negation-free" pointwise operations.

(Joint work with Clemens Kupke.)