##
Strictly positive implications: completeness, decision and definability problems

### Agi Kurucz

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