Propositional Epistemic Logics with Quantification Over Agents of Knowledge

The paper presents a family of propositional epistemic logics such that languages of these logics are extended by quantification over modal (epistemic) operators or over agents of knowledge and extended by predicate symbols that take modal (epistemic) operators (or agents) as arguments. Denote this family by ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}). There exist epistemic logics whose languages have the above mentioned properties (see, for example Corsi and Orlandelli in Stud Log 101:1159–1183, 2013; Fitting et al. in Stud Log 69:133–169, 2001; Grove in Artif Intell 74(2):311–350, 1995; Lomuscio and Colombetti in Proceedings of ATAL 1996. Lecture Notes in Computer Science (LNCS), vol 1193, pp 71–85, 1996). But these logics are obtained from first-order modal logics, while a logic of ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}) can be regarded as a propositional multi-modal logic whose language includes quantifiers over modal (epistemic) operators and predicate symbols that take modal (epistemic) operators as arguments. Among the logics of ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}) there are logics with a syntactical distinction between two readings of epistemic sentences: de dicto and de re (between ‘knowing that’ and ‘knowing of’). We show the decidability of logics of ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}) with the help of the loosely guarded fragment (LGF) of first-order logic. Namely, we generalize LGF to a higher-order decidable loosely guarded fragment. The latter fragment allows us to construct various decidable propositional epistemic logics with quantification over modal (epistemic) operators. The family of this logics coincides with ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}). There are decidable propositional logics such that these logics implicitly contain quantification over agents of knowledge, but languages of these logics are usual propositional epistemic languages without quantifiers and predicate symbols (see Grove and Halpern in J Log Comput 3(4):345–378, 1993). Some logics of ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}) can be regarded as counterparts of logics defined in Grove and Halpern (J Log Comput 3(4):345–378, 1993). We prove that the satisfiability problem for these logics of ({mathcal {P}mathcal {E}mathcal {L}}_{({ QK})}) is Pspace-complete using their counterparts in Grove and Halpern (J Log Comput 3(4):345–378, 1993).