Arrow update logic is one instance of so-called dynamic epistemic logics. These are logical frameworks that allow for the modeling of change of knowledge or belief. In the special case of arrow update logics, one can in effect model that one agent gains new knowledge. This paper investigates the satisfiability problem for arbitrary arrow update logic (AAUL) and shows that the satisfiability problem of AAUL is undecidable for general Kripke models.

In the introduction, several dynamic epistemic logics are surveyed and the differences between these logics and the known results with respect to expressivity and decidability are summarized. Then, the syntax and semantics of AAUL are presented.

The main part of the paper shortly explains the tiling problem, a known undecidable problem. Then, a rather complex formula in AAUL is presented that represents the tiling problem. A series of lemmas and proofs establish that the satisfiability of this formula is equivalent to a solution to the tiling problem, and hence prove the undecidability of the satisfiability problem for AAUL.

Although the result is rather technical, the paper is very readable; space probably did not permit some examples of AAUL, but the authors’ intuitive remarks will help readers gain some basic understanding. The AAUL formula used for the reducibility is rather complex and lengthy, but the structuring of the formula and the lemmas really help in understanding the reduction proof.