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 □ Ls. Q □ 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 □ Ls is the same. But in recent years (after 2018), we have obtained a variety of decidable Q □ Ls constructed in different ways. We distinguish between (1) the approach in which for every undecidable Q □ 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 □ Ls is obtained using general tools and a uniform method for all Q □ Ls of this class. In this paper, we compare the results of these approaches. [ABSTRACT FROM AUTHOR]