pith. sign in

arxiv: 2510.02890 · v2 · submitted 2025-10-03 · 💻 cs.LO · cs.MA

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

Philippe Balbiani , Hans van Ditmarsch , Clara Lerouvillois This is my paper

Pith reviewed 2026-05-18 10:16 UTC · model grok-4.3

classification 💻 cs.LO cs.MA
keywords asynchronous announcementsepistemic logicaxiomatisationsending and receiving messagesinfinitary logicKripke modelsdynamic modalities
0
0 comments X

The pith

An infinitary axiomatisation AA* extends the logic of asynchronous announcements to formulas valid after any history of sends and receives.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proposes a generalization of an earlier axiomatisation for epistemic logic with separate modalities for sending and receiving announcements asynchronously. The original system AA reduces formulas to pure epistemic ones when evaluated before any messages occur. The new system AA* applies to interpretations relative to arbitrary prior histories of announcements and receptions in a Kripke model. This matters because validity changes once messages have already been exchanged, for instance the statement that nobody has received a message no longer holds. The result is an infinitary axiomatisation that is sound and complete but no longer serves as a reduction system.

Core claim

The paper establishes that the semantics interpreting formulas in a Kripke model given any history of prior announcements and receptions admits a sound and complete infinitary axiomatisation AA* which properly generalizes the earlier reduction system AA for the initial state without announcements.

What carries the argument

The infinitary axiomatisation AA*, a set of axioms and rules for the send and receive modalities that remains sound and complete when formulas are evaluated relative to an arbitrary history of prior announcement events.

If this is right

  • Reasoning about knowledge after some announcements have been sent and received becomes possible within the same logical framework.
  • Statements such as nobody having received any message are no longer valid once a history is present.
  • Every formula remains equivalent to one without dynamic modalities only in the special case of the empty history.
  • The axiomatisation requires infinitary rules to capture validity across all possible histories.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The history-dependent interpretation may support modeling of communication protocols where message delivery times vary across agents.
  • Similar infinitary techniques could apply to other dynamic epistemic logics that track sequences of events rather than single updates.
  • One could check completeness by attempting to derive formulas about common knowledge after a fixed sequence of sends and receives.

Load-bearing premise

The semantics with arbitrary histories of announcements and receptions admits a sound and complete infinitary axiomatisation.

What would settle it

A specific formula that holds in the Kripke model semantics for some nonempty history of announcements and receptions but cannot be derived in AA*, or an axiom of AA* that derives a formula invalid under that semantics.

Figures

Figures reproduced from arXiv: 2510.02890 by Clara Lerouvillois, Hans van Ditmarsch, Philippe Balbiani.

Figure 1
Figure 1. Figure 1: The announcement p ∨ q is sent, after which first Alice and then Bill receives it. States are labelled with the valuations of p and q. States that are indistinguishable for an agent are linked with a label for that agent. We omit reflexive arrows. In (ii) and then (iii) and (iv), we write (pq) and draw dashed lines between that state and pq (resp. pq) to represent the update induced by the sending of p∨q a… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript proposes an infinitary axiomatisation AA* for an asynchronous epistemic logic that separates sending and receiving of messages via distinct modalities. Formulas are interpreted relative to a Kripke model plus an arbitrary finite history of prior announcements and receptions; AA* is claimed to be sound and complete for the validities under this generalised semantics. It differs from the prior reduction system AA (valid only for the empty-history case) in that it is infinitary, does not reduce to pure epistemic formulas, and does not validate statements such as 'nobody has received any message'.

Significance. If the soundness and completeness claims hold, the result would supply a uniform proof system for epistemic reasoning after arbitrary finite communication histories, extending dynamic epistemic logic to more realistic asynchronous settings. This could support verification of knowledge properties in distributed systems where message delivery is not instantaneous or uniform.

major comments (2)
  1. [§4] §4 (Soundness and completeness): the manuscript asserts that the fixed infinitary rule set of AA* is sound and complete for every possible finite history, yet supplies no explicit inductive argument or case analysis showing how the rules capture interactions that arise only after specific sequences (e.g., a send followed by selective reception by a proper subset of agents). This step is load-bearing for the central claim that a single axiomatisation works uniformly for arbitrary histories.
  2. [§3.2] §3.2 (Definition of AA*): the infinitary rules are introduced without accompanying proof sketches or concrete examples that verify they correctly generalise the empty-history case of AA while remaining complete once histories are non-empty. The absence of such verification leaves the correctness claim unsupported by the data in the text.
minor comments (2)
  1. [Introduction] The contrast between AA and AA* would be clearer if a short table listed the axioms or rules that are dropped or added when moving from the empty-history to the arbitrary-history setting.
  2. [§2] Notation for histories (sequences of sends/receives) should be introduced once and used uniformly in both semantic clauses and the axiomatisation to prevent ambiguity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. The comments highlight the need for greater explicitness in the soundness and completeness arguments for AA*, which we will address by adding the requested inductive details and examples in the revised manuscript.

