Reasoning about common knowledge with infinitely many agents (Q598197)

The complexity of the satisfiability problem for epistemic logic with an infinite set of agents is characterized in the paper. A consideration of infinitely many agents is motivated by (many) applications where the set of agents is not known in advance and has no a priori upper bound. A language \(\mathcal L^{C}_{\mathcal G}(\Phi)\) is used in the paper, where \(\Phi\) is a set of primitive propositions, \(\mathcal A\) is a possibly infinite set of agents, \(\mathcal G\) is a set of nonempty subsets of \(\mathcal A\) and formulas are build over \(\Phi\) by operators \(\neg, \vee, K_i\), for \(i \in \mathcal A, E_G, C_G\), for \(G \in {\mathcal G}\). \(C_G\) intuitively means ``common knowledge among group \(G\)'' and \(E_G\) means ``everyone in \(G\) knows''. A Kripkean semantics is given for the language(s). Standard axioms and rules for the knowledge operators \(K_i\) are used. Axioms (and a rule) for reasoning about ``everyone in \(G\) knows'' are crucial for the presented formalization. Finally, also common knowledge is axiomatized in a standard way. Two important and technically difficult main results are obtained. The first main result of the paper is regarding completeness of the axiomatization. It is shown that the axiomatization for reasoning about knowledge and common knowledge (if there are infinitely many agents) is sound and complete. Second, it is shown that there is an exponential decision procedure for satisfiability checking. It is shown that reasoning about knowledge and common knowledge with infinitely many agents is not harder than when there are finitely many agents, provided that we can check the cardinality of set differences \(G - G^{\prime}\), where \(G\) and \(G^{\prime}\) are sets of agents. Complexity results represent improvements over previous results even for finite sets of agents (the results are independent of cardinality). It is also shown that the obtained results depend on how the sets of agents are represented. The used representation involves only set difference and union; it remains an open question whether the results can be extended also for the descriptions that involve intersection and complementation. Finally, directions for extending the results of the paper are described.