Proof Theory for Distributed Knowledge

摘要

The proof theory of multi-agent epistemic logic extended with operators for distributed knowledge is studied. A proposition A is distributed knowledge within a group G if A follows from the totality of what the individual members of G know. There are known axioma-tizations for epistemic logics with the distributed knowledge operator, but apparently no cut-free proof system for such logics has yet been presented. A Gentzen-style contraction-free sequent calculus system for propositional epistemic logic with operators for distributed knowledge is given, and a cut-elimination theorem for the system is proved. Examples of reasoning about distributed knowledge that use the calculus are given.