read point-by-point responses

  1. Referee: [§4] §4 (Soundness and completeness): the manuscript asserts that the fixed infinitary rule set of AA* is sound and complete for every possible finite history, yet supplies no explicit inductive argument or case analysis showing how the rules capture interactions that arise only after specific sequences (e.g., a send followed by selective reception by a proper subset of agents). This step is load-bearing for the central claim that a single axiomatisation works uniformly for arbitrary histories.

    Authors: We agree that an explicit inductive argument over history length is not spelled out in Section 4. Soundness of AA* is established by induction on the length of the finite history, with the base case reducing to the soundness of AA and the inductive step using the infinitary rules to handle arbitrary send/receive sequences (including selective reception). Completeness proceeds by showing that any formula valid after a given history is derivable via the rules that quantify over all possible extensions of that history. We will insert a detailed inductive proof sketch and a case analysis for a send followed by selective reception in the revision. revision: yes

  2. Referee: [§3.2] §3.2 (Definition of AA*): the infinitary rules are introduced without accompanying proof sketches or concrete examples that verify they correctly generalise the empty-history case of AA while remaining complete once histories are non-empty. The absence of such verification leaves the correctness claim unsupported by the data in the text.

    Authors: The rules of AA* are formulated so that, when the history is empty, the infinitary rules collapse to those of AA (recovering the reduction to pure epistemic formulas). For non-empty histories the same rules remain complete by quantifying over all possible future receptions. We will add a short proof sketch of the reduction to AA in the empty-history case together with a concrete example (send of a formula followed by reception by only one agent) to illustrate the generalisation. revision: yes

Circularity Check

0 steps flagged

No significant circularity; AA* is an independent infinitary extension

full rationale

The paper explicitly separates the new infinitary axiomatisation AA* from the prior reduction system AA, noting that AA* does not validate the same formulas (e.g., 'nobody has received any message') and is not a reduction system. The central claim is a direct soundness-and-completeness argument for the generalized semantics (Kripke model plus arbitrary finite history of sends/receives). No step reduces a prediction or theorem to a fitted input, self-definition, or unverified self-citation chain; the infinitary rules are introduced to handle histories that AA cannot, and the derivation is presented as self-contained relative to the stated semantics. Self-citation of AA is acknowledged but not load-bearing for the new completeness result.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the semantic choice to interpret formulas relative to announcement histories and on the existence of an infinitary axiomatisation; the abstract introduces no free parameters, no new invented entities, and relies on standard background assumptions of modal logic.

axioms (1)
  • domain assumption Formulas are interpreted in a world of a Kripke model given a history of prior announcements and receptions that already happened.
    This semantic foundation is stated directly in the abstract as the setting for which AA* is proposed.

