Paper deep dive
Eventual and Strong Eventual Notions in Public Announcements
Eiji Yamada
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 9/22/2026, 4:26:22 AM
Summary
This paper introduces and analyzes 'eventual' and 'strong eventual' variants of four logical notions in public announcement logic: success, self-refutation, true lies, and impossible lies. It extends these concepts to transfinite iterations using ordinal numbers and establishes logical relationships between finite and transfinite versions, as well as connections to fixed-point views of Moore sentences and self-fulfilling sentences. The study utilizes Believed Public Announcement Logic (BPAL) and multi-agent K45 epistemic models.
Entities (12)
Relation Signals (7)
Moore Sentence → exemplifies → Self-Refutation
confidence 99% · the Moore sentence... is the most typical example of self-refuting formulas
Transfinite Iteration → extends → Finite Iteration
confidence 96% · transfinite versions, which allow transfinite iteration of announcements... relationship among finite and transfinite versions
Believed Public Announcement Logic → isusedin → Eventual and Strong Eventual Notions
confidence 95% · in this paper we use believed public announcement logic (BPAL)... we introduce eventual and strong eventual versions
Eventual Self-Refutation → isvariantof → Self-Refutation
confidence 95% · we introduce eventual and strong eventual versions of these notions... eventually self-refuting... strong eventual self-refutation
Success → isrelatedto → Self-Fulfilling Sentence
confidence 94% · what underlies success and true lies is the generalized form... of the self-fulfilling sentence
Strong Eventual Notions → ischaracterizedby → Limit of Truth Values
confidence 93% · strong eventual notions are characterized by the limit of the truth values of the announced formula
Eventual Notions → ischaracterizedby → Uniform Bound Condition
confidence 93% · Eventual notions are characterized by... the uniform bound condition
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:In dynamic epistemic logic, the four notions of success, self-refutation, true lies, and impossible lies have been discussed in the context of public announcements. In this paper, we introduce eventual and strong eventual versions of these notions, as well as their transfinite versions, which allow transfinite iteration of announcements. We also introduce the notions of always informativeness when true or false. For example, a formula is eventually self-refuting if, whenever initially true, it eventually becomes false at some finite stage under iterated announcements, and strong eventual self-refutation further requires the formula to remain false at all sufficiently late stages. There are two main results. The first result gives the relationship among strong eventual notions, eventual notions, and several other conditions including conditions on the limit of the truth values of the announced formula, the uniform bound condition, and the fixed-point views of the Moore sentence and the self-fulfilling sentence. The second result gives the relationship among finite and transfinite versions of the eventual and strong eventual notions and the fixed-point views.
Tags
Links
- Source: https://arxiv.org/abs/2609.24006v1
- Canonical: https://arxiv.org/abs/2609.24006v1
Trouble viewing inline? Open PDF directly →
Full Text
122,165 characters extracted from source content.
Expand or collapse full text
Eventual and Strong Eventual Notions in Public Announcements Eiji Yamada Email: yamada.e.112d@m.isct.ac.jp Affiliation: Department of Mathematical and Computing Science, Institute of Science Tokyo, Tokyo, Japan September 21, 2026 Abstract In dynamic epistemic logic, the four notions of success, self-refutation, true lies, and impossible lies have been discussed in the context of public announcements. In this paper, we introduce eventual and strong eventual versions of these notions, as well as their transfinite versions, which allow transfinite iteration of announcements. We also introduce the notions of always informativeness when true or false. For example, a formula is eventually self-refuting if, whenever initially true, it eventually becomes false at some finite stage under iterated announcements, and strong eventual self-refutation further requires the formula to remain false at all sufficiently late stages. There are two main results. The first result gives the relationship among strong eventual notions, eventual notions, and several other conditions including conditions on the limit of the truth values of the announced formula, the uniform bound condition, and the fixed-point views of the Moore sentence and the self-fulfilling sentence. The second result gives the relationship among finite and transfinite versions of the eventual and strong eventual notions and the fixed-point views. keywordsdynamic epistemic logic, public announcements, iterated announcements, Moore sentence 1 Introduction The apparent absurdity of asserting the sentence “p, but I do not believe p” was first noted by G. E. Moore in his “Reply to My Critics” (Moore, 1942). Wittgenstein called this phenomenon Moore’s paradox and made it a central problem about belief and assertion (Wittgenstein, 1953). Hintikka gave it a seminal treatment in epistemic logic (Hintikka, 1962). In that setting, the sentence is formalized as the Moore sentence φ:=p∧¬□p :=p p where □ is interpreted as knowledge or belief. From a static perspective, the Moore sentence φ is unknowable in the sense that φ∧□φ is unsatisfiable11 1 The terms knowable and believable as the satisfiability of φ∧□φ and □φ , respectively, are due to Yamada (2026b), which are static definitions. The terms unknowable and unbelievable are their negation, and they are known to be equivalent in KD45 and S5. To be precise, this definition of unknowability does not take the justification aspect of knowledge into consideration, and it rather means that there is no situation in which both φ is true and the agent believes φ . (Balbiani et al., 2008) uses the same term to mean that there is a formula ψ such that after announcing ψ, KφK holds where K means knowledge, which is dynamic.: In fact, we have φ∧□φ↔(p∧¬□p)∧□(p∧¬□p)↔(p∧¬□p)∧□p∧□¬□p↔⊥. (p p) (p p) (p p) p p . In KD45 (i.e., if agents have belief consistency, positive and negative introspections), we have the validity ◇□ψ↔□ψ ψ ψ so that φ is also unbelievable in the sense that □φ is unsatisfiable. We can also view the Moore sentence from a dynamic perspective. Public announcements are one of the main topics in dynamic epistemic logic. A public announcement of φ is an announcement to a group of agents that φ holds. In this setting, the Moore sentence φ=p∧¬□p =p p is the most typical example of self-refuting formulas, formulas that become false after being announced whenever they are initially true. In fact, whenever φ is true, after its announcement □p p holds, which in turn makes φ itself false. As a closely related yet somewhat separate topic, the notion of success has been a central topic in the study of public announcements. A formula φ is successful if, whenever φ is true, it remains true after being announced. This notion matters since success guarantees that true information is shared with others without changing its truth, which is often the purpose of announcements. Holliday and Icard (2010) proved that in single-agent S5, the notions of always informativeness, non-Cartesianness (the unsatisfiability of □φ ), and eventual self-refutation are equivalent. Yamada (2026b) then interpreted non-Cartesianness of φ as unbelievability of φ and showed that in single-agent KD45 and S5, the static notions of unknowability and unbelievability are equivalent to two different views of Moorean phenomena: One is the validity of φ↔(φ∧¬□φ) ( ) and the other is a contradiction among φ itself, the belief part and the possibility part of the disjunctive normal form of φ . Consequently in single-agent S5, those static conditions are equivalent to the dynamic notions of always informativeness and eventual self-refutation. On the other hand, (Ågotnes et al., 2018) introduced the remaining cases, true lies and impossible lies, where φ is a true lie if, whenever φ is false, it becomes true after an announcement, and φ is an impossible lie if, whenever φ is false, it remains false after an announcement (see Table 1). They extended these four notions to σ-validity for a finite or infinite sequence σ of 00s and 11s. For example, φ is 101101-valid if, whenever initially true, it becomes false after the first announcement and becomes true after the second announcement. (Yamada, 2026a) then gave a complete classification of such sequences in terms of σ-validity in multi-agent K45, KD45, and S5. Successful ⊧φ→[↑φ]φ →[ ] Self-refuting ⊧φ→[↑φ]¬φ →[ ] True lie ⊧¬φ→[↑φ]φ →[ ] Impossible lie ⊧¬φ→[↑φ]¬φ →[ ] Table 1: Four notions The idea of repeatedly announcing formulas (i.e., iterated announcements) is not new. In fact, iterated modal relativization has been studied as an epistemic program (Miller and Moss, 2005); repeated updates have been approached as dynamical systems with their own recurrence and limiting behavior (Sadzik, 2006; Klein and Rendsvig, 2017); and repeated public announcements yield fixed-point procedures in epistemic analyses of games (van Benthem, 2007). In this paper, we introduce eventual and strong eventual versions of the above four notions. We also introduce transfinite versions for these eventual and strong eventual notions. For example, we say that a formula φ is eventually self-refuting (denoted E10E_10) iff whenever φ is initially true, φ eventually becomes false at some point when repeatedly announced. Also, φ is strongly eventually self-refuting (SE10)(SE_10) iff whenever φ is initially true, φ eventually becomes false forever at some point when repeatedly announced. Finally, transfinitely eventually self-refuting (E10OrdE_10^Ord) and transfinitely strongly eventually self-refuting (SE10OrdSE_10^Ord) refer to their transfinite counterparts, allowing transfinitely repeated announcements through ordinals. We also introduce the notions of always informativeness when true and always informativeness when false, the former of which is the same as always informativeness as introduced by (Holliday and Icard, 2010). There are two main results in this paper. Theorem 13 gives, for each of the above four notions, the logical relationships among strong eventual notions, eventual notions, and several other conditions. Always informativeness when true/false are also included for self-refutation/true lies, respectively. According to the theorem, strong eventual notions are characterized by the limit of the truth values of the announced formula. Eventual notions are characterized by (i) limit superior or limit inferior of the truth values and (i) the uniform bound condition. Condition (i) claims that for any EijE_ij-formula φ (where i,j∈0,1i,j∈\0,1\), one can take a uniform bound N≥1N≥ 1 across all pointed models such that whenever the truth of φ is i, that of φ eventually becomes j by the N-th announcement. Furthermore, for (i,j)=(1,0)(i,j)=(1,0) (i.e., eventual self-refutation), all the agents’ beliefs are destroyed and become inconsistent by the N-th announcement. Eventual notions imply the fixed-point views of the sentences φ∧¬CGφ C_G and φ∨CGφ C_G (denoted Sij<ωS_ij^<ω). These conditions suggest that what underlies self-refutation and impossible lies is the generalized form φ∧¬CGφ C_G of the Moore sentence p∧¬□p p while what underlies success and true lies is the generalized form φ∨CGφ C_G of the self-fulfilling sentence p∨□p p. The theorem also implies that while every displayed one-way direction is strict when there are at least two agents, all the conditions collapse to the same notion in the single-agent case. Theorem 14 gives, for each (i,j)∈0,12(i,j)∈\0,1\^2, the logical relationship among EijE_ij, SEijSE_ij, EijOrdE_ij^Ord, SEijOrdSE_ij^Ord, Sij<ωS_ij^<ω, and SijOrdS_ij^Ord from the three perspectives: strong eventual vs eventual, finite iterated announcements vs transfinite iterated announcements, and what condition SijOrdS_ij^Ord is equivalent to. This paper is structured as follows. Section 2 introduces definitions of the usual epistemic logic, public announcement logic, believed public announcement logic, the four notions, and their basic properties. Section 3 defines eventual and strong eventual notions. Section 4 proves various lemmas for our main results. Section 5 gives our main results and their interpretations. Section 6 gives a conclusion and future work. A Lean formalization is available at https://github.com/eiyamada/lean-paper-formalizations. 2 Basic definitions and properties We first list several basic definitions. Let G be a nonempty finite set of agents and Prop be a countably infinite set of proposition letters. Definition 1. Define formulas in the multi-agent epistemic logic ℒL by φ:=p∣¬φ∣φ∧ψ|□iφ(i∈G,p∈) :=p ψ _i (i∈ G,\,p ) Definition 2 ((Plaza, 2007)). Define formulas in public announcement logic ℒPALL_PAL by φ:=p∣¬φ∣φ∧ψ∣□iφ∣[!φ]ψ(i∈G,p∈) :=p ψ _i [! ]ψ (i∈ G,\,p ) Definition 3 ((Ågotnes et al., 2018; Gerbrandy and Groeneveld, 1997)). Define formulas in believed public announcement logic ℒBPALL_BPAL by φ:=p∣¬φ∣φ∧ψ∣□iφ∣[↑φ]ψ(i∈G,p∈) :=p ψ _i [ ]ψ (i∈ G,\,p ) We let ℒCL_C and ℒBPALCL_BPALC denote the languages that add the common belief operator CGC_G to ℒL and ℒBPALL_BPAL, respectively. Definition 4. A model is a tuple M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) where W is a non-empty set of states, RiR_i is a binary relation on W (accessibility relation), and V:→2WV → 2^W is a valuation function. For a formula φ and a pointed model M,wM,w, let ⟦φ⟧M:=w∈W:M,w⊧φ _M:=\w∈ W M,w \ be the set of states in which φ holds. Definition 5. Let M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) be a model and φ be a formula. • When ⟦φ⟧M≠∅ _M≠ , the relativization of M to φ under public announcement is the model M|φ=(W|φ,Ri|φi∈G,V|φ)M_| =(W_| ,\R_i| \_i∈ G,V_| ) where W|φ=⟦φ⟧MW_| = _M, Ri|φ=Ri∩(W|φ×W|φ)R_i| =R_i∩(W_| × W_| ), and V|φ(p)=V(p)∩W|φV_| (p)=V(p)∩ W_| for all p∈p . • The relativization of M to φ under believed public announcement is the model M|φ=(W,Ri|φi∈G,V)M| =(W,\R_i| \_i∈ G,V) with Ri|φ=Ri∩(W×⟦φ⟧M)R_i| =R_i∩(W× _M). Definition 6. Let M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) be a model. Define truth as follows. 1. M,w⊧p⇔w∈V(p)M,w p w∈ V(p). 2. M,w⊧¬φ⇔M,w⊧̸φM,w M,w . 3. M,w⊧φ∧ψ⇔M,w⊧φ and M,w⊧ψM,w ψ M,w and M,w ψ. 4. M,w⊧□iφ⇔M,v⊧φM,w _i M,v for all v with wRivwR_iv. 5. M,w⊧[!φ]ψ⇔M,w⊧φ⇒M|φ,w⊧ψM,w [! ]ψ M,w M_| ,w ψ. 6. M,w⊧[↑φ]ψ⇔M|φ,w⊧ψM,w [ ]ψ M| ,w ψ. 7. M,w⊧CGφ⇔M,v⊧φM,w C_G M,v for all v with w(⋃i∈GRi)+vw( _i∈ GR_i)^+v where ++ denotes the transitive closure. Although public announcement logic (PAL) has been widely used in the literature, in this paper we use believed public announcement logic (BPAL) since in PAL, we can no longer consider the truth of formulas at states that have already been eliminated. That is, when we consider the truth of a formula φ at the pointed model M,wM,w, we can no longer consider the truth at w in the updated model M|φM_| whenever M,w⊧¬φM,w , simply because w∉M|φw∉ M_| . The expressive powers of ℒL, ℒPALL_PAL, and ℒBPALL_BPAL are known to be the same. That is, for any formula in one language, there is a logically equivalent formula in the other language. In fact, for example, the following lemma gives reduction axioms from ℒBPALL_BPAL to ℒL. The proof uses an induction on formulas. Lemma 1 (Reduction axioms for BPAL). For all formulas φ,ψ,χ ,ψ,χ, all proposition letters p, and all agents i∈Gi∈ G, the following formulas are valid: [↑φ]p [ ]p ↔p, p, [↑φ]¬ψ [ ] ψ ↔¬[↑φ]ψ, [ ]ψ, [↑φ](ψ∧χ) [ ](ψ χ) ↔([↑φ]ψ∧[↑φ]χ), ([ ]ψ [ ]χ), [↑φ]□iψ [ ] _iψ ↔□i(φ→[↑φ]ψ), _i( →[ ]ψ), [↑φ]◇iψ [ ] _iψ ↔◇i(φ∧[↑φ]ψ) _i( [ ]ψ) [↑φ][↑ψ]χ [ ][ ψ]χ ↔[↑(φ∧[↑φ]ψ)]χ. [ ( [ ]ψ)]χ. Let R∗R^* be the reflexive transitive closure of a binary relation R. Definition 7. A model M′=(W′,Ri′i∈G,V′)M =(W ,\R_i \_i∈ G,V ) is a submodel of M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) (written M′⊆M M) iff W′⊆W W, Ri′=Ri∩(W′×W′)R_i =R_i∩(W × W ) for all i∈Gi∈ G, and V′(p)=V(p)∩W′V (p)=V(p)∩ W for all p∈p . The generated submodel of M at w is the submodel MwM_w with domain v∈W:w(⋃i∈GRi)∗v\v∈ W w( _i∈ GR_i)^*v\. The following lemma states that in K45, the truth values of “modal atoms” do not change before and after moving between two states. Lemma 2. Let M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) be a K45 model. If wRivwR_iv, then for any formula φ of the form □iψ _iψ or ◇iψ _iψ, we have M,w⊧φ⟺M,v⊧φM,w M,v Proof. For φ=□iψ = _iψ, (⇒)( ) follows from transitivity and (⇐)( ) follows from Euclideanness. For φ=◇iψ = _iψ, the order of the properties is reversed. ∎ From the perspective of model stabilization under believed public announcements, transfinite iteration is a natural extension of finite iteration. Beyond its mathematical role, it may also admit meaningful epistemic or communicative interpretations, a possibility we leave for future investigation (cf. (van Benthem, 2007, Sections 1.2, 2.4, 5.1–5.4, and 6.2), where higher-order reasoning about players’ rationality motivates iterative strategy elimination, and transfinite approximation connects the resulting epistemic processes to fixed points characterizing game-theoretic solution concepts such as rationalizability). Definition 8. Let M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) be a model. For each ordinal α, recursively define the model M|αφ=Mα=(W,Ri|αφi∈G,V)M|^α =M^α=(W,\R_i|^α \_i∈ G,V) by: 1. Ri|0φ=RiR_i|^0 =R_i 2. Ri|α+1φ=(Ri|αφ)|φR_i|^α+1 =(R_i|^α )| 3. For limit ordinal λ, Ri|λφ=⋂α<λRi|αφR_i|^λ = _α<λR_i|^α . The following proposition states that after sufficiently many (possibly transfinite) iterations, the model stabilizes and the announced formula becomes common belief. Proposition 3. Let φ be a formula. For all models M, there is an ordinal α such that Mα=Mα+1M^α=M^α+1. Furthermore, this α satisfies Mα,w⊧CGφM^α,w C_G for all w∈Mw∈ M. Proof. Let E=(i,u,v):i∈G,(u,v)∈RiE=\(i,u,v) i∈ G,\,(u,v)∈ R_i\ be the set of all labelled arrows of M. Put κ=|E|κ=|E|, and fix an enumeration without repetition E=eξ:ξ<κE=\e_ξ:ξ<κ\. For each ordinal β, let Eβ=(i,u,v):i∈G,(u,v)∈RiβE^β=\(i,u,v):i∈ G,\ (u,v)∈ R_i^β\ be the labelled arrows remaining in MβM^β. Suppose, for a contradiction, that Mβ≠Mβ+1M^β≠ M^β+1 for every β<κ+β<κ^+. Then Eβ∖Eβ+1≠∅E^β E^β+1≠ , so define f:κ+⟶κ,f(β)=minξ<κ:eξ∈Eβ∖Eβ+1.f:κ^+ κ, f(β)= \ξ<κ:e_ξ∈ E^β E^β+1\. Thus, f(β)f(β) is the index of the first arrow deleted at stage β. To check injectivity, let β<γ<κ+β<γ<κ^+. Since the arrow sets decrease, ef(γ)∈Eγ⊆Eβ+1,ef(β)∉Eβ+1.e_f(γ)∈ E^γ E^β+1, e_f(β)∉ E^β+1. Hence f(β)≠f(γ)f(β)≠ f(γ). This gives the impossible injection from κ+κ^+ into κ. Hence Mα=Mα+1M^α=M^α+1 for some α<|E|+α<|E|^+. Mα,w⊧CGφM^α,w C_G is immediate from the transitive closure style definition of CGC_G. ∎ Definition 9 ((Ågotnes et al., 2018)). Let φ be a formula. • φ is successful iff φ→[↑φ]φ →[ ] is valid. • φ is self-refuting iff φ→[↑φ]¬φ →[ ] is valid. • φ is a true lie iff ¬φ→[↑φ]φ →[ ] is valid. • φ is an impossible lie iff ¬φ→[↑φ]¬φ →[ ] is valid. Example 1. We show that φ:=p∨□p :=p p (“p is true or the agent believes p”) is a true lie in K45. Suppose that M,w⊧¬(p∨□p)M,w (p p). Then, we have M,w⊧¬p∧¬□pM,w p p. Take any v∈R|φ(w)v∈ R| (w). Then, M,v⊧p∨□pM,v p p but by Lemma 2, we also have M,v⊧¬□pM,v p. Thus, we must have M,v⊧pM,v p so M|φ,w⊧□pM| ,w p hence M|φ,w⊧φM| ,w . In this paper, we call this formula the self-fulfilling sentence. 3 Eventual and strong eventual notions In this section, we introduce, for each i,j∈0,1i,j∈\0,1\, eventual (Eij)(E_ij) and strong eventual (SEijSE_ij) variants and their transfinite versions (EijOrdE_ij^Ord and SEijOrdSE_ij^Ord). We also introduce always informativeness when true/false (AIiAI_i) and the SijS_ij conditions. Unless otherwise stated, all models considered below are multi-agent K45 models, and validity and satisfiability are understood relative to this class. Definition 10. For b∈0,1b∈\0,1\, write φ1:=φ ^1:= and φ0:=¬φ ^0:= . For i,j∈0,1i,j∈\0,1\: When φ is fixed, we abbreviate M|αφM|^α by MαM^α. Eij(φ) E_ij( ) :⟺∀M,w(M,w⊧φi⇒∃n≥1Mn,w⊧φj), : ∀ M,w\, (M,w ^i ∃ n≥ 1\;M^n,w ^j ), SEij(φ) SE_ij( ) :⟺∀M,w(M,w⊧φi⇒∃N≥1∀n≥NMn,w⊧φj), : ∀ M,w\, (M,w ^i ∃ N≥ 1\;∀ n≥ N\;M^n,w ^j ), EijOrd(φ) E^Ord_ij( ) :⟺∀M,w(M,w⊧φi⇒∃α>0Mα,w⊧φj), : ∀ M,w\, (M,w ^i ∃α>0\;M^α,w ^j ), SEijOrd(φ) SE^Ord_ij( ) :⟺∀M,w(M,w⊧φi⇒∃α>0∀β≥αMβ,w⊧φj), : ∀ M,w\, (M,w ^i ∃α>0\;∀β≥α\;M^β,w ^j ), AIi(φ) AI_i( ) :⟺∀M,w(M,w⊧φi⇒(M|φ)w≠Mw). : ∀ M,w\, (M,w ^i (M| )_w≠ M_w ). For k<ωk<ω, write Sij(k,φ) S_ij(k, ) :⟺⊧φi→[↑φ]k(CGφ→φj), : ^i→[ ]^k(C_G → ^j), Sij<ω(φ) S^<ω_ij( ) :⟺∀k<ωSij(k,φ), : ∀ k<ω\;S_ij(k, ), SijOrd(φ) S^Ord_ij( ) :⟺∀M,w,α(M,w⊧φi∧Mα,w⊧CGφ⇒Mα,w⊧φj) : ∀ M,w,α\, (M,w ^i M^α,w C_G M^α,w ^j ) where α ranges over the ordinals. When the formula argument is omitted, the symbols above denote the corresponding classes of formulas. We use the terms eventually successful, strongly eventually successful, transfinitely eventually successful, transfinitely strongly eventually successful, eventually self-refuting, strongly eventually self-refuting, transfinitely eventually self-refuting, transfinitely strongly eventually self-refuting, eventual true lie, strong eventual true lie, transfinite eventual true lie, transfinite strong eventual true lie, eventual impossible lie, strong eventual impossible lie, transfinite eventual impossible lie, transfinite strong eventual impossible lie, always informative when true, and always informative when false in the obvious manner. In K45, a formula φ cannot be both always informative when true and always informative when false. In fact, according to Theorem 13, AI1(φ)⟺⊧CGφ→¬φandAI0(φ)⟺⊧CGφ→φ,AI_1( ) C_G → AI_0( ) C_G → , so they together imply ⊧¬CGφ C_G . However, the single-state model with empty accessibility relations is indeed K45 and the state vacuously satisfies CGφC_G . Note that the situation differs in KD45 and S5 since empty accessibility relations are not allowed: in such frames, we could possibly say something like “φ is commonly unbelievable/unknowable.” Also, although it is possible to define “φ is transfinitely always informative when true/false” as ∀M,w,α(Mα,w⊧φi⇒(Mα+1)w≠(Mα)w),∀ M,w,α (M^α,w ^i (M^α+1)_w≠(M^α)_w), this immediately reduces to the same notion as “φ is always informative when true/false” since K45 is closed under updates. Finally, for a formula φ , a pointed model M,wM,w, and n<ωn<ω, put σnM,w(φ):=1if M|nφ,w⊧φ,0if M|nφ,w⊧¬φ. _n^M,w( ):= cases1&if M|^n ,w ,\\ 0&if M|^n ,w . cases For readability, we write σnM,w _n^M,w for σnM,w(φ) _n^M,w( ). 4 Lemmas for the main results Lemma 4. Let φ be a basic multi-agent epistemic formula, M be a model, and w∈Mw∈ M. (1) (M|φ)w=Mw(M| )_w=M_w iff M,w⊧CGφM,w C_G . (2) For all i,j∈0,1i,j∈\0,1\, Eij(φ)E_ij( ) implies Sij<ω(φ)S_ij^<ω( ). Moreover, AIi(φ)AI_i( ), Si,1−i<ω(φ)S_i,1-i^<ω( ), and ⊧CGφ→φ1−i C_G → ^1-i are equivalent. (3) For all i,j∈0,1i,j∈\0,1\, Eij(φ)E_ij( ) is equivalent to the existence of N≥1N≥ 1 such that ⊧φi→⋁n=1N[↑φ]nφj. ^i→ _n=1^N[ ]^n ^j. (4) E10(φ)E_10( ), SE10(φ)SE_10( ), and the following condition are equivalent: there is an n≥1n≥ 1 such that ⊧[↑φ]n(¬φ∧⋀i∈G□i⊥). [ ]^n ( _i∈ G _i ). Proof. (1) Suppose M,w⊧CGφM,w C_G . Every arrow in MwM_w has a target reachable from w by a nonempty G-path, and that target therefore satisfies φ . Hence no arrow in MwM_w is deleted, so (M|φ)w=Mw(M| )_w=M_w. Conversely, suppose (M|φ)w=Mw(M| )_w=M_w. Every nonempty G-path from w in M then remains after the update. The target of its final arrow must therefore satisfy φ in M. Thus M,w⊧CGφM,w C_G . (2) For Eij(φ)⇒Sij<ω(φ)E_ij( ) S_ij^<ω( ), suppose Eij(φ)E_ij( ) and suppose toward a contradiction that Sij(k,φ)S_ij(k, ) fails. Then, there are M,wM,w such that M,w⊧φiM,w ^i and Mk,w⊧CGφ∧φ1−jM^k,w C_G ^1-j for some k. By (1), the value 1−j1-j is permanent from that stage on. If i≠ji≠ j, then 1−j=i1-j=i, so applying EijE_ij to MkM^k yields a contradiction. If i=ji=j, let m<km<k be the last stage before k such that M|m,w⊧φiM|^m,w ^i. Then, applying EiiE_i yields a contradiction since 1−j≠i1-j≠ i. Hence EijE_ij implies every Sij(k)S_ij(k). Next, we show equivalence among AIi(φ)AI_i( ), Si,1−i<ω(φ)S_i,1-i^<ω( ), and ⊧CGφ→φ1−i C_G → ^1-i. Recall that AIi(φ)⟺∀M,w(M,w⊧φi⇒(M|φ)w≠Mw)AI_i( ) ∀ M,w\, (M,w ^i (M| )_w≠ M_w ). Thus, by (1), AIi(φ)AI_i( ) is equivalent to ⊧φi→¬CGφ ^i→ C_G , which is propositionally equivalent to ⊧CGφ→φ1−i C_G → ^1-i. For Si,1−i<ω(φ)S_i,1-i^<ω( ) to ⊧CGφ→φ1−i C_G → ^1-i, note that Si,1−i<ω(φ)⟺∀k<ω,⊧φi→[↑φ]k(CGφ→φ1−i)S_i,1-i^<ω( ) ∀ k<ω,\, ^i→[ ]^k(C_G → ^1-i). So, taking k=0k=0 yields ⊧φi→(CGφ→φ1−i) ^i→(C_G → ^1-i), which is propositionally equivalent to ⊧CGφ→φ1−i C_G → ^1-i. Conversely, ⊧CGφ→φ1−i C_G → ^1-i clearly gives Si,1−i<ω(φ)S_i,1-i^<ω( ) since K45 is closed under updates. (3) The right-to-left implication is immediate from the definition of Eij(φ)E_ij( ). For the converse, suppose Eij(φ)E_ij( ) holds and that no such uniform bound exists. Then, for every N≥1N≥ 1, the formula φi∧⋀n=1N[↑φ]nφ1−j ^i _n=1^N[ ]^n ^1-j is K45-satisfiable. Since BPAL is reducible to the basic epistemic language, compactness of K45 yields a pointed model M,wM,w such that M,w⊧φiM,w ^i and Mn,w⊧φ1−jM^n,w ^1-j for every n≥1n≥ 1. This contradicts Eij(φ)E_ij( ). (4) We first show that E10(φ)E_10( ) implies ⊧[↑φ]n(¬φ∧⋀i∈G□i⊥) [ ]^n ( _i∈ G _i ). Suppose E10E_10. By (3), there is an N≥1N≥ 1 such that ⊧φ→⋁m=1N[↑φ]m¬φ. → _m=1^N[ ]^m . We now show ⊧[↑φ]N+1(¬φ∧⋀i∈G□i⊥) [ ]^N+1 ( _i∈ G _i ). Take any model M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) and w∈Mw∈ M. We first show M,w⊧[↑φ]N+1⋀i∈G□i⊥M,w [ ]^N+1 _i∈ G _i . That is, every agent’s relation is empty after the N+1N+1-th announcement. Suppose, towards a contradiction, that x(Ri|N+1φ)yx(R_i|^N+1 )y for some i∈Gi∈ G and x,y∈Mx,y∈ M. Then, since an arrow survives from stage m to stage m+1m+1 only if its target satisfies φ at stage m, we get M|mφ,y⊧φM|^m ,y for every 0≤m≤N0≤ m≤ N. However, this contradicts the earlier claim, so that we have ⊧[↑φ]N+1⋀i∈G□i⊥ [ ]^N+1 _i∈ G _i . We finally show M,w⊧[↑φ]N+1¬φM,w [ ]^N+1 . Suppose toward a contradiction that M|N+1φ,w⊧φM|^N+1 ,w . Since the model is edgeless, further announcements of φ do not change it. Hence M|N+1+mφ,w⊧φM|^N+1+m ,w for every m<ωm<ω. However, applying E10(φ)E_10( ) to the pointed K45 model M|N+1φ,wM|^N+1 ,w gives a contradiction. Therefore, we have ⊧[↑φ]N+1(¬φ∧⋀i∈G□i⊥). [ ]^N+1 ( _i∈ G _i ). Conversely, suppose that ⊧[↑φ]n(¬φ∧⋀i∈G□i⊥) [ ]^n ( _i∈ G _i ) for some n≥1n≥ 1. Then after n announcements the model is edgeless and φ is false everywhere. Since an edgeless model is unchanged by every further believed public announcement, φ remains false at all later stages. Thus SE10(φ)SE_10( ) holds. Finally, SE10(φ)SE_10( ) implies E10(φ)E_10( ) immediately from the definitions. ∎ Lemma 5. Let φ be a basic multi-agent epistemic formula. For every i,j∈0,1i,j∈\0,1\ we have SEij⇒Eij⇒EijOrd⇒Sij<ωSE_ij E_ij E_ij^Ord S_ij^<ω, SEijOrd⇒EijOrdSE_ij^Ord E_ij^Ord, and SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord. For i≠ji≠ j, EijOrdE_ij^Ord, SEijOrdSE_ij^Ord, SijOrdS_ij^Ord, and Sij<ωS_ij^<ω are equivalent. Proof. Most of the displayed implications follow immediately from the definitions: SEij⇒Eij⇒EijOrdSE_ij E_ij E_ij^Ord and SEijOrd⇒EijOrdSE_ij^Ord E_ij^Ord. Thus it remains to prove three facts: EijOrd⇒Sij<ωE_ij^Ord S_ij^<ω, SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord, and, when i≠ji≠ j, Sij<ω⇒SEijOrdS_ij^<ω SE_ij^Ord. Proof of EijOrd⇒Sij<ωE_ij^Ord S_ij^<ω. We first prove EijOrd⇒Sij<ωE_ij^Ord S_ij^<ω. Fix k<ωk<ω and suppose, towards a contradiction, that Sij(k,φ)S_ij(k, ) fails. Then there are a K45 model M and a state w such that M,w⊧φiM,w ^i and Mk,w⊧CGφ∧φ1−jM^k,w C_G ^1-j. By Lemma 4(1), the generated model at w is fixed from stage k onward. Hence Mα,w⊧φ1−jfor every α≥k.M^α,w ^1-j every α≥ k. Suppose first that i≠ji≠ j. Since i,j∈0,1i,j∈\0,1\, we have i=1−ji=1-j, so Mk,w⊧φiM^k,w ^i. Applying EijOrd(φ)E_ij^Ord( ) to the pointed tail model Mk,wM^k,w requires φj ^j to hold at some later ordinal stage. This is impossible because φ1−j ^1-j is permanent from stage k onward. Now suppose that i=ji=j. Since φi ^i holds at stage 00 and φ1−i ^1-i holds at stage k, we have k>0k>0. Let m<km<k be the last finite stage before k at which Mm,w⊧φiM^m,w ^i. Then Mn,w⊧φ1−ifor every m<n≤k.M^n,w ^1-i every m<n≤ k. Moreover, φ1−i ^1-i is permanent from stage k onward by the preceding argument. Thus the tail beginning at Mm,wM^m,w never returns to the value i at any positive ordinal stage, contradicting EiiOrd(φ)E_i^Ord( ). Therefore Sij(k,φ)S_ij(k, ) holds for every k<ωk<ω, and hence EijOrd(φ)⇒Sij<ω(φ)E_ij^Ord( ) S_ij^<ω( ). Proof of SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord. We next prove SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord. Suppose first that SijOrd(φ)S_ij^Ord( ) holds, and let M,w⊧φiM,w ^i. By Proposition 3, there is an ordinal λ such that Mλ=Mλ+1M^λ=M^λ+1 and Mλ,w⊧CGφM^λ,w C_G . Hence, by SijOrd(φ)S_ij^Ord( ), we have Mλ,w⊧φjM^λ,w ^j. Since MλM^λ is a fixed point, this truth value is permanent at all later stages. Thus SEijOrd(φ)SE_ij^Ord( ) holds. If λ=0λ=0, we may use stage 11 as the positive witnessing ordinal. Conversely, suppose that SEijOrd(φ)SE_ij^Ord( ) holds. Let M,w⊧φiM,w ^i, and suppose that for some ordinal α, Mα,w⊧CGφM^α,w C_G . By Lemma 4(1), the generated model at w is fixed from stage α onward. Hence the truth value of φ at w is also permanent from stage α onward. If Mα,w⊧φ1−jM^α,w ^1-j, then Mβ,w⊧φ1−jM^β,w ^1-j for every β≥αβ≥α, which contradicts SEijOrd(φ)SE_ij^Ord( ). Therefore Mα,w⊧φjM^α,w ^j, and so SijOrd(φ)S_ij^Ord( ) holds. Thus, we have proved SijOrd(φ)⟺SEijOrd(φ)S_ij^Ord( ) SE_ij^Ord( ). Proof of the equivalence when i≠ji≠ j. Finally, suppose that i≠ji≠ j. Then j=1−ij=1-i, and Lemma 4(2) gives Sij<ω(φ)⟺⊧CGφ→φj.S_ij^<ω( ) C_G → ^j. Assume Sij<ω(φ)S_ij^<ω( ) and let M,w⊧φiM,w ^i. Choose a fixed stage λ by Proposition 3. Since Mλ,w⊧CGφM^λ,w C_G , the displayed validity gives Mλ,w⊧φjM^λ,w ^j. As the model is fixed from stage λ onward, φj ^j remains true forever. Hence SEijOrd(φ)SE_ij^Ord( ) holds. Combining this implication with SEijOrd⇒EijOrd⇒Sij<ωSE_ij^Ord E_ij^Ord S_ij^<ω and with SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord, we obtain, for i≠ji≠ j, EijOrd⟺SEijOrd⟺SijOrd⟺Sij<ωE_ij^Ord SE_ij^Ord S_ij^Ord S_ij^<ω. ∎ Lemma 6. In single-agent K45, Mw|nφ=Mw|n+1φM_w|^n =M_w|^n+1 for some n≥1n≥ 1. Consequently, SEijSE_ij, EijE_ij, SEijOrdSE_ij^Ord, EijOrdE_ij^Ord, SijOrdS_ij^Ord, and Sij<ωS_ij^<ω are equivalent for every i,j∈0,1i,j∈\0,1\. Proof. Let M=(W,R,V),wM=(W,R,V),w be a pointed K45 model, and let P be the finite set of proposition letters occurring in φ . Put Sn:=(R|nφ)(w)S_n:=(R|^n )(w). We first show that the generated model at w reaches a fixed point after finitely many announcements. In a transitive and Euclidean frame, xRyxRy implies R(x)=R(y)R(x)=R(y) and yRyyRy. Hence, for every y∈S0y∈ S_0, we have R(y)=S0R(y)=S_0. Since believed public announcement only restricts the targets of arrows, induction on n gives Rn(y)=SnR^n(y)=S_n for every y∈S0y∈ S_0. Now let x,y∈S0x,y∈ S_0 have the same P-valuation. We claim that, for every n<ωn<ω, Mn,x⊧φM^n,x iff Mn,y⊧φM^n,y . More generally, the same holds for every subformula of φ . This follows by induction on the construction of formulas. The propositional and Boolean cases are immediate. For the modal case, x and y have the same successor set SnS_n, so, for example, Mn,x⊧□ψM^n,x ψ iff every state in SnS_n satisfies ψ, iff Mn,y⊧□ψM^n,y ψ. Therefore, whenever Sn+1⊊SnS_n+1 S_n, at least one entire P-valuation type disappears from the successor set. Indeed, if y∈Sn∖Sn+1y∈ S_n S_n+1, then Mn,y⊧¬φM^n,y , and every state in SnS_n with the same P-valuation as y also satisfies ¬φ and is deleted as a target at the next update. Since there are at most 2|P|2^|P| P-valuation types, the successor set can strictly decrease only finitely many times. Hence there is some k<ωk<ω such that Sk=Sk+1S_k=S_k+1. It follows that the generated model at w is fixed from stage k onward. By Lemma 4(1), Mk,w⊧CGφM^k,w C_G . We now prove the collapse of the six notions. Suppose first that Sij<ω(φ)S_ij^<ω( ) holds and that M,w⊧φiM,w ^i. Choose a finite fixed stage k as above. Since Sij(k,φ)S_ij(k, ) holds, we have Mk,w⊧CGφ→φjM^k,w C_G → ^j. As Mk,w⊧CGφM^k,w C_G , it follows that Mk,w⊧φjM^k,w ^j. The generated model is fixed from stage k onward, so Mn,w⊧φjM^n,w ^j for every n≥kn≥ k, and indeed Mα,w⊧φjM^α,w ^j for every ordinal α≥kα≥ k. Thus Sij<ω(φ)S_ij^<ω( ) implies both SEij(φ)SE_ij( ) and SEijOrd(φ)SE_ij^Ord( ). Combining this with the general implications SEij⇒Eij⇒EijOrd⇒Sij<ωSE_ij E_ij E_ij^Ord S_ij^<ω, with SEijOrd⇒EijOrdSE_ij^Ord E_ij^Ord, and with SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord (see Lemma 5), we obtain SEij⟺Eij⟺SEijOrd⟺EijOrd⟺SijOrd⟺Sij<ω.SE_ij E_ij SE_ij^Ord E_ij^Ord S_ij^Ord S_ij^<ω. ∎ Lemma 7. If |G|≥2|G|≥ 2, then S10<ω⇏E10S_10^<ω E_10 and S01<ω⇏E01S_01^<ω E_01. Proof. We construct two basic formulas θ10 _10 and θ01 _01 such that θ10∈S10<ω∖E10 _10∈ S_10^<ω E_10 and θ01∈S01<ω∖E01 _01∈ S_01^<ω E_01. Choose distinct agents a,b∈Ga,b∈ G and atoms r,sr,s. For any formula χ, define Lχ:=(s∧◇a(¬s∧χ))∨(¬s∧◇b(s∧χ)),D:=L⊤.Lχ:=(s _a( s χ)) ( s _b(s χ)), D:=L . Put θ10:=D∧L¬D _10:=D L D. Also put ψ:=¬r∧Dψ:= r D and θ01:=ψ∨(□aψ∧□bψ) _01:=ψ ( _aψ _bψ). Proof of S10<ω(θ10)S_10^<ω( _10) and S01<ω(θ01)S_01^<ω( _01) We first prove S10<ω(θ10)S_10^<ω( _10) and S01<ω(θ01)S_01^<ω( _01). Take any pointed model M,xM,x. Suppose that M,x⊧θ10M,x _10. Then L¬DL D holds at x, so there is an a- or b-successor y such that M,y⊧¬DM,y D. Hence M,y⊧¬θ10M,y _10. Thus ⊧θ10→¬CGθ10 _10→ C_G _10, or equivalently, ⊧CGθ10→¬θ10 C_G _10→ _10. By Lemma 4(2), S10<ω(θ10)S_10^<ω( _10). For θ01 _01, suppose that M,x⊧¬θ01M,x _01. Then M,x⊧¬ψM,x ψ and M,x⊧¬□iψM,x _iψ for some i∈a,bi∈\a,b\. Choose y such that xRiyxR_iy and M,y⊧¬ψM,y ψ. Since RiR_i is transitive and Euclidean, xRiyxR_iy implies yRiyyR_iy. Therefore M,y⊧¬□iψM,y _iψ, and hence M,y⊧¬θ01M,y _01. Thus ⊧¬θ01→¬CGθ01 _01→ C_G _01, or equivalently, ⊧CGθ01→θ01 C_G _01→ _01. Again by Lemma 4(2), S01<ω(θ01)S_01^<ω( _01). Proof of θ10∉E10 _10∉ E_10 and θ01∉E01 _01∉ E_01 It remains to show that θ10∉E10 _10∉ E_10 and θ01∉E01 _01∉ E_01. We use one common model. Let W consist of the empty sequence ϵε together with all nonempty finite strictly decreasing sequences of natural numbers. Define the rank by ρ(ϵ)=ωρ(ε)=ω and, for a nonempty sequence σ, let ρ(σ)ρ(σ) be its last entry. For each σ, let Cσ:=σ⌢q:q<ρ(σ)C_σ:=\σ q:q<ρ(σ)\ where σ⌢qσ q denotes the sequence obtained by appending q to σ. Thus CσC_σ is the set of children of σ. For example, Cϵ=⟨0⟩,⟨1⟩,…C_ε=\ 0 , 1 ,…\ and C⟨2⟩=⟨2,0⟩,⟨2,1⟩C_ 2 =\ 2,0 , 2,1 \. Let s hold exactly at sequences of even length and let r hold only at ϵε. Define Ra:=⋃|σ| even(σ∪Cσ)×Cσ,Rb:=⋃|σ| odd(σ∪Cσ)×Cσ,R_a:= _|σ| even(\σ\∪ C_σ)× C_σ, R_b:= _|σ| odd(\σ\∪ C_σ)× C_σ, and interpret every other agent relation as empty. For each agent, these relations are disjoint unions of blocks of the form X×CX× C with C⊆XC X. Each such block is transitive and Euclidean, so the resulting model is K45 (see Figure 1). In this model, LχLχ simply says that some child one level below satisfies χ. In particular, D=L⊤D=L holds exactly when at least one child remains accessible. Thus D detects whether the current block still has a surviving target. For a sequence σ, write ι(σ)=a (σ)=a if |σ||σ| is even and ι(σ)=b (σ)=b if |σ||σ| is odd. Also put Cσn:=σ⌢q:n≤q<ρ(σ)C_σ^n:=\σ q:n≤ q<ρ(σ)\. We first analyze iteration by θ10 _10, writing M10n:=M|nθ10M_10^n:=M|^n _10. We claim that, for every n<ωn<ω, every σ, and every x∈σ∪Cσx∈\σ\∪ C_σ, Rι(σ)M10n(x)=Cσn.R_ (σ)^M_10^n(x)=C_σ^n. At the same time, for every finite-rank σ, M10n,σ⊧D⟺M10n,σ⊧θ10⟺n<ρ(σ).M_10^n,σ D M_10^n,σ _10 n<ρ(σ). The statement Rι(σ)M10n(x)=CσnR_ (σ)^M_10^n(x)=C_σ^n means that, at each finite stage, every block is peeled from left to right according to rank: after n announcements, precisely the targets of rank at least n remain accessible. These statements follow simultaneously by induction on n. The relation statement is immediate for n=0n=0. Suppose it holds at stage n. Since the ι(σ) (σ)-successors of σ are precisely the members of CσnC_σ^n, D holds at σ exactly when n<ρ(σ)n<ρ(σ). If n<ρ(σ)n<ρ(σ), the child σ⌢nσ n is still accessible. Its rank is n, so it has no child of rank at least n and hence falsifies D at stage n. Thus it witnesses L¬DL D, and θ10 _10 holds at σ. Conversely, if n≥ρ(σ)n≥ρ(σ), then D, and therefore θ10 _10, is false at σ. Consequently a child σ⌢qσ q survives as a target from stage n to stage n+1n+1 exactly when n<qn<q, giving Cσn+1C_σ^n+1. This completes the induction. Now consider the root ϵε. Since ρ(ϵ)=ωρ(ε)=ω, at every finite stage n the child ⟨n⟩ n is still accessible and witnesses L¬DL D. Hence M10n,ϵ⊧θ10for every n<ω.M_10^n,ε _10 every n<ω. In particular, θ10 _10 is initially true at ϵε but never becomes false at any positive finite stage. Therefore θ10∉E10 _10∉ E_10. Notice also that every arrow target has finite rank, so all arrows disappear at stage ω; the root trajectory is 1,1,1,…,0ω,0ω+1,….1,1,1,…,0_ω,0_ω+1,…. We next analyze iteration by θ01 _01, writing M01n:=M|nθ01M_01^n:=M|^n _01. The key observation is that θ01 _01 and ψ agree at every current arrow target. Indeed, if y is a target of an i-arrow and ψ is false at y, then K45 gives yRiyyR_iy, so □iψ _iψ is false at y and hence θ01 _01 is false there. The converse is immediate because ψ is a disjunct of θ01 _01. Thus, at every current arrow target, θ01 _01 holds iff ψ holds. No arrow in our model targets the root, so r is false at every arrow target. Hence, at every arrow target, ψ holds iff D holds. It follows by induction, exactly as above, that Rι(σ)M01n(x)=CσnR_ (σ)^M_01^n(x)=C_σ^n for every n<ωn<ω, every σ, and every x∈σ∪Cσx∈\σ\∪ C_σ. At the root ϵε, ψ is false at every stage because r is true there. At every finite stage n, the root still has the a-successor ⟨n⟩ n . This state has rank n, so D, and therefore ψ, is false there at stage n. Hence □aψ _aψ is false at the root and M01n,ϵ⊧¬θ01for every n<ω.M_01^n,ε _01 every n<ω. Thus θ01 _01 is initially false at the root but never becomes true at any positive finite stage. Therefore θ01∉E01 _01∉ E_01. At stage ω, all arrows have disappeared. Since ψ is still false at the root while both □aψ _aψ and □bψ _bψ are vacuously true, θ01 _01 becomes true there. Its root trajectory is therefore 0,0,0,…,1ω,1ω+1,….0,0,0,…,1_ω,1_ω+1,…. We have thus constructed θ10∈S10<ω∖E10 _10∈ S_10^<ω E_10 and θ01∈S01<ω∖E01 _01∈ S_01^<ω E_01. Hence S10<ω⇏E10S_10^<ω E_10 and S01<ω⇏E01S_01^<ω E_01 for every |G|≥2|G|≥ 2. ∎ ϵερ(ϵ)=ωρ(ε)= ⟨0⟩ 0 ⟨1⟩ 1 ⟨2⟩ 2 ⟨3⟩ 3 ⟨4⟩ 4 ⋯·s⟨1,0⟩ 1,0 ⟨2,0⟩ 2,0 ⟨2,1⟩ 2,1 ⟨3,0⟩ 3,0 ⟨3,1⟩ 3,1 ⟨3,2⟩ 3,2 ⟨4,0⟩ 4,0 ⟨4,1⟩ 4,1 ⟨4,2⟩ 4,2 ⟨4,3⟩ 4,3 ⟨2,1,0⟩ 2,1,0 ⟨3,1,0⟩ 3,1,0 ⟨3,2,0⟩ 3,2,0 ⟨3,2,1⟩ 3,2,1 ⟨3,2,1,0⟩ 3,2,1,0 ¬s s¬s s Figure 1: The two-agent rank-peeling model. Blue arrows are RaR_a-arrows and red arrows are RbR_b-arrows. Horizontal colored segments schematically indicate the Euclidean accessibility among targets in the same block. Transitive arrows and reflexive arrows are omitted. Definition 11 (Two-peeling model). Choose distinct agents a,b∈Ga,b∈ G. Let H:=um,0∣m∈ωH:=\u_m,0 m∈ω\, and define the model M=(W,Rii∈G,V)M=(W,\R_i\_i∈ G,V) by W:=w∪um,j∣m∈ω, 0≤j≤2m+1,W:=\w\∪\u_m,j m∈ω,\ 0≤ j≤ 2m+1\, Ra:=(w∪H)×H∪⋃m∈ω⋃0≤j≤2mjoddum,j,um,j+1×um,j+1,R_a:=(\w\∪ H)× H\;∪\; _m∈ω _ subarrayc0≤ j≤ 2m\\ j\ odd subarray\u_m,j,u_m,j+1\×\u_m,j+1\, Rb:=⋃m∈ω⋃0≤j≤2mjevenum,j,um,j+1×um,j+1,R_b:= _m∈ω _ subarrayc0≤ j≤ 2m\\ j\ even subarray\u_m,j,u_m,j+1\×\u_m,j+1\, and Rc:=∅R_c:= for every c∈G∖a,bc∈ G \a,b\. The valuation is given by V(r):=w,V(r):=\w\, V(s):=um,j∣m∈ω, 0≤j≤2m+1,jodd,V(s):=\u_m,j m∈ω,\ 0≤ j≤ 2m+1,\ j\ odd\, V(p):=um,0∣m∈ω,meven,V(p):=\u_m,0 m∈ω,\ m\ even\, and V(t):=H,V(u):=u0,0.V(t):=H, V(u):=\u_0,0\. For every proposition letter q∉r,s,p,t,uq∉\r,s,p,t,u\, let V(q):=∅V(q):= (See Figure 2(a)). The components of each relation are disjoint and every non-empty component has a common target set, so the model is K45. Lemma 8. If |G|≥2|G|≥ 2, E11∖SE11E_11 SE_11 is nonempty. Moreover, E01 E01E_01 SE_01 is also nonempty. Proof. Let D D :=(s∧◇a(¬r∧¬s))∨(¬s∧◇b(¬r∧s)), :=(s _a( r s)) ( s _b( r s)), A A :=¬r∧□b(r∨D),Z:=◇a(¬r∧¬s∧p∧¬A), := r _b(r D), Z:= _a( r s p A), DA D^A :=(s∧◇a(A∧¬r∧¬s))∨(¬s∧◇b(A∧¬r∧s)), :=(s _a(A r s)) ( s _b(A r s)), A A^A :=¬r∧□b(A→(r∨DA)),Z+:=◇a(A∧¬r∧¬s∧p∧¬A), := r _b(A→(r D^A)), Z^+:= _a(A r s p A^A), θ11E _11^E :=A∨(r∧(Z∨¬Z+)). :=A (r (Z Z^+) ). Proof of θ11E∈E11∩E01 _11^E∈ E_11∩ E_01. We first show θ11E∈E11∩E01 _11^E∈ E_11∩ E_01. Take any model M. We claim that, θ11E _11^E agrees with A at non-r states in M, and that [↑θ11E]Z↔Z+[ _11^E]Z Z^+ is valid: At non-r states, θ11E↔A _11^E A is trivial. We prove [↑θ11E]D↔DA[ _11^E]D D^A, [↑θ11E]A↔A[ _11^E]A A^A, and finally, [↑θ11E]Z↔Z+[ _11^E]Z Z^+ using the reduction axioms for BPAL (Lemma 1): [↑θ11E]D [ _11^E]D ↔[↑A]D [ A]D ↔(s∧[↑A]◇a(¬r∧¬s))∨(¬s∧[↑A]◇b(¬r∧s)) (s [ A] _a( r s)) ( s [ A] _b( r s)) ↔(s∧◇a(A∧[↑A](¬r∧¬s))∨(¬s∧◇b(A∧[↑A](¬r∧s)) (s _a(A [ A]( r s)) ( s _b(A [ A]( r s)) ↔(s∧◇a(A∧¬r∧¬s))∨(¬s∧◇b(A∧¬r∧s)) (s _a(A r s)) ( s _b(A r s)) ↔DA, D^A, [↑θ11E]A [ _11^E]A ↔[↑θ11E](¬r∧□b(r∨D)) [ _11^E]( r _b(r D)) ↔¬r∧□b(θ11E→[↑θ11E](r∨D)) r _b( _11^E→[ _11^E](r D)) ↔¬r∧□b(A→(r∨DA)) r _b(A→(r D^A)) ↔A, A^A, [↑θ11E]Z [ _11^E]Z ↔[↑θ11E]◇a(¬r∧¬s∧p∧¬A) [ _11^E] _a( r s p A) ↔◇a(θ11E∧[↑θ11E](¬r∧¬s∧p∧¬A)) _a( _11^E [ _11^E]( r s p A)) ↔◇a(A∧¬r∧¬s∧p∧¬A) _a(A r s p A^A) ↔Z+. Z^+. This proves the claim. We now check θ11E∈E01 _11^E∈ E_01. If θ11E _11^E is false at an r-state in M, then Z is false and Z+Z^+ is true, so θ11E _11^E is true after one update by [↑θ11E]Z↔Z+[ _11^E]Z Z^+. If θ11E _11^E is false at a non-r state x, then A=¬r∧□b(r∨D)A= r _b(r D) is false at x, so choose a b-successor satisfying ¬r∧¬D r D. The K45 identity Rb(x)=Rb(y)R_b(x)=R_b(y) for xRbyxR_by shows that every non-r b-successor of x also falsifies A. Thus, after an announcement of θ11E _11^E, all arrows from x to such states are removed, and A becomes true. Thus, θ11E _11^E is a true lie and hence θ11E∈E01 _11^E∈ E_01. We next check θ11E∈E11 _11^E∈ E_11. Take any w∈Mw∈ M and suppose M,w⊧θ11EM,w _11^E. If M1,w⊧θ11EM^1,w _11^E, θ11E _11^E already satisfies E11E_11. If M1,w⊧¬θ11EM^1,w _11^E, we have M2,w⊧θ11EM^2,w _11^E since θ11E _11^E is a true lie as we have just seen. Therefore, θ11E∈E11 _11^E∈ E_11. Proof of θ11E∉SE11 _11^E∉ SE_11 and θ11E∉SE01 _11^E∉ SE_01. We next show θ11E∉SE11 _11^E∉ SE_11 and θ11E∉SE01 _11^E∉ SE_01 using the two-peeling model M in Definition 11. We first check M,w⊧θ11EM,w _11^E. Since u0,1u_0,1 has no a-successor and satisfies s∧¬rs r, we have M,u0,1⊧¬DM,u_0,1 D. The unique b-successor of u0,0u_0,0 is u0,1u_0,1, and hence M,u0,0⊧¬AM,u_0,0 A. Moreover, M,u0,0⊧¬r∧¬s∧pM,u_0,0 r s p. Since wRau0,0wR_au_0,0, it follows that M,w⊧ZM,w Z. As M,w⊧rM,w r, we therefore have M,w⊧r∧ZM,w r Z and hence M,w⊧θ11EM,w _11^E. Write Mn:=M|nθ11EM^n:=M|^n _11^E and, for 0≤ℓ≤m0≤ ≤ m, put Pm,ℓ:=um,2ℓ,um,2ℓ+1P_m, :=\u_m,2 ,u_m,2 +1\. We first determine where A is false on each branch. At stage 00, the terminal state um,2m+1u_m,2m+1 satisfies s and has no a-successor. Hence M,um,2m+1⊧¬DM,u_m,2m+1 D. The two states in Pm,mP_m,m have the common b-successor um,2m+1u_m,2m+1. Since r is false at every branch state, it follows that M,x⊧¬AM,x A for every x∈Pm,mx∈ P_m,m. On the other hand, if ℓ<m <m, then um,2ℓ+1u_m,2 +1 has the a-successor um,2ℓ+2u_m,2 +2, which satisfies ¬r∧¬s r s. Hence M,um,2ℓ+1⊧DM,u_m,2 +1 D, and therefore every state in Pm,ℓP_m, satisfies A. Claim. For every n<ωn<ω and every m≥nm≥ n, Mn,x⊧¬A⟺x∈Pm,m−nM^n,x A x∈ P_m,m-n for every state x on branch m (see Figure 2). Proof of claim. The case n=0n=0 was proved above. (⇐)( ) Suppose the claim holds at stage n. Note that Pm,m−n=um,2(m−n),um,2(m−n)+1P_m,m-n=\u_m,2(m-n),u_m,2(m-n)+1\. Since r is false at every branch state, θ11E _11^E agrees there with A. Hence the update from MnM^n to Mn+1M^n+1 deletes every arrow whose target belongs to Pm,m−nP_m,m-n. In particular, if n<mn<m, the a-arrow from um,2(m−n)−1u_m,2(m-n)-1 to um,2(m−n)u_m,2(m-n) is deleted. Thus Mn+1,um,2(m−n)−1⊧¬D.M^n+1,u_m,2(m-n)-1 D. The two states in Pm,m−n−1=um,2(m−n)−2,um,2(m−n)−1P_m,m-n-1=\u_m,2(m-n)-2,u_m,2(m-n)-1\ have the common b-successor um,2(m−n)−1u_m,2(m-n)-1, and therefore both falsify A in Mn+1M^n+1. (⇒)( ) For the converse, the common b-successor um,2(m−n)+1u_m,2(m-n)+1 of the states in Pm,m−nP_m,m-n is itself an A-false target at stage n, so the corresponding b-arrows are deleted. Hence the □b _b-conjunct of A is vacuously true there at stage n+1n+1. All other pairs retain the witnesses that made their corresponding D-formulas true. Thus Pm,m−n−1P_m,m-n-1 is the unique A-false pair on branch m at stage n+1n+1. This proves the claim by induction. ∎ ■ In particular, the head um,0u_m,0 is A-false exactly at stage m. Since all branch heads are a-successors of w initially, and an a-arrow to um,0u_m,0 is deleted precisely in the update following stage m, we obtain RaMn(w)=um,0∣m≥nR_a^M^n(w)=\u_m,0 m≥ n\. Among these heads, un,0u_n,0 is the unique one satisfying ¬A A at stage n. Every branch head satisfies ¬r∧¬s r s, and M,um,0⊧pM,u_m,0 p iff m is even. Therefore Mn,w⊧Z⟺Mn,un,0⊧p⟺n is even.M^n,w Z M^n,u_n,0 p n is even. Moreover, by [↑θ11E]Z↔Z+[ _11^E]Z Z^+, Mn,w⊧Z+⟺Mn+1,w⊧Z⟺n is odd.M^n,w Z^+ M^n+1,w Z n is odd. Since r is true at w and A is false there, we have Mn,w⊧θ11E⟺Mn,w⊧Z∨¬Z+⟺n is even.M^n,w _11^E M^n,w Z Z^+ n is even. Hence the truth-value sequence of θ11E _11^E at w is 1,0,1,0,…1,0,1,0,…. Therefore θ11E∉SE11 _11^E∉ SE_11. Since the pointed model M1,wM^1,w starts with value 00 and has the subsequent sequence 0,1,0,1,…0,1,0,1,…, we also have θ11E∉SE01 _11^E∉ SE_01. ∎ wwrru0,0u_0,0u1,0u_1,0u2,0u_2,0u3,0u_3,0p, t, uuttpp, t⋮ 0,1u_0,1ssu1,1u_1,1u1,2u_1,2u1,3u_1,3ssssu2,1u_2,1u2,2u_2,2u2,3u_2,3u2,4u_2,4u2,5u_2,5ssssssu3,1u_3,1u3,2u_3,2u3,3u_3,3u3,4u_3,4u3,5u_3,5u3,6u_3,6u3,7u_3,7s (a) M wwrru0,0u_0,0u1,0u_1,0u2,0u_2,0u3,0u_3,0p, t, uuttpp, t⋮ 0,1u_0,1ssu1,1u_1,1u1,2u_1,2u1,3u_1,3ssssu2,1u_2,1u2,2u_2,2u2,3u_2,3u2,4u_2,4u2,5u_2,5ssssssu3,1u_3,1u3,2u_3,2u3,3u_3,3u3,4u_3,4u3,5u_3,5u3,6u_3,6u3,7u_3,7s (b) M1=M|θ11E=M|θ11SE=M|θ11<ωM^1=M| _11^E=M| _11^SE=M| _11^<ω wwrru0,0u_0,0u1,0u_1,0u2,0u_2,0u3,0u_3,0p, t, uuttpp, t⋮ 0,1u_0,1ssu1,1u_1,1u1,2u_1,2u1,3u_1,3ssssu2,1u_2,1u2,2u_2,2u2,3u_2,3u2,4u_2,4u2,5u_2,5ssssssu3,1u_3,1u3,2u_3,2u3,3u_3,3u3,4u_3,4u3,5u_3,5u3,6u_3,6u3,7u_3,7s (c) M2=M|2θ11E=M|2θ11SE=M|2θ11<ωM^2=M|^2 _11^E=M|^2 _11^SE=M|^2 _11^<ω Figure 2: The two-peeling model in Definition 11. Blue arrows and red arrows indicate the accessibility relations of a and b, respectively. Transitive arrows are omitted. Definition 12 (One-peeling model). Choose distinct agents a,b∈Ga,b∈ G and consider the following model M=(W,Rii∈G,V).M=(W,\R_i\_i∈ G,V).22 2 The model is almost the same as the two-peeling model in Definition 11 except that j≤mj≤ m now, not j≤2m+1j≤ 2m+1. Let H:=um,0∣m≥1H:=\u_m,0 m≥ 1\ and put W:=w∪um,j∣m≥1, 0≤j≤m.W:=\w\∪\u_m,j m≥ 1,\ 0≤ j≤ m\. Define Ra:=(w∪H)×H∪⋃m≥1⋃0≤j<mj oddum,j,um,j+1×um,j+1,R_a:=(\w\∪ H)× H\;∪\; _m≥ 1 _ subarrayc0≤ j<m\\ j odd subarray\u_m,j,u_m,j+1\×\u_m,j+1\, and Rb:=⋃m≥1⋃0≤j<mj evenum,j,um,j+1×um,j+1.R_b:= _m≥ 1 _ subarrayc0≤ j<m\\ j even subarray\u_m,j,u_m,j+1\×\u_m,j+1\. For every c∈G∖a,bc∈ G \a,b\, let Rc:=∅R_c:= . The valuation is given by V(r):=w,V(s):=um,j∣m≥1, 0≤j≤m,j odd,V(r):=\w\, V(s):=\u_m,j m≥ 1,\ 0≤ j≤ m,\ j odd\, and V(p):=um,0∣m≥1,m even.V(p):=\u_m,0 m≥ 1,\ m even\. All other proposition letters are false everywhere (see Figure 3(a)). Lemma 9. If |G|≥2|G|≥ 2, E00 E00E_00 SE_00 is nonempty. Proof. Put Lχ:=(s∧◇a(¬r∧¬s∧χ))∨(¬s∧◇b(¬r∧s∧χ)),Lχ:=(s _a( r s χ)) ( s _b( r s χ)), let LkL^k denote k-fold iteration of L, and set Dk:=Lk⊤D_k:=L^k , Hk:=Dk∧¬Dk+1H_k:=D_k D_k+1, and Xk:=◇a(¬r∧¬s∧p∧Hk).X_k:= _a( r s p H_k). Let θ00E:=(¬r∧D1)∨(r∧X1∧¬X2). _00^E:=( r D_1) (r X_1 X_2). Proof of θ00E∈E00 _00^E∈ E_00 For k≥1k≥ 1, we first show ⊧[↑θ00E]Dk↔Dk+1 [ _00^E]D_k D_k+1. At every non-r state, θ00E _00^E agrees with D1D_1. Hence, for any formula χ, the reduction axioms for BPAL (Lemma 1) give [↑θ00E]Lχ [ _00^E]Lχ ↔(s∧◇a(θ00E∧[↑θ00E](¬r∧¬s∧χ))) (s _a( _00^E [ _00^E]( r s χ)) ) ∨(¬s∧◇b(θ00E∧[↑θ00E](¬r∧s∧χ))) ( s _b( _00^E [ _00^E]( r s χ)) ) ↔(s∧◇a(D1∧¬r∧¬s∧[↑θ00E]χ)) (s _a(D_1 r s [ _00^E]χ) ) ∨(¬s∧◇b(D1∧¬r∧s∧[↑θ00E]χ)) ( s _b(D_1 r s [ _00^E]χ) ) ↔L(D1∧[↑θ00E]χ). L (D_1 [ _00^E]χ ). Here the second equivalence uses the fact that every target occurring in the definition of L satisfies ¬r r, and therefore θ00E↔D1 _00^E D_1 at such a target. We now prove ⊧[↑θ00E]Dk↔Dk+1 [ _00^E]D_k D_k+1 by induction on k≥1k≥ 1. For k=1k=1, since D1=L⊤D_1=L , the preceding equivalence gives [↑θ00E]D1↔L(D1∧⊤)↔LD1↔D2.[ _00^E]D_1 L(D_1 ) LD_1 D_2. Suppose [↑θ00E]Dk↔Dk+1[ _00^E]D_k D_k+1. Since Dk+1=LDkD_k+1=LD_k, we obtain [↑θ00E]Dk+1 [ _00^E]D_k+1 ↔[↑θ00E]LDk [ _00^E]LD_k ↔L(D1∧[↑θ00E]Dk) L (D_1 [ _00^E]D_k ) ↔L(D1∧Dk+1) L(D_1 D_k+1) ↔LDk+1 LD_k+1 ↔Dk+2. D_k+2. The penultimate equivalence follows from ⊧Dk+1→D1 D_k+1→ D_1: since ⊧Dk→⊤ D_k→ , the definition of L gives ⊧LDk→L⊤ LD_k→ L . Hence ⊧Dk+1→D1 D_k+1→ D_1. Consequently, the same reduction shifts the other indexed formulas by one: for every k≥1k≥ 1, [↑θ00E]Hk↔Hk+1[ _00^E]H_k H_k+1, since Hk=Dk∧¬Dk+1H_k=D_k D_k+1, and [↑θ00E]Xk↔Xk+1[ _00^E]X_k X_k+1 since [↑θ00E]Xk [ _00^E]X_k ↔[↑θ00E]◇a(¬r∧¬s∧p∧Hk) [ _00^E] _a( r s p H_k) ↔◇a(θ00E∧¬r∧¬s∧p∧[↑θ00E]Hk) _a ( _00^E r s p [ _00^E]H_k ) ↔◇a(D1∧¬r∧¬s∧p∧Hk+1) _a (D_1 r s p H_k+1 ) ↔◇a(¬r∧¬s∧p∧Hk+1) _a( r s p H_k+1) ↔Xk+1. X_k+1. The third equivalence uses θ00E↔D1 _00^E D_1 at every ¬r r-state and [↑θ00E]Hk↔Hk+1[ _00^E]H_k H_k+1. The fourth equivalence follows from ⊧Hk+1→D1 H_k+1→ D_1. Take any M,wM,w and suppose that M,w⊧¬θ00EM,w _00^E. Suppose first that M,w⊧¬rM,w r. Since θ00E _00^E agrees with D1D_1 at every non-r state, we have M,w⊧¬D1M,w D_1. Now D1=L⊤D_1=L is a disjunction of diamond formulas, and believed public announcements only delete arrows. Therefore, once D1D_1 is false at a state, it remains false after every further update. Since the valuation of r does not change, it follows that Mn,w⊧¬θ00EM^n,w _00^E for every n≥1n≥ 1. Suppose next that M,w⊧rM,w r. If M1,w⊧¬θ00EM^1,w _00^E, there is nothing to prove. Otherwise, suppose M1,w⊧θ00EM^1,w _00^E. Since r remains true at w, the definition of θ00E _00^E gives M1,w⊧¬X2M^1,w X_2. The equivalence [↑θ00E]X1↔X2[ _00^E]X_1 X_2 is valid in every K45 model, so applying it to M1M^1 yields M2,w⊧X1⟺M1,w⊧X2.M^2,w X_1 M^1,w X_2. Hence M2,w⊧¬X1M^2,w X_1. Since r is still true at w, we obtain M2,w⊧¬θ00EM^2,w _00^E. Thus, whenever θ00E _00^E is initially false, it is false again after either one or two updates. Therefore θ00E∈E00 _00^E∈ E_00. Proof of θ00E∉SE00 _00^E∉ SE_00 We show θ00E∉SE00 _00^E∉ SE_00 using the one-peeling model M in Definition 12. We first determine the truth of DkD_k in the initial model. We claim that for every m≥1m≥ 1, 0≤j≤m0≤ j≤ m, and k≥1k≥ 1, M,um,j⊧Dk⟺k≤m−j.M,u_m,j D_k k≤ m-j. For k=1k=1, this follows directly from the definition of L: the relevant a- or b-successor of um,ju_m,j is um,j+1u_m,j+1 when j<mj<m, while no such successor exists when j=mj=m. Suppose the claim holds for k. Since Dk+1=LDkD_k+1=LD_k, we have M,um,j⊧Dk+1 M,u_m,j D_k+1 ⟺j<m and M,um,j+1⊧Dk j<m and M,u_m,j+1 D_k ⟺k≤m−j−1 k≤ m-j-1 ⟺k+1≤m−j. k+1≤ m-j. Thus the claim follows by induction. In particular, at the head um,0u_m,0, M,um,0⊧Hk⟺M,um,0⊧Dk∧¬Dk+1⟺m=k.M,u_m,0 H_k M,u_m,0 D_k D_k+1 m=k. Since every head is an a-successor of w, every head satisfies ¬r∧¬s r s, and p holds at um,0u_m,0 exactly when m is even, it follows that M,w⊧Xk⟺k is even.M,w X_k k is even. Write Mn:=M|nθ00EM^n:=M|^n _00^E. From the validity [↑θ00E]Xk↔Xk+1[ _00^E]X_k X_k+1, induction on n gives Mn,w⊧Xk⟺M,w⊧Xk+n.M^n,w X_k M,w X_k+n. Hence Mn,w⊧X1⟺n is odd,Mn,w⊧X2⟺n is even.M^n,w X_1 n is odd, M^n,w X_2 n is even. The valuation of r is unchanged by the updates, so Mn,w⊧rM^n,w r for every n<ωn<ω. Therefore, by the definition of θ00E _00^E, Mn,w⊧θ00E M^n,w _00^E ⟺Mn,w⊧X1∧¬X2 M^n,w X_1 X_2 ⟺n is odd. n is odd. Thus the truth-value sequence of θ00E _00^E at w is 0,1,0,1,…0,1,0,1,…. In particular, M,w⊧¬θ00EM,w _00^E, but θ00E _00^E is true at arbitrarily large finite stages. Hence θ00E∉SE00 _00^E∉ SE_00. ∎ wwrru1,0u_1,0u1,1u_1,1ssu2,0u_2,0u2,1u_2,1ssu2,2u_2,2ppu3,0u_3,0u3,1u_3,1ssu3,2u_3,2u3,3u_3,3ssu4,0u_4,0u4,1u_4,1ssu4,2u_4,2u4,3u_4,3ssu4,4u_4,4p⋮ (a) M wwrru1,0u_1,0u1,1u_1,1ssu2,0u_2,0u2,1u_2,1ssu2,2u_2,2ppu3,0u_3,0u3,1u_3,1ssu3,2u_3,2u3,3u_3,3ssu4,0u_4,0u4,1u_4,1ssu4,2u_4,2u4,3u_4,3ssu4,4u_4,4p⋮ (b) M1=M|θ00E=M|θ11SEO=M|θ00SEOM^1=M| _00^E=M| _11^SEO=M| _00^SEO wwrru1,0u_1,0u1,1u_1,1ssu2,0u_2,0u2,1u_2,1ssu2,2u_2,2ppu3,0u_3,0u3,1u_3,1ssu3,2u_3,2u3,3u_3,3ssu4,0u_4,0u4,1u_4,1ssu4,2u_4,2u4,3u_4,3ssu4,4u_4,4p⋮ (c) M2=M|2θ00E=M|2θ11SEO=M|2θ00SEOM^2=M|^2 _00^E=M|^2 _11^SEO=M|^2 _00^SEO Figure 3: The one-peeling model in Definition 12. Blue arrows and red arrows indicate the accessibility relations of a and b, respectively. Lemma 10. If |G|≥2|G|≥ 2, SE11Ord 11SE_11^Ord E_11 and SE00Ord 00SE_00^Ord E_00 are nonempty. Proof. Choose distinct agents a,b∈Ga,b∈ G and put χ:=(s∧◇a¬s)∨(¬s∧◇bs),θ11SEO:=χ∨(□aχ∧□bχ).χ:=(s _a s) ( s _bs), _11^SEO:=χ ( _aχ _bχ). Proof of θ11SEO∈SE11Ord _11^SEO∈ SE_11^Ord. Suppose M,w⊧θ11SEOM,w _11^SEO, where M is any K45 model. Write Mα:=M|αθ11SEOM^α:=M|^α _11^SEO and let RiαR_i^α be the accessibility relation for agent i in MαM^α. By Proposition 3, choose an ordinal λ≥1λ≥ 1 such that Mλ=Mλ+1M^λ=M^λ+1. Every arrow in MλM^λ has a target satisfying θ11SEO _11^SEO; otherwise it would be deleted in the next update. Suppose, towards a contradiction, that Mλ,w⊧¬θ11SEOM^λ,w _11^SEO. Then Mλ,w⊧¬χM^λ,w χ and at least one of □aχ _aχ and □bχ _bχ is false at w. Thus there are i∈a,bi∈\a,b\ and a state v such that wRiλvwR_i^λv and Mλ,v⊧¬χM^λ,v χ. By Euclideanness of RiλR_i^λ, we have vRiλvvR_i^λv, so Mλ,v⊧¬□iχM^λ,v _iχ. Together with Mλ,v⊧¬χM^λ,v χ, this gives Mλ,v⊧¬θ11SEOM^λ,v _11^SEO, contradicting the fact that v is the target of an arrow in MλM^λ. Therefore Mλ,w⊧θ11SEOM^λ,w _11^SEO. Since the model is unchanged at every later stage, Mβ,w⊧θ11SEOM^β,w _11^SEO for every β≥λβ≥λ. This proves θ11SEO∈SE11Ord _11^SEO∈ SE_11^Ord. Proof of θ11SEO∉E11 _11^SEO∉ E_11. Let m,jm,j range over natural numbers and let all the following states be distinct. We use the one-peeling model in Definition 12. See Figure 3. The updated models will also be the same. Initially, every head um,0u_m,0 satisfies χ, since it satisfies ¬s s and has the b-successor um,1u_m,1 satisfying s. Moreover, Ra(w)=HR_a(w)=H and Rb(w)=∅R_b(w)= . Hence M,w⊧□aχ∧□bχM,w _aχ _bχ, and therefore M,w⊧θ11SEOM,w _11^SEO. Write Mn:=M|nθ11SEOM^n:=M|^n _11^SEO and let RinR_i^n be its relations. We first explain which arrows are deleted at each update. If xRinyxR_i^ny for i∈a,bi∈\a,b\, Euclideanness gives yRinyyR_i^ny. If χ is false at y, then □iχ _iχ is false there as well, and hence θ11SEO _11^SEO is false there. Conversely, χ implies θ11SEO _11^SEO by definition. Thus, at every target of an a- or b-arrow in MnM^n, χ and θ11SEO _11^SEO have the same truth value. An existing arrow therefore survives the next update exactly when its target satisfies χ in MnM^n. We claim that, for every n≥0n≥ 0, m≥1m≥ 1, 0≤j≤m0≤ j≤ m, x∈Wx∈ W, and i∈a,bi∈\a,b\, xRinum,j⟺xRium,jandn≤m−j.xR_i^nu_m,j xR_iu_m,j\ and\ n≤ m-j. The case n=0n=0 follows from the definition of M0M^0. Suppose the claim holds at stage n. At um,ju_m,j, the definition of χ selects the b-relation when j is even and the a-relation when j is odd. Initially, this relation has the single successor um,j+1u_m,j+1 if j<mj<m, and has no successor if j=mj=m. For j<mj<m, the states um,ju_m,j and um,j+1u_m,j+1 have opposite truth values of s, and the relevant arrow remains at stage n exactly when n≤m−j−1n≤ m-j-1. Thus Mn,um,j⊧χ⟺n<m−j.M^n,u_m,j χ n<m-j. Using the condition for an existing arrow to survive, we obtain xRin+1um,j xR_i^n+1u_m,j ⟺xRinum,jandMn,um,j⊧χ xR_i^nu_m,j\ and\ M^n,u_m,j χ ⟺xRium,jandn<m−j xR_iu_m,j\ and\ n<m-j ⟺xRium,jandn+1≤m−j. xR_iu_m,j\ and\ n+1≤ m-j. This proves the claim by induction and establishes the displayed condition for χ at every finite stage. In particular, Ran(w)=um,0∣m≥1,n≤mR_a^n(w)=\u_m,0 m≥ 1,\ n≤ m\ and Rbn(w)=∅R_b^n(w)= . Since s is false at w, we have Mn,w⊧¬χM^n,w χ at every finite stage. For each n≥1n≥ 1, the head un,0u_n,0 is still an a-successor of w, but Mn,un,0⊧¬χM^n,u_n,0 χ because n<n<n is false. Hence Mn,w⊧¬□aχM^n,w _aχ, and therefore Mn,w⊧¬θ11SEOM^n,w _11^SEO for every n≥1n≥ 1. Since θ11SEO _11^SEO is true at M,wM,w but false at every positive finite stage, θ11SEO∉E11 _11^SEO∉ E_11. Finally, every arrow targets some um,ju_m,j and is deleted by stage m−j+1m-j+1. Thus all relations are empty at stage ω. Both □aχ _aχ and □bχ _bχ are then true at w, and further updates leave the model unchanged. The truth values at w are 1,0,0,…,1ω,1ω+1,…1,0,0,…,1_ω,1_ω+1,…. Put D:=(s∧◇a(¬r∧¬s))∨(¬s∧◇b(¬r∧s)),A:=¬r∧D,D:=(s _a( r s)) ( s _b( r s)), A:= r D, and let Y:=□a(r∨A),θ00SEO:=A∨(r∧¬Y).Y:= _a(r A), _00^SEO:=A (r Y). Proof of θ00SEO∈SE00Ord _00^SEO∈ SE_00^Ord. Suppose M,w⊧¬θ00SEOM,w _00^SEO, where M is any K45 model, and write Mα:=M|αθ00SEOM^α:=M|^α _00^SEO. Suppose first that M,w⊧¬rM,w r. At every non-r state, θ00SEO _00^SEO agrees with A, and A agrees with D. Hence M,w⊧¬DM,w D. Since believed public announcements only delete arrows and do not change valuations, neither of the diamond disjuncts of D can become true at a later stage once it is false. Therefore Mα,w⊧¬DM^α,w D, and hence Mα,w⊧¬θ00SEOM^α,w _00^SEO, for every ordinal α. Suppose next that M,w⊧rM,w r. By Proposition 3, choose an ordinal λ such that Mλ=Mλ+1M^λ=M^λ+1. Replacing λ by λ+1λ+1 if necessary, we may assume λ>0λ>0. We claim that Mλ,w⊧¬θ00SEOM^λ,w _00^SEO. Since MλM^λ is fixed, every arrow remaining in MλM^λ has a θ00SEO _00^SEO-true target. Thus, if wRaλvwR_a^λv, then Mλ,v⊧θ00SEOM^λ,v _00^SEO. If Mλ,v⊧rM^λ,v r, then Mλ,v⊧r∨AM^λ,v r A immediately. If instead Mλ,v⊧¬rM^λ,v r, then θ00SEO _00^SEO agrees with A at v, so Mλ,v⊧AM^λ,v A, and again Mλ,v⊧r∨AM^λ,v r A. Consequently every a-successor of w satisfies r∨Ar A, and hence Mλ,w⊧Y.M^λ,w Y. Since r is true at w, A=¬r∧DA= r D is false there. Therefore Mλ,w⊧¬θ00SEOM^λ,w _00^SEO. As MλM^λ is fixed, this remains true at every later stage. Thus θ00SEO∈SE00Ord _00^SEO∈ SE_00^Ord. Proof of θ00SEO∉E00 _00^SEO∉ E_00. For the counterexample, we again use the one-peeling model M,wM,w in Definition 12. See again Figure 3. The updated models will also be the same. No arrow in this model has w as its target. Hence every arrow target satisfies ¬r r. At such a state, θ00SEO↔A↔D. _00^SEO A D. In the countermodel for Lemma 9, the formula θ00E _00^E also agrees with D at every arrow target. Therefore iteration by θ00SEO _00^SEO deletes exactly the same arrows at every stage as iteration by θ00E _00^E. Initially, every branch head um,0u_m,0 satisfies D, since m≥1m≥ 1. Hence every a-successor of w satisfies A, so M,w⊧YM,w Y. Since M,w⊧rM,w r, we have M,w⊧¬θ00SEO.M,w _00^SEO. Now let n≥1n≥ 1 be finite. As in the countermodel of Lemma 9, the head un,0u_n,0 is still an a-successor of w at stage n, but Mn,un,0⊧¬D.M^n,u_n,0 D. Since r is false at un,0u_n,0, we also have Mn,un,0⊧¬AM^n,u_n,0 A. Thus Mn,w⊧¬YM^n,w Y, and, since r remains true at w, Mn,w⊧θ00SEOfor every finite n≥1.M^n,w _00^SEO every finite n≥ 1. At stage ω, all arrows have been deleted. Hence Mω,w⊧YM^ω,w Y vacuously, so Mω,w⊧¬θ00SEOM^ω,w _00^SEO. The model is fixed from that stage onward. Thus the truth-value sequence of θ00SEO _00^SEO at w is 0,1,1,…,0ω,0ω+1,…0,1,1,…,0_ω,0_ω+1,…. In particular, θ00SEO _00^SEO is initially false but is true at every positive finite stage. Therefore θ00SEO∉E00 _00^SEO∉ E_00. ∎ Lemma 11. If |G|≥2|G|≥ 2, SE11 E11OrdSE_11 SE_11^Ord and S11<ω 11OrdS_11^<ω E_11^Ord are nonempty. Proof. Choose distinct agents a,b∈Ga,b∈ G. Define C C :=¬r∧¬t,P:=¬r∧t, := r t, P:= r t, D D :=(s∧◇a(C∧¬s))∨(¬s∧◇b(C∧s)), :=(s _a(C s)) ( s _b(C s)), A A :=¬r∧□b(r∨t∨D),Q:=□a(P→¬A),B:=A∨Q, := r _b(r t D), Q:= _a(P→ A), B:=A Q, Y Y :=◇aP,Z:=◇a(P∧u),H:=□a(P→B), := _aP, Z:= _a(P u), H:= _a(P→ B), θ11SE _11^SE :=(C∧A)∨(P∧B)∨(r∧Y), :=(C A) (P B) (r Y), θ11<ω _11^<ω :=(C∧A)∨(P∧B)∨(r∧(Z∨(Y∧H))). :=(C A) (P B) (r (Z (Y H)) ). We first show the following two facts that will be used for both θ11SE _11^SE and θ11<ω _11^<ω (MnM^n here denotes the updated model either by θ11SE _11^SE or θ11<ω _11^<ω): 1. For all n, if Mn,x⊧¬r∧¬AM^n,x r A, then Mn+1,x⊧AM^n+1,x A. 2. For all n, if Mn,x⊧YM^n,x Y, then Mn+1,x⊧YM^n+1,x Y. For the first statement, suppose that Mn,x⊧¬r∧¬AM^n,x r A. Then there is a b-successor y of x such that y⊧C∧¬Dy C D. If z is any C-valued b-successor of x, then transitivity and Euclideanness give Rb(x)=Rb(z)R_b(x)=R_b(z). Since x and z both satisfy ¬r r, it follows that A is false at z. At a C-state, both θ11SE _11^SE and θ11<ω _11^<ω agree with A. Hence every C-valued b-successor of x is a false announcement target and is deleted by the next update. After that update, every remaining b-successor of x satisfies r∨tr t, so Mn+1,x⊧AM^n+1,x A. Since later updates only delete arrows, A remains true at x at all later finite stages. For the second statement, suppose that Mn,x⊧YM^n,x Y. Thus x has a P-valued a-successor. We show that at least one such successor survives the next update. If some P-valued a-successor y satisfies A, then y⊧By B, and hence both displayed announcement formulas are true at y. Thus the arrow to y survives. Otherwise every P-valued a-successor of x satisfies ¬A A. Choose one such successor y. Since xRayxR_ay, K45 gives Ra(x)=Ra(y)R_a(x)=R_a(y). Hence every P-valued a-successor of y also satisfies ¬A A, so y⊧Qy Q. Therefore y⊧By B, and again both announcement formulas are true at y. Thus the arrow to y survives. Consequently, Mn+1,x⊧YM^n+1,x Y. Proof of θ11SE∈SE11 _11^SE∈ SE_11. We first show θ11SE∈SE11 _11^SE∈ SE_11. Take any pointed K45 model M,wM,w such that M,w⊧θ11SEM,w _11^SE, and write Mn:=M|nθ11SEM^n:=M|^n _11^SE. Suppose first that M,w⊧¬rM,w r. Since the valuation does not change, w satisfies either C or P at every stage. Whenever A is true at w, θ11SE _11^SE is also true there: if w satisfies C, this follows from the disjunct C∧AC A, and if w satisfies P, then A implies B and hence P∧BP B. If A never becomes false at any finite stage, then θ11SE _11^SE remains true at every finite stage. Otherwise, let n be a finite stage at which A is false. By the first fact above, A is true from stage n+1n+1 onward, and therefore θ11SE _11^SE is also true from stage n+1n+1 onward. Suppose next that M,w⊧rM,w r. Since M,w⊧θ11SEM,w _11^SE, its third disjunct gives M,w⊧YM,w Y. By the second fact above, Y remains true at every finite stage. Since r also remains true, Mn,w⊧θ11SEM^n,w _11^SE for every n<ωn<ω. Thus θ11SE∈SE11 _11^SE∈ SE_11. Proof of θ11SE∉SE11Ord _11^SE∉ SE_11^Ord We use the two-peeling model in Definition 11. See Figure 2. For 0≤ℓ≤m0≤ ≤ m, put Pm,ℓ:=um,2ℓ,um,2ℓ+1P_m, :=\u_m,2 ,u_m,2 +1\. Write Mn:=M|nθ11SEM^n:=M|^n _11^SE. We claim that, at every finite stage n, (i)for every m≥n,Pm,m−n is the unique A-false pair on branch m,(i)Ran(w)=um,0∣m≥n,(i)un,0 is the unique B-false state among these heads. array[]l(i)&for every m≥ n,\ P_m,m-n is the unique $A$-false pair on branch m,\\[5.69054pt] (i)&R_a^n(w)=\u_m,0 m≥ n\,\\[5.69054pt] (i)&u_n,0 is the unique $B$-false state among these heads. array At stage 00, the terminal state um,2m+1u_m,2m+1 satisfies C∧sC s and has no a-successor satisfying C∧¬sC s. Hence it falsifies D. Since the two states in Pm,mP_m,m have um,2m+1u_m,2m+1 as their common b-successor, both falsify A. Every earlier pair is A-true, because its common odd b-successor has the next even state as an a-successor satisfying C∧¬sC s. Thus (i) holds for n=0n=0. All heads are initially a-successors of w, so (i) also holds. The head u0,0u_0,0 is A-false, whereas every head um,0u_m,0 with m>0m>0 is A-true. Moreover, u1,0u_1,0 is a P-valued a-successor of u0,0u_0,0 satisfying A, so u0,0⊧¬Qu_0,0 Q. Hence u0,0⊧¬Bu_0,0 B, while every later head satisfies B because it satisfies A. This proves (i) at stage 00. Now suppose (i)–(i) hold at stage n. For every m>nm>n, deleting the arrows whose targets lie in the A-false pair Pm,m−nP_m,m-n removes the a-arrow into its even member. Consequently, the odd state immediately to its left loses the witness that made D true, and the preceding pair Pm,m−n−1P_m,m-n-1 becomes A-false. At the same time, the old A-false pair loses its common b-target and becomes A-true. All other pairs remain A-true. Hence (i) holds at stage n+1n+1. By (i), un,0u_n,0 is the only false announcement target among the currently accessible heads, so exactly this head is deleted from the common a-successor set. Thus Ran+1(w)=um,0∣m≥n+1R_a^n+1(w)=\u_m,0 m≥ n+1\, proving (i). By (i), un+1,0u_n+1,0 is now the unique A-false surviving head. The later head un+2,0u_n+2,0 is still accessible and satisfies A, so un+1,0⊧¬Qu_n+1,0 Q and therefore un+1,0⊧¬Bu_n+1,0 B. Every later head satisfies A, hence B. This proves (i) and completes the induction. Since every surviving head satisfies P, (i) gives Mn,w⊧YM^n,w Y for every n<ωn<ω. Since r is true at w, Mn,w⊧θ11SEfor every n<ω.M^n,w _11^SE every n<ω. On the other hand, every head um,0u_m,0 is deleted as an a-target after finitely many updates. Hence Raω(w)=∅R_a^ω(w)= , so Mω,w⊧¬YM^ω,w Y and therefore Mω,w⊧¬θ11SEM^ω,w _11^SE. All remaining arrows are also deleted by stage ω, so the model is fixed from that stage onward. Thus the truth-value sequence at w is 1,1,1,…,0ω,0ω+1,…1,1,1,…,0_ω,0_ω+1,…. Therefore θ11SE∉SE11Ord _11^SE∉ SE_11^Ord. Proof of θ11<ω∈S11<ω _11^<ω∈ S_11^<ω. We first prove θ11<ω∈S11<ω _11^<ω∈ S_11^<ω. Fix k<ωk<ω, take any pointed K45 model M,wM,w such that M,w⊧θ11<ωM,w _11^<ω, and write Mn:=M|nθ11<ωM^n:=M|^n _11^<ω. Suppose that Mk,w⊧¬θ11<ωM^k,w _11^<ω. We show that Mk,w⊧¬CGθ11<ωM^k,w C_G _11^<ω. Suppose first that Mk,w⊧¬rM^k,w r. Whether w satisfies C or P, the falsity of θ11<ω _11^<ω implies Mk,w⊧¬AM^k,w A. Hence there is a b-successor v satisfying C∧¬DC D. As observed above, K45 gives Rb(w)=Rb(v)R_b(w)=R_b(v), so A is also false at v. Since v satisfies C, Mk,v⊧¬θ11<ωM^k,v _11^<ω. Thus a directly accessible state already falsifies the announcement formula, and hence Mk,w⊧¬CGθ11<ωM^k,w C_G _11^<ω. Suppose next that Mk,w⊧rM^k,w r. Since M,w⊧θ11<ωM,w _11^<ω and r is true at w initially, we have M,w⊧Z∨(Y∧H)M,w Z (Y H). Since Z→YZ→ Y, this implies M,w⊧YM,w Y. By the persistence of Y proved above, Mk,w⊧YM^k,w Y. The assumption Mk,w⊧¬θ11<ωM^k,w _11^<ω therefore gives Mk,w⊧¬Z∧¬HM^k,w Z H. From ¬H H there is an a-successor v satisfying P∧¬BP B. At a P-state, θ11<ω _11^<ω agrees with B, so Mk,v⊧¬θ11<ωM^k,v _11^<ω. Again Mk,w⊧¬CGθ11<ωM^k,w C_G _11^<ω. Thus, for every k<ωk<ω, whenever θ11<ω _11^<ω is initially true and false at stage k, CGθ11<ωC_G _11^<ω is also false there. Hence θ11<ω∈S11<ω _11^<ω∈ S_11^<ω. Proof of θ11<ω∉E11Ord _11^<ω∉ E_11^Ord Finally, use the same two-peeling model M,wM,w in Definition 11 and Figure 2. At every arrow target, r is false, and therefore θ11SE _11^SE and θ11<ω _11^<ω both agree with (C∧A)∨(P∧B)(C A) (P B). Hence the two formulas induce exactly the same sequence of accessibility relations on this model. Initially, u0,0u_0,0 is an a-successor of w satisfying P∧uP u, so M,w⊧ZM,w Z and therefore M,w⊧θ11<ωM,w _11^<ω. At every positive finite stage n, the surviving heads are exactly um,0u_m,0 with m≥nm≥ n. Hence Y is true, while Z is false because u0,0u_0,0 is no longer accessible. Moreover, the accessible head un,0u_n,0 is B-false, so H is false. Therefore Mn,w⊧¬θ11<ωfor every 1≤n<ω.M^n,w _11^<ω every 1≤ n<ω. At stage ω, Y and Z are both false, so θ11<ω _11^<ω is still false; the model is fixed thereafter. Thus its truth-value sequence at w is 1,0,0,…,0ω,0ω+1,…1,0,0,…,0_ω,0_ω+1,…. There is no positive ordinal stage at which the initial truth value returns. Hence θ11<ω∉E11Ord _11^<ω∉ E_11^Ord. ∎ Lemma 12. If |G|≥2|G|≥ 2, SE00 E00OrdSE_00 SE_00^Ord and S00<ω 00OrdS_00^<ω E_00^Ord are nonempty. Proof. Choose distinct agents a,b∈Ga,b∈ G. Put W W :=¬r∧¬t,T:=¬r∧t, := r t, T:= r t, D D :=(s∧◇a(W∧¬s))∨(¬s∧◇b(W∧s)), :=(s _a(W s)) ( s _b(W s)), F F :=◇a(W∧D),B:=◇a(W∧¬D), := _a(W D), B:= _a(W D), N N :=□a¬W,U:=◇aT,K:=F∨(N∧U), := _a W, U:= _aT, K:=F (N U), θ00SE _00^SE :=(W∧D)∨(T∧K)∨(r∧N∧U), :=(W D) (T K) (r N U), θ00<ω _00^<ω :=(W∧D)∨(T∧K)∨(r∧(B∨(N∧U))). :=(W D) (T K) (r (B (N U)) ). At every state satisfying ¬r r, the two formulas agree: if x⊧Wx W, they both agree with D at x, while if x⊧Tx T, they both agree with K at x. We first establish the following three facts. Fix either φ=θ00SE = _00^SE or φ=θ00<ω = _00^<ω, and write Mn:=M|nφM^n:=M|^n . 1. If Mn,x⊧W∧¬DM^n,x W D, then Mm,x⊧W∧¬DM^m,x W D for every m≥nm≥ n. 2. If Mn,x⊧T∧¬KM^n,x T K, then Mm,x⊧T∧¬KM^m,x T K for every m≥nm≥ n. 3. If Mn+1,x⊧N∧UM^n+1,x N U, then Mn,x⊧N∧UM^n,x N U. First, suppose Mn,x⊧W∧¬DM^n,x W D. Since believed public announcements only delete arrows and do not change valuations, the diamond formula D cannot become true at any later stage. Hence Mm,x⊧W∧¬DM^m,x W D for every m≥nm≥ n. Second, suppose Mn,x⊧T∧¬KM^n,x T K. Then Mn,x⊧¬FM^n,x F. The falsity of F persists under further updates. If Mn,x⊧¬UM^n,x U, then U also remains false, so K remains false. Suppose instead that Mn,x⊧UM^n,x U. Since K is false, Mn,x⊧¬NM^n,x N. Let y be any T-valued a-successor of x. Since xRanyxR_a^ny and RanR_a^n is transitive and Euclidean, Ran(x)=Ran(y)R_a^n(x)=R_a^n(y). Therefore F, N, and U have the same truth values at x and y, and hence Mn,y⊧¬KM^n,y K. Since Mn,y⊧TM^n,y T, we have Mn,y⊧¬φM^n,y . Thus every a-arrow from x to a T-valued state is deleted at the next update. Consequently U is false from stage n+1n+1 onward, and since F remains false, so does K. Third, N∧UN U cannot become true for the first time at a finite successor stage. Suppose Mn+1,x⊧N∧UM^n+1,x N U. Choose y such that xRan+1yxR_a^n+1y and Mn+1,y⊧TM^n+1,y T. Since the arrow to y survives the update, Mn,y⊧φM^n,y , and therefore Mn,y⊧KM^n,y K. Suppose toward a contradiction that Mn,x⊧¬NM^n,x N. Since xRanyxR_a^ny, we again have Ran(x)=Ran(y)R_a^n(x)=R_a^n(y), so Mn,y⊧¬NM^n,y N. As Mn,y⊧KM^n,y K, it follows that Mn,y⊧FM^n,y F. Hence there is z such that yRanzyR_a^nz and Mn,z⊧W∧DM^n,z W D. The equality Ran(x)=Ran(y)R_a^n(x)=R_a^n(y) gives xRanzxR_a^nz. Since φ is true at every W∧DW D state, the arrow from x to z survives to stage n+1n+1, contradicting Mn+1,x⊧NM^n+1,x N. Thus Mn,x⊧NM^n,x N. Moreover, the surviving T-valued successor y already gives Mn,x⊧UM^n,x U. Hence Mn+1,x⊧N∧UM^n+1,x N U implies Mn,x⊧N∧UM^n,x N U. Proof of θ00SE∈SE00 _00^SE∈ SE_00. We first show θ00SE∈SE00 _00^SE∈ SE_00. Take any pointed K45 model M,xM,x and suppose M,x⊧¬θ00SEM,x _00^SE. If M,x⊧WM,x W, then M,x⊧¬DM,x D, so the first fact implies Mn,x⊧¬θ00SEM^n,x _00^SE for every n<ωn<ω. If M,x⊧TM,x T, then M,x⊧¬KM,x K, so the second fact gives the same conclusion. Finally, suppose M,x⊧rM,x r. Then M,x⊧¬(N∧U)M,x (N U). If N∧UN U became true at some positive finite stage, repeated use of the third fact would imply that it was already true at stage 00, a contradiction. Hence Mn,x⊧¬θ00SEM^n,x _00^SE for every n<ωn<ω. Therefore θ00SE∈SE00 _00^SE∈ SE_00. Proof of θ00<ω∈S00<ω _00^<ω∈ S_00^<ω. Fix k<ωk<ω, take any pointed K45 model M,xM,x, and suppose M,x⊧¬θ00<ωM,x _00^<ω. We show that Mk,x⊧CGθ00<ωM^k,x C_G _00^<ω implies Mk,x⊧¬θ00<ωM^k,x _00^<ω. If Mk,x⊧¬θ00<ωM^k,x _00^<ω, there is nothing to prove. Suppose instead that Mk,x⊧θ00<ωM^k,x _00^<ω. By the first two facts, an initially false state satisfying W or T cannot become true at a finite stage. Hence M,x⊧rM,x r. At an r-state, θ00<ω _00^<ω agrees with B∨(N∧U)B (N U). Since the formula is initially false, M,x⊧¬(N∧U)M,x (N U). By the third fact, N∧UN U is still false at stage k. Therefore Mk,x⊧BM^k,x B. Choose y such that xRakyxR_a^ky and Mk,y⊧W∧¬DM^k,y W D. At y, θ00<ω _00^<ω agrees with D, so Mk,y⊧¬θ00<ωM^k,y _00^<ω. Hence Mk,x⊧¬CGθ00<ωM^k,x C_G _00^<ω. Thus S00(k,θ00<ω)S_00(k, _00^<ω) holds for every k<ωk<ω, and therefore θ00<ω∈S00<ω _00^<ω∈ S_00^<ω. Proof of θ00SE∉SE00Ord _00^SE∉ SE_00^Ord and θ00<ω∉E00Ord _00^<ω∉ E_00^Ord. We now give one model witnessing both remaining non-membership claims. Let H:=um,0∣m≥1,Ω:=w,z∪um,j∣m≥1, 0≤j≤m.H:=\u_m,0 m≥ 1\, :=\w,z\∪\u_m,j m≥ 1,\ 0≤ j≤ m\. Define M=(Ω,Rii∈G,V)M=( ,\R_i\_i∈ G,V) by Ra R_a :=(w,z∪H)×(z∪H) :=(\w,z\∪ H)×(\z\∪ H) ∪⋃m≥1⋃0≤j<mj oddum,j,um,j+1×um,j+1, ∪ _m≥ 1 _ subarrayc0≤ j<m\\ j odd subarray\u_m,j,u_m,j+1\×\u_m,j+1\, Rb R_b :=⋃m≥1⋃0≤j<mj evenum,j,um,j+1×um,j+1. := _m≥ 1 _ subarrayc0≤ j<m\\ j even subarray\u_m,j,u_m,j+1\×\u_m,j+1\. For every c∈G∖a,bc∈ G \a,b\, put Rc:=∅R_c:= . Let V(r):=w,V(t):=z,V(s):=um,j∣m≥1, 0≤j≤m,j odd.V(r):=\w\, V(t):=\z\, V(s):=\u_m,j m≥ 1,\ 0≤ j≤ m,\ j odd\. All other proposition letters are false everywhere. Thus M,w⊧rM,w r, M,z⊧TM,z T, and every branch state satisfies W. The relations are transitive and Euclidean, so M is a K45 model (see Figure 4). No arrow has w as its target. Since w is the only r-state, θ00SE _00^SE and θ00<ω _00^<ω agree at every arrow target. Hence they induce the same sequence of accessibility relations on this model; write this common sequence as MnM^n. On every branch state the two formulas agree with D, and the state z cannot serve as a W-valued witness for either diamond in D. Now, we have Mn,um,j⊧DM^n,u_m,j D iff n<m−jn<m-j, and at stage n the surviving branch heads are precisely the um,0u_m,0 with m≥nm≥ n. The state z remains an a-target at every finite stage. Indeed, at stage n the head un+1,0u_n+1,0 is still accessible from z and satisfies W∧DW D. Hence Mn,z⊧FM^n,z F, so Mn,z⊧KM^n,z K, and therefore both announcement formulas are true at z. It follows that, at every finite stage n, the a-successors of w are z together with the surviving branch heads. Hence Mn,w⊧¬NM^n,w N, because a W-valued branch head is still accessible, while Mn,w⊧UM^n,w U because z is still accessible. Therefore Mn,w⊧¬θ00SEM^n,w _00^SE for every n<ωn<ω. At stage ω all branch heads have disappeared, while z remains. Thus the only a-successor of w is z, and Mω,w⊧N∧UM^ω,w N U. Hence Mω,w⊧θ00SEM^ω,w _00^SE. The same is true at z: its only remaining a-successor is itself, so Mω,z⊧N∧UM^ω,z N U, and therefore Mω,z⊧KM^ω,z K. Hence all remaining arrows target a state at which both announcement formulas are true, and the model is fixed from stage ω onward. The truth-value sequence of θ00SE _00^SE at w is 0,0,0,…,1ω,1ω+1,…0,0,0,…,1_ω,1_ω+1,…. Thus θ00SE∉SE00Ord _00^SE∉ SE_00^Ord. Finally consider θ00<ω _00^<ω at the same root. At stage 00, every branch head satisfies D, so M,w⊧¬BM,w B. Since also M,w⊧¬NM,w N, we have M,w⊧¬θ00<ωM,w _00^<ω. For every finite n≥1n≥ 1, the head un,0u_n,0 is still an a-successor of w and satisfies ¬D D. Thus Mn,w⊧BM^n,w B, and hence Mn,w⊧θ00<ωM^n,w _00^<ω. At stage ω, Mω,w⊧N∧UM^ω,w N U, so the formula remains true, and the model is fixed thereafter. Its truth-value sequence at w is 0,1,1,…,1ω,1ω+1,…0,1,1,…,1_ω,1_ω+1,…. Thus the initial value 00 never occurs again at any positive ordinal stage. Therefore θ00<ω∉E00Ord _00^<ω∉ E_00^Ord. ∎ wwrrzzttu1,0u_1,0u1,1u_1,1ssu2,0u_2,0u2,1u_2,1ssu2,2u_2,2u3,0u_3,0u3,1u_3,1ssu3,2u_3,2u3,3u_3,3ssu4,0u_4,0u4,1u_4,1ssu4,2u_4,2u4,3u_4,3ssu4,4u_4,4⋮ (a) M wwrrzzttu1,0u_1,0u1,1u_1,1ssu2,0u_2,0u2,1u_2,1ssu2,2u_2,2u3,0u_3,0u3,1u_3,1ssu3,2u_3,2u3,3u_3,3ssu4,0u_4,0u4,1u_4,1ssu4,2u_4,2u4,3u_4,3ssu4,4u_4,4⋮ (b) M1=M|θ00SE=M|θ00<ωM^1=M| _00^SE=M| _00^<ω wwrrzzttu1,0u_1,0u1,1u_1,1ssu2,0u_2,0u2,1u_2,1ssu2,2u_2,2u3,0u_3,0u3,1u_3,1ssu3,2u_3,2u3,3u_3,3ssu4,0u_4,0u4,1u_4,1ssu4,2u_4,2u4,3u_4,3ssu4,4u_4,4⋮ (c) M2=M|2θ00SE=M|2θ00<ωM^2=M|^2 _00^SE=M|^2 _00^<ω Figure 4: A finite prefix of the common countermodel for the two separations in Lemma 12. Blue arrows represent RaR_a and red arrows represent RbR_b. At each finite stage, the accessibility relations induced by θ00SE _00^SE and θ00<ω _00^<ω coincide. The blue chain through z and the surviving branch heads schematically indicates common RaR_a-accessibility among those states; nonadjacent arrows and self-loops at z and the branch heads are omitted. 5 Main results Theorem 13. Let φ∈ℒ . In multi-agent K45, we have the following. In single-agent K45, all the conditions in each item are equivalent. Every displayed right arrow is strict when |G|≥2|G|≥ 2. (1) φ is strongly eventually successful is strongly eventually successful ⟺ ∀M,w[σ0M,w=1⇒limn→∞σnM,w=1] ∀ M,w\,[ _0^M,w=1 _n→∞ _n^M,w=1] ⟹ φ is eventually successful is eventually successful ⟺ ∀M,w[σ0M,w=1⇒lim supn→∞σnM,w=1] ∀ M,w\,[ _0^M,w=1 _n→∞ _n^M,w=1] ⟺ ∃N≥1,⊧φ→⋁n=1N[↑φ]nφ ∃ N≥ 1, → _n=1^N[ ]^n ⟹ ∀k≥0,⊧φ→[↑φ]k(φ↔(φ∨CGφ)). ∀ k≥ 0, →[ ]^k( ( C_G )). (2) φ is strongly eventually self-refuting is strongly eventually self-refuting ⟺ ∀M,wlimn→∞σnM,w=0 ∀ M,w\, _n→∞ _n^M,w=0 ⟺ φ is eventually self-refuting is eventually self-refuting ⟺ ∀M,wlim infn→∞σnM,w=0 ∀ M,w\, _n→∞ _n^M,w=0 ⟺ ∃N≥1,⊧[↑φ]N(¬φ∧⋀i∈G□i⊥) ∃ N≥ 1, [ ]^N ( _i∈ G _i ) ⟹ φ is always informative when true is always informative when true ⟺ ∀k≥0,⊧φ→[↑φ]k(φ↔(φ∧¬CGφ)) ∀ k≥ 0, →[ ]^k( ( C_G )) ⟺ ⊧CGφ→¬φ C_G → ⟺ ⊧φ↔(φ∧¬CGφ). ( C_G ). (3) φ is a strong eventual true lie is a strong eventual true lie ⟺ ∀M,wlimn→∞σnM,w=1 ∀ M,w\, _n→∞ _n^M,w=1 ⟹ φ is an eventual true lie is an eventual true lie ⟺ ∀M,wlim supn→∞σnM,w=1 ∀ M,w\, _n→∞ _n^M,w=1 ⟺ ∃N≥1⊧⋁n=1N[↑φ]nφ ∃ N≥ 1\, _n=1^N[ ]^n ⟹ φ is always informative when false is always informative when false ⟺ ∀k≥0,⊧¬φ→[↑φ]k(φ↔(φ∨CGφ)) ∀ k≥ 0, →[ ]^k( ( C_G )) ⟺ ⊧CGφ→φ C_G → ⟺ ⊧φ↔(φ∨CGφ). ( C_G ). (4) φ is a strong eventual impossible lie is a strong eventual impossible lie ⟺ ∀M,w[σ0M,w=0⇒limn→∞σnM,w=0] ∀ M,w\,[ _0^M,w=0 _n→∞ _n^M,w=0] ⟹ φ is an eventual impossible lie is an eventual impossible lie ⟺ ∀M,w[σ0M,w=0⇒lim infn→∞σnM,w=0] ∀ M,w\,[ _0^M,w=0 _n→∞ _n^M,w=0] ⟺ ∃N≥1,⊧¬φ→⋁n=1N[↑φ]n¬φ ∃ N≥ 1, → _n=1^N[ ]^n ⟹ ∀k≥0,⊧¬φ→[↑φ]k(φ↔(φ∧¬CGφ)). ∀ k≥ 0, →[ ]^k( ( C_G )). Proof. The equivalences with the limit conditions for strongly eventual success and strong eventual impossible lies follow immediately from the definitions, since a sequence with values in 0,1\0,1\ converges to 11 or 00 iff it is eventually constantly 11 or 00, respectively. For strong eventual true lies, suppose first that φ is a strong eventual true lie. Take any pointed model M,wM,w. If σ0M,w=0 _0^M,w=0, then limn→∞σnM,w=1 _n→∞ _n^M,w=1 by definition. Suppose σ0M,w=1 _0^M,w=1. If σnM,w=1 _n^M,w=1 for every n, there is nothing to prove. Otherwise, choose m≥1m≥ 1 such that σmM,w=0 _m^M,w=0. Applying strong eventual truth to the pointed tail model Mm,wM^m,w gives limn→∞σnM,w=1 _n→∞ _n^M,w=1. Conversely, if every truth-value sequence converges to 11, then in particular every sequence with σ0M,w=0 _0^M,w=0 does so. Hence φ is a strong eventual true lie⟺∀M,wlimn→∞σnM,w=1. is a strong eventual true lie ∀ M,w\; _n→∞ _n^M,w=1. We next verify the three characterizations using lim sup or lim inf . If φ∈E11 ∈ E_11 and σ0M,w=1 _0^M,w=1, then every occurrence of 11 is followed by a later occurrence of 11, by applying E11E_11 to the corresponding tail model. Hence 11 occurs infinitely often and lim supn→∞σnM,w=1 _n→∞ _n^M,w=1. Conversely, the latter condition immediately gives a positive stage at which φ is true. Thus E11(φ)⟺∀M,w[σ0M,w=1⇒lim supn→∞σnM,w=1].E_11( ) ∀ M,w\,[ _0^M,w=1 _n→∞ _n^M,w=1]. The same argument gives E00(φ)⟺∀M,w[σ0M,w=0⇒lim infn→∞σnM,w=0]E_00( ) ∀ M,w\,[ _0^M,w=0 _n→∞ _n^M,w=0]. For E01E_01, suppose first that E01(φ)E_01( ) holds and take any pointed model M,wM,w. If 11 occurred only finitely often, then σnM,w=0 _n^M,w=0 for every sufficiently large n. Applying E01(φ)E_01( ) to a tail model beginning at such a stage would give a later occurrence of 11, a contradiction. Hence lim supn→∞σnM,w=1 _n→∞ _n^M,w=1. Conversely, if lim supn→∞σnM,w=1 _n→∞ _n^M,w=1 for every pointed model, then every pointed model with σ0M,w=0 _0^M,w=0 has a positive stage at which φ is true. Therefore E01(φ)⟺∀M,wlim supn→∞σnM,w=1.E_01( ) ∀ M,w\; _n→∞ _n^M,w=1. The uniform finite-bound characterizations in (1) and (4) follow directly from Lemma 4(3). For (3), suppose E01(φ)E_01( ) holds. By the same lemma, there is an N≥1N≥ 1 such that ⊧¬φ→⋁n=1N[↑φ]nφ. → _n=1^N[ ]^n . Take any pointed model M,wM,w. If M1,w⊧φM^1,w , then the required disjunction already holds at stage 11. Otherwise, M1,w⊧¬φM^1,w , so applying the displayed validity to the pointed model M1,wM^1,w yields Mn+1,w⊧φM^n+1,w for some 1≤n≤N1≤ n≤ N. Hence ⊧⋁n=1N+1[↑φ]nφ. _n=1^N+1[ ]^n . The converse follows immediately from the definition of E01(φ)E_01( ). For (2), Lemma 4(4) gives the equivalence of strongly eventual self-refutation, eventual self-refutation, and the existence of an N≥1N≥ 1 such that ⊧[↑φ]N(¬φ∧⋀i∈G□i⊥). [ ]^N ( _i∈ G _i ). The last condition implies limn→∞σnM,w=0 _n→∞ _n^M,w=0 at every pointed model, since after stage N the model is edgeless and φ is false everywhere. Conversely, if limn→∞σnM,w=0 _n→∞ _n^M,w=0 at every pointed model, then every initially true instance of φ eventually becomes false, so E10(φ)E_10( ) holds. The limit condition implies the corresponding lim inf condition. Conversely, if lim infn→∞σnM,w=0 _n→∞ _n^M,w=0 at every pointed model, then every initially true instance becomes false at some positive finite stage, so E10(φ)E_10( ) holds. The implications from strong eventuality to eventuality follow from the definitions. Lemma 4(2) gives the last implication in (1), the last implication in (4), and the implication from an eventual true lie to the remaining conditions in (3). The equivalences involving always informativeness follow from the same lemma and the propositional equivalences between CGφ→φC_G → and φ↔(φ∨CGφ) ( C_G ), and between CGφ→¬φC_G → and φ↔(φ∧¬CGφ) ( C_G ). The single-agent claim follows from Lemma 6, together with the equivalences established above. For |G|≥2|G|≥ 2, strictness in (1) is witnessed by Lemmas 8 and 11. Strictness in (2) follows from Lemma 7. Strictness in (3) follows from the E01∖SE01E_01 SE_01 witness in Lemma 8 and from Lemma 7. Strictness in (4) is witnessed by Lemmas 9 and 12. For larger groups, all additional accessibility relations are interpreted as empty. ∎ In all the four cases, strong eventual notions are characterized by limit and eventual notions are characterized by (i) limit superior or limit inferior, and (i) uniform bounds. Eventual notions further imply the fixed-point views of the sentences φ∧¬CGφ C_G and φ∨CGφ C_G . We can view the result from three sets of categories: preservation (11, 00) vs reversal (10, 01), true-initial (11, 10) vs false-initial (01, 00), and true-target (11, 01) vs false-target (10, 00). On the reversal side, the preconditions for limit and limsup/liminf characterizations can be omitted, Sij<ωS_ij^<ω can be simplified to ⊧CGφ→¬φ C_G → (“common belief of φ implies ¬φ ”) or ⊧CGφ→φ C_G → (“common belief of φ implies φ ”), and there are always informativeness characterizations. On the other hand, those are absent on the preservation side. As for true-initial and false-initial sides, the preservation cases are symmetric in the displayed characterizations, whereas the reversal cases exhibit an additional asymmetry: SE10=E10SE_10=E_10, but SE01⊊E01SE_01 E_01 when |G|≥2|G|≥ 2. Finally, the true-target side has limsup and φ∨CGφ C_G while the false-target side has liminf and φ∧¬CGφ C_G in their characterizations. Next, we analyze, for each (i,j)∈0,12(i,j)∈\0,1\^2, the logical relationship among EijE_ij, SEijSE_ij, EijOrdE_ij^Ord, SEijOrdSE_ij^Ord, Sij<ωS_ij^<ω, and SijOrdS_ij^Ord. We take the three perspectives: strong eventual vs eventual, finite vs transfinite, and what condition SijOrdS_ij^Ord is equivalent to. The incomparability Eii|SEiiOrdE_i SE_i^Ord is not needed from these perspectives, but we record it for completeness since it follows immediately from the preceding lemmas. Theorem 14. For formulas in ℒL: In multi-agent K45, we have the following. In single-agent K45, all the conditions in each item are equivalent. Every displayed right arrow is strict when |G|≥2|G|≥ 2. (1) SE11⇒E11⇒E11Ord⇒S11<ω,S11Ord⇔SE11Ord⇒E11Ord.SE_11 E_11 E^Ord_11 S^<ω_11, S_11^Ord SE_11^Ord E_11^Ord. Moreover, E11∥SEOrd11,SE11∥SEOrd11.E_11 SE^Ord_11, SE_11 SE^Ord_11. (2) SE10⇔E10⇒E10Ord⇔SE10Ord⇔S10Ord⇔S10<ωSE_10 E_10 E_10^Ord SE_10^Ord S_10^Ord S_10^<ω (3) SE01⇒E01⇒E01Ord⇔SE01Ord⇔S01Ord⇔S01<ωSE_01 E_01 E_01^Ord SE_01^Ord S_01^Ord S_01^<ω (4) SE00⇒E00⇒E00Ord⇒S00<ω,S00Ord⇔SE00Ord⇒E00Ord.SE_00 E_00 E^Ord_00 S^<ω_00, S_00^Ord SE_00^Ord E_00^Ord. Moreover, E00∥SEOrd00,SE00∥SEOrd00.E_00 SE^Ord_00, SE_00 SE^Ord_00. Here ∥ denotes incomparability. Proof. The valid implications and the equivalence SijOrd⇔SEijOrdS_ij^Ord SE_ij^Ord follow from Lemma 5. That lemma also gives the four-way equivalence when i≠ji≠ j. Lemma 4(4) gives SE10⇔E10SE_10 E_10, while SE01⇒E01SE_01 E_01 follows directly from the definitions. In the 1111 case, Lemma 8 gives the strictness of SE11⇒E11SE_11 E_11, while Lemma 10 gives θ11SEO∈SE11Ord∖E11 _11^SEO∈ SE_11^Ord E_11, and hence also θ11SEO∈E11Ord∖E11 _11^SEO∈ E_11^Ord E_11. Lemma 11 gives θ11SE∈SE11∖SE11Ord _11^SE∈ SE_11 SE_11^Ord; since SE11⊆E11⊆E11OrdSE_11 E_11 E_11^Ord, this also yields θ11SE∈E11Ord∖SE11Ord _11^SE∈ E_11^Ord SE_11^Ord. These witnesses also establish the two stated incomparability results. Lemma 11 gives θ11<ω∈S11<ω∖E11Ord _11^<ω∈ S_11^<ω E_11^Ord, proving the strictness of E11Ord⇒S11<ωE_11^Ord S_11^<ω. The 0000 case is analogous: Lemma 9 gives the strictness of SE00⇒E00SE_00 E_00, Lemma 10 gives θ00SEO∈SE00Ord∖E00 _00^SEO∈ SE_00^Ord E_00 and hence θ00SEO∈E00Ord∖E00 _00^SEO∈ E_00^Ord E_00, and Lemma 12 gives θ00SE∈SE00∖SE00Ord _00^SE∈ SE_00 SE_00^Ord and hence θ00SE∈E00Ord∖SE00Ord _00^SE∈ E_00^Ord SE_00^Ord. Again these witnesses give the two incomparability results. Lemma 12 gives θ00<ω∈S00<ω∖E00Ord _00^<ω∈ S_00^<ω E_00^Ord, proving the strictness of E00Ord⇒S00<ωE_00^Ord S_00^<ω. For the 1010 and 0101 cases, Lemma 7, together with the ordinal equivalences above, gives Eij⊊EijOrdE_ij E_ij^Ord. Lemma 8 gives SE01⊊E01SE_01 E_01. The single-agent equivalences follow from Lemma 6. ∎ In the multi-agent case with at least two agents, the above theorem shows that strong eventuality implies eventuality in all the four cases, both in the finite and transfinite cases. In the finite case, the converse holds only for the 10 case. In the transfinite cases, the converse holds only in the reversal cases. Also, finite eventuality implies transfinite eventuality but the converse does not hold in all the four cases. On the other hand, finite strong eventuality does not necessarily imply transfinite strong eventuality: finite strong eventuality implies transfinite strong eventuality only on the reversal side. Furthermore, transfinite strong eventuality does not imply finite strong eventuality in all the four cases. In short, “strong” implies “weak” while “finite” does not necessarily imply “transfinite” and vice versa. Note also that the transfinite fixed-point views are equivalent to the transfinite strong eventual notions. Remark 1 (Extension to richer languages). Theorems 13 and 14 remain unchanged for φ∈ℒBPAL _BPAL by Lemma 1. For φ∈ℒC _C or φ∈ℒBPALC _BPALC, all implications and equivalences in the two theorems whose proofs do not use compactness remain valid. More precisely, the following modifications are needed. For Theorem 13, the equivalences between the eventual conditions and their uniform finite-bound characterizations are replaced by the corresponding implications from the uniform finite-bound conditions to the eventual conditions. Thus, for (i,j)∈(1,1),(0,1),(0,0)(i,j)∈\(1,1),(0,1),(0,0)\, ∃N≥1⊧φi→⋁n=1N[↑φ]nφj⟹Eij(φ),∃ N≥ 1\; ^i→ _n=1^N[ ]^n ^j E_ij( ), while the converse is not asserted. The remaining limit and fixed-point characterizations in these three items remain unchanged. In the (1,0)(1,0) case, the corresponding part of the theorem becomes ∃N≥1⊧[↑φ]N(¬φ∧⋀i∈G□i⊥) ∃ N≥ 1\; [ ]^N ( _i∈ G _i ) ⟹SE10(φ)⟺∀M,wlimn→∞σnM,w=0 SE_10( ) ∀ M,w\, _n→∞ _n^M,w=0 ⟹E10(φ)⟺∀M,wlim infn→∞σnM,w=0. E_10( ) ∀ M,w\, _n→∞ _n^M,w=0. The implication from E10E_10 to always informativeness when true, together with the subsequent fixed-point equivalences in Theorem 13(2), also remains valid. In particular, neither E10⇒SE10E_10 SE_10 nor the implication from E10E_10 to the uniform terminal-stage condition above is asserted. For Theorem 14, the only modification is that SE10⇔E10SE_10 E_10 is replaced by SE10⇒E10SE_10 E_10. All the other displayed implications, equivalences, strictness results, and incomparability results remain valid. No strictness claim is made here for the additional implication SE10⇒E10SE_10 E_10. In the single-agent case, the original statements remain unchanged also for ℒBPALCL_BPALC, since on single-agent K45 frames CaψC_\a\ψ is equivalent to □aψ _aψ, and the BPAL reduction axioms then reduce every such formula to a basic epistemic formula. 6 Conclusion We introduced eventual and strong eventual notions for success, self-refutation, true lies, and impossible lies, as well as their transfinite versions. The first theorem shows that strong eventual notions are characterized by limit while eventual notions are characterized by limsup/liminf and the uniform bound conditions. In particular, iterated announcements of any eventually self-refuting formula destroy all the agents’ beliefs by the uniform bound. Eventual notions further imply fixed-point views of the Moore sentence and the self-fulfilling sentence. The second theorem shows that strong eventuality implies eventuality within both the finite and transfinite settings whereas “finite” does not necessarily imply “transfinite” and vice versa. The transfinite fixed-point views are equivalent to transfinite strong eventual notions. In the single-agent case, all the notions in each item in the two theorems are equivalent. Future directions include analyses in multi-agent KD45 and S5 to see which directions fail and which notions become equivalent. Analyses for ℒCL_C and ℒBPALCL_BPALC are left, although most of the results already hold (Remark 1). More fine-grained interpretations and the roles of transfinite iterated announcements are also left (section 2). Connections between our results and unknowability/unbelievability (Yamada, 2026b), and the idea of φ being commonly unbelievable, which was briefly mentioned in Section 3, are also worth exploring. We could relate our results with the classification results of σ-validity (Yamada, 2026a). Acknowledgements I thank Ryo Kashima and Koki Okura for their comments and feedback during seminars. The author used GPT-5.6 Sol (Ultra) and GPT-6 Astra for reasoning, literature search, coding, drawing figures, and proofreading. Some of the proofs were written by these models but were thoroughly checked and modified by the author, who takes full responsibility for the final content. Statements and Declarations Funding This research was supported by the Science Tokyo Support Program for Doctoral Students, funded by the Universities for International Research Excellence. Competing interests The author has no competing interests to declare. Author contributions The author is the sole author of the manuscript. Data availability No datasets were generated or analyzed during the current study. References Ågotnes et al. (2018) T. Ågotnes, H. van Ditmarsch, and Y. Wang True lies. Synthese 195 (10), p. 4581–4615. External Links: Document, Link Cited by: §1, Definition 3, Definition 9. Balbiani et al. (2008) P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi, and T. de Lima ‘Knowable’ as ‘known after an announcement’. The Review of Symbolic Logic 1 (3), p. 305–334. External Links: Document, Link Cited by: footnote 1. Gerbrandy and Groeneveld (1997) J. Gerbrandy and W. Groeneveld Reasoning about information change. Journal of Logic, Language and Information 6 (2), p. 147–169. External Links: Document, Link Cited by: Definition 3. Hintikka (1962) J. Hintikka Knowledge and belief: an introduction to the logic of the two notions. Cornell University Press, Ithaca, NY. Cited by: §1. Holliday and Icard (2010) W. H. Holliday and T. F. Icard Moorean phenomena in epistemic logic. In Advances in Modal Logic 8, L. D. Beklemishev, V. Goranko, and V. Shehtman (Eds.), p. 178–199. External Links: Link Cited by: §1, §1. Klein and Rendsvig (2017) D. Klein and R. K. Rendsvig Convergence, continuity and recurrence in dynamic epistemic logic. In Logic, Rationality, and Interaction (LORI 2017), Lecture Notes in Computer Science, Vol. 10455, p. 71–85. External Links: Document Cited by: §1. Miller and Moss (2005) J. S. Miller and L. S. Moss The undecidability of iterated modal relativization. Studia Logica 79 (3), p. 373–407. External Links: Document Cited by: §1. Moore (1942) G. E. Moore A reply to my critics. In The Philosophy of G. E. Moore, P. A. Schilpp (Ed.), The Library of Living Philosophers, Vol. 4, p. 535–677. Cited by: §1. Plaza (2007) J. Plaza Logics of public communications. Synthese 158, p. 165–179. External Links: Document Cited by: Definition 2. Sadzik (2006) T. Sadzik Exploring the iterated update universe. ILLC Prepublication Series Technical Report P-2006-26, Institute for Logic, Language and Computation (ILLC), University of Amsterdam. External Links: Link Cited by: §1. van Benthem (2007) J. van Benthem Rational dynamics and epistemic logic in games. International Game Theory Review 9 (1), p. 13–45. External Links: Document Cited by: §1, §2. Wittgenstein (1953) L. Wittgenstein Philosophical investigations. Basil Blackwell, Oxford. Note: See Part I, Section x Cited by: §1. Yamada (2026a) E. Yamada Classification of σ-validity in iterated announcements. Note: Version 3, 24 August 2026 External Links: 2607.04685, Document, Link Cited by: §1, §6. Yamada (2026b) E. Yamada The sources of unknowability and self-refutation in epistemic and dynamic epistemic logic. Note: Version 1, 18 September 2026 External Links: 2609.21317, Document, Link Cited by: §1, §6, footnote 1.