Epistemic Logics with Quantification Over Epistemic Operators: Decidability and Expressiveness

The optimal balance between decidability and expressiveness is a big problem of logical systems, in particular, of quantified epistemic logics (QELs). On the one hand, decidability is a very significant characteristic of logics that allows us to use such logics in the framework of artificial intelligence. On the other hand, QELs have important expressive capabilities that should not be lost when we construct decidable fragments of these logics. QELs are known to be much more expressive than first-order logics. One important example of their extra expressive power is that they allow us to distinguish between de dicto and de re readings of epistemic sentences. It is clear that such capabilities should be preserved as much as possible in decidable fragments. In this paper, we consider extensions of QELs that include quantification over modalities. Denote this extensions by Q square Ls. Q square Ls allows us to make more subtle distinctions between de dicto and de re readings of epistemic sentences, and we also should keep these new features as much as possible in decidable fragments. It is known that there are not much interesting decidable QELs. The situation with Q square Ls is the same. But in recent years (after 2018), we have obtained a variety of decidable Q square Ls constructed in different ways. We distinguish between (1) the approach in which for every undecidable Q square L and for every variant of its decidable fragment, a specific proof is constructed, and (2) the approach in which a class of decidable Q square Ls is obtained using general tools and a uniform method for all Q square Ls of this class. In this paper, we compare the results of these approaches.