A Note on Boolean Modal Logic

We present a proof of a theorem mentioned in an earlier paper “Modal environment for Boolean speculations”, devoted to the study of extended modal languages containing the so-called “window” or “sufficiency” modal operator m. The theorem states that a particular axiom system for the poly-modal logic encompassing union, intersection and complement of relations (a Boolean analog of the propositional dynamic logic of Pratt, Fischer, Ladner and Segerberg) is complete for the standard Kripke semantics. Moreover this system modally defines the standard semantics — so in the terminology of the present paper the axiomatics is adequate. On the other hand our logic has the finite model property. Thus a fragment of second order logic, rather powerful with respect to expressiveness, turns out to be decidable.