Strong conservativity and completeness for fragments of infinitary action logic

Abstract

We study fragments of infinitary action logic, the algebraic logic of *-continuous residuated Kleene lattices, from the point of view of entailment from (possibly infinite) sets of hypotheses. The contribution of this article is twofold. First, we show, by establishing a cut normalisation result, that elementary fragments obtained by restricting the set of connectives are strongly conservative. This means that conservativity holds not just for pure derivability, but also for derivability from sets of hypotheses.
This is proved in the presence of iterative divisions---compound connectives of a division and Kleene iteration in the denominator. Second, for the fragment with divisions, intersection, and iterative divisions, we prove strong completeness w.r.t. natural classes of models on language algebras and algebras of binary relations.