{"@context":["https://w3id.org/fdo/context/v1",{"schema":"https://schema.org/","prov":"http://www.w3.org/ns/prov#","fdo":"https://w3id.org/fdo/vocabulary/"}],"@id":"https://fdo.portal.mardi4nfdi.de/fdo/Q310079","@type":"DigitalObject","kernel":{"@id":"https://fdo.portal.mardi4nfdi.de/fdo/Q310079","digitalObjectType":"https://schema.org/ScholarlyArticle","primaryIdentifier":"mardi:Q310079","kernelVersion":"v1","immutable":true,"modified":"2026-01-23T03:01:04Z"},"profile":{"@context":"https://schema.org","@type":"ScholarlyArticle","@id":"https://portal.mardi4nfdi.de/entity/Q310079","name":"The undecidability of quantified announcements","headline":"The undecidability of quantified announcements","description":"scientific article; zbMATH DE number 6624777","url":"https://portal.mardi4nfdi.de/entity/Q310079","datePublished":"2016-09-07","author":[{"@id":"https://portal.mardi4nfdi.de/entity/Q542136"},{"@id":"https://portal.mardi4nfdi.de/entity/Q813421"},{"@id":"https://portal.mardi4nfdi.de/entity/Q476191"}],"publisher":[{"@id":"https://portal.mardi4nfdi.de/entity/Q195358"}],"identifier":{"@type":"PropertyValue","propertyID":"doi","value":"10.1007/S11225-016-9657-0","url":"https://doi.org/10.1007/S11225-016-9657-0"},"sameAs":["https://doi.org/10.1007/S11225-016-9657-0"],"comment":"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.","citation":[{"@id":"https://portal.mardi4nfdi.de/entity/Q2500827"},{"@id":"https://portal.mardi4nfdi.de/entity/Q975877"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1258296"},{"@id":"https://portal.mardi4nfdi.de/entity/Q310079"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3455546"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3580674"},{"@id":"https://portal.mardi4nfdi.de/entity/Q2971701"},{"@id":"https://portal.mardi4nfdi.de/entity/Q391146"},{"@id":"https://portal.mardi4nfdi.de/entity/Q2901205"},{"@id":"https://portal.mardi4nfdi.de/entity/Q476194"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4845472"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3086938"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5271062"},{"@id":"https://portal.mardi4nfdi.de/entity/Q2574887"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4329525"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4342096"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5494230"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5404483"},{"@id":"https://portal.mardi4nfdi.de/entity/Q2915020"},{"@id":"https://portal.mardi4nfdi.de/entity/Q2904048"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3608740"}]},"provenance":{"prov:generatedAtTime":"2026-01-23T03:01:04Z","prov:wasAttributedTo":"MaRDI Knowledge Graph"}}