Kripke completeness of strictly positive modal logics over meet-semilattices with operators

Our concern is the completeness problem for strongly positive (SP) theories, that is, sets of implications between SP-terms built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, SP-theories have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations of a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given SP-theory.