pith-pipeline@v0.9.0 · 5723 in / 1432 out tokens · 44029 ms · 2026-05-18T10:16:09.188357+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    Apt, Davide Grossi, and Wiebe van der Hoek

    Krzysztof R. Apt, Davide Grossi, and Wiebe van der Hoek. Epistemic protocols for distributed gossiping. Proc. of 15th TARK, 2016

    work page 2016

  2. [2]

    From public announcements to asynchronous announcements

    Philippe Balbiani, Hans van Ditmarsch, and Sa´ ul Fern´ andez Gonz´ alez. From public announcements to asynchronous announcements. In ECAI 2020 , pages 75–82. IOS Press, 2020

    work page 2020

  3. [3]

    Quantifying over asynchronous information change

    Philippe Balbiani, Hans van Ditmarsch, and Sa´ ul Fern´ andez Gonz´ alez. Quantifying over asynchronous information change. In International Conference on Advances in Modal Logic (AiML 2020), volume 13, pages 33–52. College Publications, 2020

    work page 2020

  4. [4]

    Asynchronous announcements

    Philippe Balbiani, Hans van Ditmarsch, and Sa´ ul Fern´ andez Gonz´ alez. Asynchronous announcements. ACM Transactions on Computational Logic (TOCL) , 23(2):1–38, 2022. 33

    work page 2022

  5. [5]

    Bridges between dynamic doxastic and doxastic temporal logics

    Johan van Benthem and C´ edric D´ egremont. Bridges between dynamic doxastic and doxastic temporal logics. In International Conference on Logic and the Foundations of Game and Decision Theory , pages 151–173. Springer, 2008

    work page 2008

  6. [6]

    Merging frameworks for interaction

    Johan van Benthem, Jelle Gerbrandy, Tomohiro Hoshi, and Eric Pacuit. Merging frameworks for interaction. Journal of Philosophical Logic , 38:491–526, 2009

    work page 2009

  7. [7]

    Merging frameworks for in- teraction: del and etl

    Johan van Benthem, Jelle Gerbrandy, and Eric Pacuit. Merging frameworks for in- teraction: del and etl. In Proceedings of the 11th conference on Theoretical aspects of rationality and knowledge , pages 72–81, 2007

    work page 2007

  8. [8]

    Dynamic logic of preference upgrade

    Johan van Benthem and Fenrong Liu. Dynamic logic of preference upgrade. Journal of Applied Non-Classical Logics, 17(2):157–182, 2007

    work page 2007

  9. [9]

    Bochvar and Merrie Bergmann

    Dmitri A. Bochvar and Merrie Bergmann. On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus. History and Philosophy of Logic , 2(1-2):87–112, 1981

    work page 1981

  10. [10]

    Modal weak kleene logics: axiomatizations and relational semantics

    Stefano Bonzio and Nicol` o Zamperlin. Modal weak kleene logics: axiomatizations and relational semantics. arXiv, 2024. url: https://arxiv.org/abs/2403.01274

    work page arXiv 2024

  11. [11]

    On communicating finite-state machines

    Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM (JACM) , 30(2):323–342, 1983

    work page 1983

  12. [12]

    The synchronicity of dy- namic epistemic logic

    C´ edric D´ egremont, Benedikt L¨ owe, and Andreas Witzel. The synchronicity of dy- namic epistemic logic. In Proceedings of the 13th Conference on Theoretical Aspects of Rationality and Knowledge , pages 145–152, 2011

    work page 2011

  13. [13]

    One hundred prisoners and a lightbulb-logic and computation

    Hans van Ditmarsch, Jan van Eijck, and William Wu. One hundred prisoners and a lightbulb-logic and computation. In KR Toronto, pages 90–100, 2010

    work page 2010

  14. [14]

    Dynamic epistemic logic, volume 337

    Hans van Ditmarsch, Wiebe Hoek, and Barteld Kooi van Der. Dynamic epistemic logic, volume 337. Springer Science & Business Media, 2007

    work page 2007

  15. [15]

    Halpern, Yoram Moses, and Moshe Y

    Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning about Knowledge. MIT Press, 1995. doi: 10.7551/mitpress/5803.001.0001

    work page doi:10.7551/mitpress/5803.001.0001 1995

  16. [16]

    Reasoning about information change

    Jelle Gerbrandy and Willem Groeneveld. Reasoning about information change. Jour- nal of logic, language and information , 6:147–169, 1997

    work page 1997

  17. [17]

    Halpern and Yoram Moses

    Joseph Y. Halpern and Yoram Moses. Knowledge and common knowledge in a dis- tributed environment. Journal of the ACM (JACM) , 37(3):549–587, 1990

    work page 1990

  18. [18]

    Stephen C. Kleene. Introduction to metamathematics. North-Holland Publishing Co., Amsterdam, and P. Noordhoff, Groningen, 1952

    work page 1952

  19. [19]

    Reasoning about knowledge and messages in asynchronous multi-agent systems

    Sophia Knight, Bastien Maubert, and Fran¸ cois Schwarzentruber. Reasoning about knowledge and messages in asynchronous multi-agent systems. Mathematical Struc- tures in Computer Science , 29(1):127–168, 2019

    work page 2019

  20. [20]

    Kshemkalyani and Mukesh Singhal

    Ajay D. Kshemkalyani and Mukesh Singhal. Distributed computing: principles, algo- rithms, and systems . Cambridge University Press, 2011. 34

    work page 2011

  21. [21]

    Time, clocks, and the ordering of events in a distributed system

    Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM , 21(7), 1978

    work page 1978

  22. [22]

    Revising a labelled sequent cal- culus for public announcement logic

    Shoshin Nomura, Katsuhiko Sano, and Satoshi Tojo. Revising a labelled sequent cal- culus for public announcement logic. In Structural Analysis of Non-Classical Logics: The Proceedings of the Second Taiwan Philosophical Logic Colloquium , pages 131–

    work page

  23. [23]

    Concurrent common knowledge: defining agree- ment for asynchronous systems

    Prakash Panangaden and Kim Taylor. Concurrent common knowledge: defining agree- ment for asynchronous systems. Distributed Computing, 6(2):73–93, 1992

    work page 1992

  24. [24]

    Logics of public communications

    Jan Plaza. Logics of public communications. Synthese, 158:165–179, 2007. 35 Appendix: our validities and those of [4] are the same Let ▷ ◁+ and ⊨+ denote the agreement and satisfaction relations defined in Section 2.3 and ▷ ◁− and ⊨− those defined in [4]. In this work, ▷ ◁− and ⊨− are simultaneously defined for states s, histories α and formulas φ as foll...

    work page 2007