The undecidability of quantified announcements (Q310079)

The framework of the paper is expressed in the language of \mathrm{EL}, epistemic logic, consisting of formulas built over a countable set \(P\) of propositional atoms using \(\neg\), \(\wedge\) and the modalities \(K_a\) for \(a\) in a finite set \(A\) of agents, complemented with formulas of the form \([\psi]\varphi\), \([\bullet]\varphi\), \([G]\varphi\) and \([\langle G\rangle]\varphi\) with \(\psi\) an arbitrary formula in the extended language and \(G\) an arbitrary subset of \(A\), giving rise to the logics \mathrm{PAL}\ of \textit{public announcements}, \mathrm{APAL}\ of \textit{arbitrary public announcements}, \mathrm{GAL}\ of \textit{group announcements}, and \mathrm{CAL}\ of \textit{coalition announcements}, respectively. These formulas are interpreted over structures of the form \(M=(S,\sim,V)\) where \(S\) is a nonempty set of worlds, \(\sim\) assigns to each \(a\in A\) an equivalence relation \(\sim_a\) over \(S\) (the world indistinguishability relation for agent \(a\)), and \(V\) assigns to each \(p\in P\) the set of members of \(S\) in which \(p\) in true. Given such a structure \(M\) and \(s\in M\) -- a pair denoted by \(M_s\) --, the notion \(M_s\models\varphi\) is inductively defined as follows. Let \(\mathrm{EL}^G\) be the subset of \mathrm{EL}\ consisting of all formulas of the form \(\bigwedge_{a\in G}K_a\phi_a\), \(a\in G\), \(\phi_a\in\mathrm{EL}\). {\parindent=0.7cm \begin{itemize}\item[--] If \(\varphi\) is of the form \(p\in P\) then \(M_s\models\varphi\) iff \(s\in V(p)\). \item[--] If \(\varphi\) is of the form \(\neg\phi\) then \(M_s\models\varphi\) iff \(M_s\not\models\phi\). \item[--] If \(\varphi\) is of the form \(\phi_1\wedge\phi_2\) then \(M_s\models\varphi\) iff \(M_s\models\phi_1\) and \(M_s\models\phi_2\). \item[--] If \(\varphi\) is of the form \(K_a\phi\) then \(M_s\models\varphi\) iff for all \(t\in S\) with \(s\sim_a t\),\(M_t\models\phi\). \item[--] If \(\varphi\) is of the form \([\psi]\phi\) then \(M_s\models\varphi\) iff \(M_s\models\psi\) implies \(M_s^\psi\models\phi\) where \(M^\psi=(S',\sim',V')\) is such that (1) \(S' =\{s\in S\mid M_s\models\psi\}\), (2) for all \(a\in A\), \(\sim'_a =\sim_a\cap(S'\times S')\) and (3) for all \(p\in P\), \(V'(p)=V(p)\cap S'\): after the true announcement of \(\psi\), \(\phi\) will hold. \item[--] If \(\varphi\) is of the form \([\bullet]\phi\) then \(M_s\models\varphi\) iff for all \(\psi\in\mathrm{EL}\), \(M_s\models[\psi]\phi\): after publicly announcing any true formula of epistemic logic, \(\phi\) is true. \item[--] If \(\varphi\) is of the form \([G]\phi\) then \(M_s\models\varphi\) iff for all \(\psi\in\mathrm{EL}^G\), \(M_s\models[\psi]\phi\): after a group of agents (simultaneously) announce any statement they know to be true, \(\phi\) is true. \item[--] If \(\varphi\) is of the form \([\langle G\rangle]\phi\) then \(M_s\models\varphi\) iff for all \(\psi\in\mathrm{EL}^G\), there exists \(\psi'\in\mathrm{EL}^{A\setminus G}\) with \(M_s\models[\psi\wedge\psi']\phi\): after a group of agents announce any statement they know to be true, and the agents not in the group announce a ``response'' they know to be true, \(\phi\) is true. \end{itemize}} \mathrm{APAL}\ and \mathrm{GAL}\ have been shown to be undecidable, using a construction that requires five agents. In this paper, an improved construction that only requires two agents is presented, providing a complete picture of decidability for these logics as satisfiability for the single agent fragments is trivially decidable. The authors further prove the new result that \mathrm{CAL}\ is also undecidable. The proofs are based on encoding an undecidable tiling problem into the logic.