Reasoning about common knowledge with infinitely many agents
type: Item
instance of: scholarly article
title: Reasoning about common knowledge with infinitely many agents
zbMATH Open document ID: 1078.03014
author: Joseph Y. Halpern
author: Richard A. Shore
published in: Information and Computation
publication date: 2004-08-06T00:00:00Z
review text: 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 represent…
reviewed by: Jan Šefránek
Mathematics Subject Classification ID: 03B42
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68T30
zbMATH DE Number: 2083128
zbMATH Keywords: reasoning about knowledge
zbMATH Keywords: infinitely many agents
zbMATH Keywords: axiomatization
zbMATH Keywords: completeness
zbMATH Keywords: satisfiability
zbMATH Keywords: decision procedure
zbMATH Keywords: exponential complexity
zbMATH Keywords: epistemic logic
MaRDI profile type: Publication
full work available at URL: j.ic.2004.01.003
OpenAlex ID: W1965555095
cites work: Agreeing to disagree
cites work: Q3867808
cites work: Q4845472
cites work: What can machines know?
cites work: Propositional dynamic logic of regular programs
cites work: Q4221242
cites work: The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
cites work: A guide to completeness and complexity for modal logics of knowledge and belief
DOI: 10.1016/J.IC.2004.01.003
description: scientific article; zbMATH DE number 2083128