An sp-implication is an implication between two strictly positive modal formulas, built from propositional variables, conjunction and modal diamond operators. Originated in algebra, logic and computer science, sp-implications have two natural semantics: meet-semilattices with monotone operators (SLOs) providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) that are often used as the intended semantics in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given set of sp-implications. We also investigate related decision and definability problems. The studied questions can also be reformulated as purely algebraic questions about varieties of SLOs.
joint work with S.Kikot, Y.Tanaka, F.Wolter and M.Zakharyaschev