How arbitrary are arbitrary public announcements?

Abstract

Public announcements are used in dynamic epistemic logic to model certain kinds of information change. A formula 〈ψ〉φ represents the statement that after ψ is publicly announced φ will be the case. Sometimes we want to reason about whether it is possible for φ to become true after some announcement. In order to do this an arbitrary public announcement operator {white diamond suit} can be added to an epistemic logic with public announcements. Ideally a formula {white diamond suit}φ would hold if and only if there is a formula ψ such that 〈ψ〉φ. However, in order to avoid circularity the {white diamond suit} operator can only quantify over those ψ that are {white diamond suit}-free. So {white diamond suit}φ holds if and only if there is a {white diamond suit}-free ψ such that 〈ψ〉φ. As a result it does not follow immediately from the definition that 〈ψ〉φ implies {white diamond suit}φ if ψ contains a {white diamond suit}. But the implication may still hold in some cases. In this paper I show that on finite models 〈ψ〉φ implies {white diamond suit}φ for every ψ, and that on finitely branching models 〈ψ〉φ implies {white diamond suit}φ for every ψ if φ is {white diamond suit}-free. Finally I also show that there are φ and ψ such that 〈ψ〉φ does not imply {white diamond suit}φ even on a finitely branching model. © 2014 Springer-Verlag Berlin Heidelberg.