Summary: [For the entire collection see Zbl 0758.00018.]
We present a proof of a theorem mentioned in an earlier paper [the authors and T. Tinchev, Mathematical logic and its applications, Proc. Adv. Int. Summer Sch. Conf., Druzhba/Bulg. 1986, 253-263 (1987; Zbl 0701.03008)], devoted to the study of extended modal languages containing the so-called “window” or “suifficiency” modal operator. 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.