Axiomatisation for an asynchronous epistemic logic with sending and receiving messages
It provides a more complete axiomatisation for logics of asynchronous communication, but the contribution is incremental as it extends prior work without introducing new paradigms or empirical results.
The paper generalizes an existing axiomatisation for asynchronous epistemic logic with sending and receiving messages to handle formulas valid under any history of prior announcements and receptions, resulting in an infinitary, non-reduction system.
We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any message. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.