How Arbitrary Are Arbitrary Public Announcements?

Abstract

Public announcements are used in dynamic epistemic logic to model certain kinds of information change. A formula $\left<\psi\right>\varphi$ 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 $\lozenge$ can be added to an epistemic logic with public announcements. Ideally a formula $\lozenge \varphi$ would hold if and only if there is a formula ψ such that $\left<\psi\right>\varphi$. However, in order to avoid circularity the $\lozenge$ operator can only quantify over those ψ that are $\lozenge$-free. So $\lozenge \varphi$ holds if and only if there is a $\lozenge$-free ψ such that $\left<\psi\right>\varphi$.

As a result it does not follow immediately from the definition that $\left<\psi\right>\varphi$ implies $\lozenge \varphi$ if ψ contains a $\lozenge$. But the implication may still hold in some cases. In this paper I show that on finite models $\left<\psi\right>\varphi$ implies $\lozenge \varphi$ for every ψ, and that on finitely branching models $\left<\psi\right>\varphi$ implies $\lozenge \varphi$ for every ψ if ϕ is $\lozenge$-free. Finally I also show that there are ϕ and ψ such that $\left<\psi\right>\varphi$ does not imply $\lozenge \varphi$ even on a finitely branching model.