A Representation Theorem for Reasoning in First-Order Multi-Agent Knowledge Bases

Levesque's notion of only-knowing provides a natural formalisation of a knowledge base: it precisely captures the beliefs and non-beliefs that follow from the knowledge base, including introspection and de dicto versus de re distinctions in a first-order setting. Apart from its attractive properties in terms of specification, a major result about only-knowing is Levesque's representation theorem, which shows how reasoning in (single-agent) knowledge bases can be Turingreduced to ordinary first-order logic. While numerous proposals have been made to lift the logic of only-knowing to the multiagent case, generalising the representation theorem has remained an open problem. In this paper, we develop a Turing reduction from reasoning in multi-agent knowledge bases to ordinary, nonepistemic first-order logic and thus obtain a new representation theorem for the multi-agent case.