Proof. For \(\varphi=\Box_i\psi\), \((\Rightarrow)\) follows from transitivity and \((\Leftarrow)\) follows from Euclideanness. For \(\varphi=\Diamond_i\psi\), the order of the properties is reversed. ◻

Proof.

1. Well-definedness We first show that the displayed equivalence classes are well-defined. For \(0^\omega\), \(\varphi:=\bot\) is \(0^\omega\)-valid and \(0^\omega\)-satisfiable, so \(0^\omega\) is indeed in \(S\). For \(1^\omega\), take \(\varphi:=\top\). For \(10^\omega\), take \(\varphi:=p\land\lnot\Box_i p\). This is 10-valid hence \(10^\omega\)-valid by Lemma 4 and \(10^\omega\)-satisfiable by the S5 (hence K45) model \(M=(W,\{R_i\}_{i\in G},V)\) where \(W=\{w,v\}\), \(R_i=W\times W\) for all \(i\in G\), and \(V(p)=\{w\}\).

   For \(01^k\,(k\geq 1)\), follows from Lemma 9. For \(01^\omega\), \(\varphi:=p\lor\Box_i p\) is non-trivially \(01^\omega\)-valid by Example 1.

   Equality Next, we show the equality. \((\supseteq)\) is clear. \((\subseteq)\): Take any \(\sigma\in S\). Note that \(\sigma\) has length \(\geq 2\).

   If \(\sigma\) starts with 00, \(\sigma\in [0^\omega]\): In fact, let \(\varphi\) be any formula. If \(\varphi\) is \(\sigma\)-valid, then it is \(00\)-valid hence \(0^\omega\)-valid by Lemma 2. Conversely, suppose that \(\varphi\) is \(0^\omega\)-valid. Then, \(\sigma\) cannot contain a 1, since otherwise contradicts \(\sigma\)-satisfiability. Thus, we have \(\sigma\in [0^\omega]\).

   If \(\sigma\) starts with \(11\), \(\sigma\in [1^\omega]\) by the same reasoning as above.

   If \(\sigma\) starts with 10, we have \(\sigma\in [10^\omega]\) by Lemma 4.

   If \(\sigma\) starts with 01, \(\sigma\) is either of the form \(01^k\) for some \(k\geq 1\), or \(01^\omega\), or \(\sigma\) has a prefix of the form \(01^k0\) for some \(k\geq 1\). The last case is impossible by Lemma 7. Thus, we have either \(\sigma\in [01^k]\) for some \(k\geq 1\) or \(\sigma\in [01^\omega]\).

   Disjointness Finally, we show that the equivalence classes are disjoint by a pair-wise check. For \([0^\omega]\) and \([1^\omega]\), \(\Box_i\bot\) is \(1^\omega\)-valid but not \(0^\omega\)-valid. For \([0^\omega]\) and \([10^\omega]\), \(p\) is \(0^\omega\)-valid but not \(10^\omega\)-valid. Disjointness between \([0^\omega]\) and \([01^k]\), \([0^\omega]\) and \([01^\omega]\), and \([1^\omega]\) and \([10^\omega]\) are clear. For \([1^\omega]\) and \([01^k]\), and \([1^\omega]\) and \([01^\omega]\), \(p\) is \(1^\omega\)-valid but not \(01^k\)-valid nor \(01^\omega\)-valid. For \([10^\omega]\) and \([01^k]\), and \([10^\omega]\) and \([01^\omega]\), \(p\lor\Box_i p\) is \(01^k\)-valid and \(01^\omega\)-valid but not \(10^\omega\)-valid since \(p\lor\Box_i p\) is true forever at the K45 model \(M=(W,\{R_i\}_{i\in G}, V),w\) where \(W=\{w\}\), \(R_i=\{(w,w)\}\) for all \(i\in G\), and \(V(p)=W\). For \([01^k]\) and \([01^\omega]\), follows from Lemma 9.

2. Well-definedness For \([10]\), \(\varphi:=p\land\lnot\Box_i p\) is non-trivially \(10\)-valid. For \([101^\omega]\), follows from Lemmas 11 and 5. The arguments are the same for the other equivalence classes.

   Equality Take any \(\sigma\in S\).

   If \(\sigma\) starts with 00, 11, or 01, the same argument as [itm:classification95k45] works.

   If \(\sigma\) starts with 10, there are three possibilities. If \(\sigma\) is 10, \(\sigma\in [10]\). If \(\sigma\) starts with 100, \(\sigma\in[10^\omega]\) by Lemma 4 so \(\sigma\in [10^\omega]\). If \(\sigma\) starts with 101, then \(\sigma\in [101^\omega]\) by Lemma 5.

   Disjointness We separate the displayed equivalence classes into \[A=\{[0^\omega], \bigsqcup_{k\geq 1}[01^k], [01^\omega], [1^\omega]\}\] and \[B=\{[10], [10^\omega], [101^\omega]\}.\]

   For the disjointness in \(A\), we can use the same witness formulas as in [itm:classification95k45].

   For the disjointness in \(B\): For \([10]\) and \([10^\omega]\), there is a 10-valid formula that is not 100-valid by Lemma 4. For \([10]\), \([101^\omega]\), \(p\land\lnot\Box p\) is 10-valid but not \(101^\omega\)-valid so they are disjoint. For \([10^\omega]\) and \([101^\omega]\), \(p\land\lnot\Box p\) is \(10^\omega\)-valid but not \(101^\omega\)-valid.

   For the disjointness between \(A\) and \(B\): For the elements \([10],[10^\omega],[101^\omega]\) in \(B\) and the elements \([0^\omega],[1^\omega]\) in \(A\), \(p\) is both \(0^\omega\)-valid and \(1^\omega\)-valid but not \(10\)-valid. For the elements \([10],[10^\omega],[101^\omega]\) in \(B\) and \([01^k],[01^\omega]\) in \(A\), \(p\lor\Box p\) is both \(01^k\)-valid and \(01^\omega\)-valid but not \(10\)-valid. Therefore, the elements in \(A\) and the elements in \(B\) are disjoint.

3. Well-definedness For \([0^k]\,(k\geq 2)\), follows from Lemma 10. The arguments are the same for the other equivalence classes.

   Equality Take any \(\sigma\in S\).

   If \(\sigma\) starts with 0, \(\sigma\) is in one of the following equivalence classes: \[[0^k]\;(k\ge 2),\qquad [0^\omega],\qquad [01^k]\;(k\ge 1),\qquad [01^\omega].\] In fact, if \(\sigma\) starts with \(01\), it is either in \([01^k]\) for some \(k\geq 1\) or \([01^\omega]\) since there is no non-trivially \(01^k0\)-valid formula for each \(k\geq 1\) by Lemma 7. Also, if \(\sigma\) starts with \(00\), it is either in \([0^k]\) for some \(k\geq 2\) or \([0^\omega]\) since there is no non-trivially \(0^k1\)-valid formula for each \(k\geq 2\) by Lemma 6.

   If \(\sigma\) starts with 1, \(\sigma\) is in one of the following equivalence classes: \[[10],\qquad [10^\omega],\qquad [101^\omega], \qquad [1^\omega].\] In fact, if \(\sigma\) starts with 11, \(\sigma\in [1^\omega]\) by Lemma 3. If \(\sigma\) is \(10\), \(\sigma\in [10]\). If \(\sigma\) starts with 101, \(\sigma\in [101^\omega]\) by Lemma 5. If \(\sigma\) starts with 100, \(\sigma\in [10^\omega]\) by Lemma 4.

   Disjointness We separate the displayed equivalence classes into \[A=\{[0^\omega], \bigsqcup_{k\geq 1}[01^k], [01^\omega], [10], [10^\omega], [101^\omega], [1^\omega]\}\] and \[B=\{\bigsqcup_{k\geq 2}[0^k]\}.\] For the disjointness in \(A\), we can use the same witnesses as [itm:classification95single95kd45]. For the disjointness in \(B\), use Lemma 10.

   It remains to compare the classes in \(A\) with those in \(B\). Fix \(k\geq 2\). First, \([0^k]\neq [0^\omega]\) by Lemma 10. Second, \([0^k]\neq [1^\omega]\) since \(\Box_i\bot\) is \(1^\omega\)-valid but not \(0^k\)-valid. In fact, after the announcement of \(\Box_i\bot\), all \(i\)-arrows are deleted, making \(\Box_i\bot\) true. Finally, \(p\) separates \([0^k]\) from all the remaining classes in \(A\).

 ◻

Proof. Well-definedness The same argument in the multi-agent S5 case (Theorem 1 [itm:classification95s5]) works.

Equality Take any \(\sigma\in S\).

If \(\sigma\) starts with \(00\), we have either \(\sigma\in [0^\omega]\) or \(\sigma\in [0^k]\) for some \(k\geq 2\). In fact, \(\sigma\) cannot have a prefix of the form \(0^k1\) for some \(k\geq 2\) by Conjecture 2 [itm:nonexistence95conj95of950k195multi95kd45].

If \(\sigma\) starts with \(01\), we have either \(\sigma\in [01^k]\) for some \(k\geq 1\) or \(\sigma\in [01^\omega]\) by Conjecture 2 [itm:nonexistence95conj95of9501k095kd45].

If \(\sigma\) starts with \(10\), there are three cases. If \(\sigma=10\), then \(\sigma\in[10]\). If \(\sigma\) starts with \(100\), \(\sigma\in [10^\omega]\) by 4. If \(\sigma\) starts with \(101\), then \(\sigma\in[101^\omega]\) by Lemma 5.

If \(\sigma\) starts with \(11\), \(\sigma\in [1^\omega]\) by Lemma 3.

Disjointness The same argument in the multi-agent S5 case (Theorem 1 [itm:classification95s5]) works. ◻

Proof. Let \(\varphi\) be any 00-valid formula and \(M,w\) be any model. If \(M,w\models\lnot\varphi\), we have \(M|\varphi,w\models\lnot\varphi\) by 00-validity.

Multi-agent K45 Since \(M|\varphi\) is again a K45 model, we must have \(M|^2\varphi,w\models\lnot\varphi\). Continuing this reasoning, we have that \(\varphi\) is \(0^\omega\)-valid.

Single-agent KD45 If \(R|\varphi(w)=\varnothing\), the model never changes so \(\varphi\) is \(0^\omega\)-valid. If \(R|\varphi(w)\neq\varnothing\), the generated submodel \(M_w\) is again KD45 since \(R|\varphi(w)=R|\varphi(v)\) for all \(v\in M_w\). Thus, again we have \(M|^n\varphi,w\models\lnot\varphi\) for all \(n\geq 2\) hence \(\varphi\) is \(0^\omega\)-valid. ◻

Proof. Suppose that \(\varphi\) is \(11\)-valid in multi-agent K45, KD45, or S5 and let \(T_n=\llbracket\varphi\rrbracket_{M|^n\varphi}\). Then, \(T_0\subseteq T_1\), so for any K45, KD45, or S5 model \(M=(W,\{R_i\}_{i\in G},V)\) and \(i\in G\), we have \[R_i|^2\varphi = R_i\cap(W\times T_0)\cap(W\times T_1) = R_i\cap(W\times T_0) = R_i|\varphi.\] Thus, \(M|^2\varphi=M|\varphi\). Now, if \(M,w\models\varphi\), then \(M|\varphi,w\models\varphi\) by 11-validity so the truth of \(\varphi\) at \(w\) remains 1 forever. Thus \(\varphi\) is \(1^\omega\)-valid. ◻

Proof. Multi-agent K45

Suppose that \(\varphi\) is \(10^k\)-valid for some \(k\geq 1\). Suppose that \(M,w\models\varphi\) for some K45 model \(M,w\) and for each \(n\geq 0\), let \(T_n:=\llbracket \varphi\rrbracket_{M|^n\varphi}\). Since \(\varphi\) is \(10\)-valid, we have \(M|\varphi,w\models\lnot\varphi\), so \(T_0\cap T_1=\varnothing\). Thus, \[R_i|^2\varphi=R_i\cap (W\times T_0)\cap (W\times T_1)=R_i\cap (W\times (T_0\cap T_1))=\varnothing.\] This means \(M|^2\varphi=M|^3\varphi=\cdots\) by the monotonicity of arrow-elimination, so \(M|^n\varphi\models\lnot\varphi\) for all \(n\geq 2\). Furthermore, we claim that \(M|^2\varphi,w\models\lnot\varphi\); otherwise, \(M|^2\varphi,w\models\varphi\) and since \(M|^2\varphi\) is again a K45 model (this reasoning fails for KD45), we would have \(M|^3\varphi,w\models\lnot\varphi\), contradicting \(M|^2\varphi=M|^3\varphi\). Thus, \(\varphi\) is \(10^\omega\)-valid.

Multi-agent KD45 and S5 The proof that \(10^k\)-validity implies \(10^{k+1}\)-validity for \(k\geq 2\) is the same as above except that we use 100-validity to claim \(M|^2\varphi,w\models\lnot\varphi\).

For the existence of a formula that is non-trivially 10-valid but not 100-valid, we show that \(\varphi:= (p\wedge\Diamond_a p\wedge\Diamond_a\neg p) \vee \Box_a\bot\) is such an example.³

To show that \(\varphi\) is 10-valid, let \(M,w\) be any KD45 model and suppose that \(M,w\models\varphi\). Then \(M,w\models p\land\Diamond_a p\land\Diamond_a\lnot p\) since \(\Box_a\bot\) is false. Take any \(u\in W\) with \(wR_a u\). Then, \(M,u\models\Diamond_a p\land\Diamond_a\lnot p\) by Lemma 1, so \(u\in M|\varphi\) iff \(M,u\models\varphi\) iff \(M,u\models p\). Thus, \(M|\varphi,w\models\Box_a p\) so \(M|\varphi,w\not\models\Diamond_a\lnot p\). Also, \(M|\varphi,w\not\models\Box_a\bot\) by \(M,w\models\Diamond_a p\) and \(M,u\models\Diamond_a p\land\Diamond_a \lnot p\) for all \(u\in W\) with \(wR_au\). Thus, we have \(M|\varphi,w\not\models\varphi\) hence \(\varphi\) is 10-valid.

To show that \(\varphi\) is not 100-valid, define \(M=(W, \{R_i\}_{i\in G}, V)\) by \(W=\{w,u,v\}\), \(R_i=W\times W\) for all \(i\in G\), and \(V(p)=\{w,u\}\).

Then, we have \(M,w\models\varphi\), \(M|\varphi,w\models\lnot\varphi\) but \(M|^2\varphi,w\models\varphi\), as can be seen from the figure. Thus, \(\varphi\) is non-trivially 10-valid but not 100-valid. ◻

Proof. If \(\varphi\) is \(101\)-valid, then \(T_0\cap T_1=\varnothing\). Hence, for all \(i\in G\), \(R_i|^2\varphi = R_i\cap(W\times T_0)\cap(W\times T_1) = \varnothing\), so we have \(M|^2\varphi=M|^3\varphi=\cdots\). Thus, \(\varphi\) is \(101^\omega\)-valid. ◻

Proof. Suppose toward a contradiction that there is a non-trivially \(0^k1\)-valid formula \(\varphi\) for some \(k\geq 2\). Then there is a finite S5 model \(M,w\) such that \(M,w\models\lnot\varphi,M|\varphi,w\models\lnot\varphi,\ldots,M|^{k-1}\varphi,w\models\lnot\varphi,M|^k\varphi,w\models\varphi\). Let \(A_0=W\) and \(A_k=\bigcap_{j<k}T_j\) for \(k\geq 1\) where \(T_j=\llbracket\varphi\rrbracket_{M|^j\varphi}\). Note that \(\{A_k\}_{k=0}^\infty\) is a decreasing sequence and \(R_i|^k\varphi=R_i\cap (W\times A_k)\) holds. Since the truth of \(\varphi\) at \(w\) changes when shifting from \(M|^{k-1}\varphi\) to \(M|^k\varphi\), we must have \(A_{k-1}\supsetneq A_k\).

Take a \(u\in A_{k-1}\backslash A_k\). Then, \(M|^{k-1}\varphi,u\models\lnot\varphi\) by \(u\notin T_{k-1}\). Now consider the submodel \(M\restriction A_{k-1}\). Since \(M\) is S5, \(M\restriction A_{k-1}\) is also S5, so we have \[\begin{align} (M\restriction A_{k-1}),u&\models\lnot\varphi, \,(M\restriction A_{k-1})|\varphi,u\models\lnot\varphi, \ldots,\, (M\restriction A_{k-1})|^{k-1}\varphi,u\models\lnot\varphi,\\ (M\restriction A_{k-1})|^k\varphi,u&\models\varphi \end{align}\] again by \(0^k1\)-validity of \(\varphi\). Note that in general, the accessibility relations of \(M\restriction A_n\) and \(M|^n\varphi\) for each \(n\geq 1\) are given by \(R_i\cap (A_n\times A_n)\) and \(R_i\cap(W\times A_n)\), respectively, so that \(M\restriction A_n,v\models\psi\iff M|^n\varphi,v\models\psi\) holds for all formulas \(\psi\) and \(v\in A_n\). Thus, from \((M\restriction A_{k-1})|^{k-1}\varphi,u\models\lnot\varphi\) and \((M\restriction A_{k-1})|^k\varphi,u\models\varphi\), we get \(M|^{2k-2}\varphi,u\models\lnot\varphi\) and \(M|^{2k-1}\varphi,u\models\varphi\). This implies \(u\in A_{2k-2}\backslash A_{2k-1}\), so \(A_{2k-2}\supsetneq A_{2k-1}\).

Repeating this reasoning gives infinitely many strict decreases, contradicting that \(M\) is finite. Therefore, there is no non-trivially \(0^k1\)-valid formula for all \(k\geq 2\). ◻

Proof. If there were a non trivially \(01^k0\)-valid formula \(\varphi\), there would be a finite K45, KD45, or S5 model \(M,w\) such that \(M,w\models\lnot\varphi\) by the \(01^k0\)-satisfiability of \(\varphi\) and the finite model property.

Multi-agent K45 and single-agent KD45 If \(M\) is K45, \(M|^n\varphi\) is also K45 for all \(n\geq 1\). We show that this also holds for single-agent KD45. Suppose that \(M\) is single-agent KD45. Suppose for contradiction that \(M|\varphi\) is not serial. Then, \(R|\varphi(w)=\varnothing\) for some \(w\in M|\varphi\). Since \(M\) is serial, choose \(v\) with \(wRv\). Then, by \(R(w)=R(v)\), we have \(R|\varphi(v)=R|\varphi(w)=\varnothing\). Moreover, \(M,v\models\lnot\varphi\) since \(wRv\) and \(R|\varphi(w)=\varnothing\), so we have \(M|\varphi,v\models\varphi\) by \(01^k0\)-validity of \(\varphi\). However, \(R|\varphi(v)=\varnothing\) implies that the truth of \(\varphi\) remains true after that (this part does not apply to multi-agent KD45), contradicting \(01^k0\)-validity. Thus, \(M|\varphi\) is also single-agent KD45, and more generally, \(M|^n\varphi\) is single-agent KD45 for all \(n\geq 1\).

Therefore, both in multi-agent K45 and single-agent KD45, we would have the truth pattern \(0(1^k0)^\omega\), contradicting the fact that the truth of \(\varphi\) at \(w\) must stabilize since \(M\) is finite.

Multi-agent S5 Suppose that \(M\) is S5. By \(01^k0\)-validity, we have \(M,w\models\lnot\varphi,M|\varphi,w\models\varphi,\ldots,M|^k\varphi,w\models\varphi, M|^{k+1}\varphi,w\models\lnot\varphi\). Let \(A_0=W\) and \(A_k=\bigcap_{j<k}T_j\) for \(k\geq 1\) where \(T_j=\llbracket\varphi\rrbracket_{M|^j\varphi}\). Then, \(R_i|^k\varphi=R_i\cap (W\times A_k)\). Since the truth of \(\varphi\) at \(w\) changes when shifting from \(M|^{k}\varphi\) to \(M|^{k+1}\varphi\), we must have \(A_{k}\supsetneq A_{k+1}\). Take any \(u\in A_{k}\supsetneq A_{k+1}\). Then, \(M|^{k}\varphi,u\models\lnot\varphi\) hence \(M\restriction A_{k},u\models\lnot\varphi\). Applying \(01^k0\)-validity to the S5 model \(M\restriction A_{k}\) yields \(A_{2k}\supsetneq A_{2k+1}\) by the same argument as Lemma 6. Repeating this contradicts the fact that \(M\) is finite. Thus, there is no non-trivially \(01^k0\)-valid formula. ◻

Proof. Fix \(k\geq 2\) and let \(P_0,P_1,\ldots,P_{k-1}\) be proposition letters. Let \[A:=P_0\land\bigwedge_{1\leq r\leq k-1}\lnot P_r\] and for \(1\leq j\leq k-1\), \[C_j:=P_j\land\bigwedge_{\substack{0\leq r\leq k-1\\r\neq j}}\lnot P_r.\] So, the formula \(A\) says that only \(P_0\) holds among the proposition letters \(P_0,P_1,\ldots,P_{k-1}\), and \(C_j\) says that only \(P_j\) holds. Let \[B_0:=A\land\Diamond_a\top\land\bigwedge_{j=1}^{k-1}\Diamond_b C_j\land\Box_a(A\land\bigwedge_{j=1}^{k-1}\Diamond_b C_j)\] and for \(1\leq j\leq k-1\), \[B_j:=(A\lor C_j)\land\Box_a\bot\land\bigwedge_{m=1}^{j-1}\Box_b\lnot C_m\land\Diamond_b C_j.\] Finally let \(\varphi_k:=\lnot (B_0\lor B_1\lor\cdots\lor B_{k-1})\).

We show that \(\varphi_k\) is non-trivially \(0^k\)-valid but not \(0^{k+1}\)-valid.

\(\varphi_k\) is \(0^k\)-valid Let \(M\) be any KD45 model and suppose \(M,w\models\lnot\varphi_k\). Then \(M,w\models B_0\lor B_1\lor\cdots\lor B_{k-1}\). Our goal is to show \(M|^n\varphi_k,w\models\lnot\varphi_k\) for all \(1\leq n\leq k-1\). That is, \[M|^n\varphi_k,w\models B_0\lor B_1\lor\cdots\lor B_{k-1}\] for all \(1\leq n\leq k-1\).

We first show \(M|^n\varphi_k,w\models\Box_a\bot\) for all \(n\geq 1\). Since \(M\) is serial, \(\Box_a\bot\) is false at \(M,w\), so we have \(M,w\models B_0\). So, take any \(v\in W\) with \(wR_a v\). Then, we have \(M,v\models A\land \bigwedge_{j=1}^{k-1}\Diamond_b C_j\) by \(M,w\models\Box_a(A\land\bigwedge_{j=1}^{k-1}\Diamond_b C_j\)). Also, \(M,v\models\Diamond_a\top\land\Box_a(A\land\bigwedge_{j=1}^{k-1}\Diamond_b C_j)\) since \(M\) is transitive and Euclidean. Thus, we get \(M,v\models B_0\). This means that all the \(a\)-successor arrows from \(w\) will be deleted after an update so that we have \(M|^n\varphi_k,w\models\Box_a\bot\) for all \(n\geq 1\).

Next, for each \(1\leq j\leq k-1\), choose an \(s_j\in W\) such that \(wR_b s_j\) and \(M,s_j\models C_j\) (this is possible by \(M,w\models B_0\)).

Finally, we show \(M|^n\varphi_k,w\models\lnot\varphi_k\) for all \(1\leq n\leq k-1\). Fix \(1\leq n\leq k-1\). By the claim above, we have \(w(R_b|^n\varphi_k)s_n\) so there is an \(s_j\) such that \(w(R_b|^n\varphi_k)s_j\) with \(1\leq j\leq n\). Let \(m\) be the least such index.

Now, we show \(M|^n\varphi_k,w\models B_m\) in particular. First, \(M|^n\varphi_k,w\models A\) because \(M,w\models B_0\) and valuations never change. Also, \(M|^n\varphi_k,w\models\Box_a\bot\) as already shown. Furthermore, \(M|^n\varphi_k,w\models\bigwedge_{j=1}^{m-1}\Box_b\lnot C_j\land \Diamond_b C_m\) by minimality of \(m\). Thus, \(M|^n\varphi_k,w\models B_m\).

Therefore, \(M|^n\varphi_k,w\models\lnot\varphi_k\) for all \(1\leq n\leq k-1\). Together with the initial assumption that \(M,w\models\lnot\varphi_k\), we conclude that \(\varphi_k\) is \(0^k\)-valid.

\(\varphi_k\) is not \(0^{k+1}\)-valid. Define the KD45 model \(M=(W, \{R_i\}_{i\in G},V)\) by \(W=\{w,s_1,\ldots,s_{k-1}\}\), \(R_a=W\times \{w\}\), \(R_b=W\times \{s_1,\ldots,s_{k-1}\}\), \(R_c=W\times W\) for all \(c\in G\backslash\{a,b\}\), and finally \(V(P_0)=\{w\}\) and \(V(P_j)=\{s_j\}\) for \(1\leq j\leq k-1\). We then have \(M,w\models A\) and \(M,s_j\models C_j\) for \(1\leq j\leq k-1\).

We check the truth of \(\varphi_k\) at each state in the updated models (see Figure 2).

For the initial model \(M\), we have \(M,w\models\lnot\varphi_k\) by \(M,w\models B_0\). Also, \(M,s_j\models\varphi_k\) for all \(1\leq j\leq k-1\) since \(B_0\) is false by \(M,s_j\not\models A\) and \(B_j\) is false by \(M,s_j\not\models\bigwedge_{m=1}^{j-1}\Box_b\lnot C_m\).

For \(M|\varphi_k\), we have \(M|\varphi_k,w\models\lnot\varphi_k\) and \(M|\varphi_k,s_1\models\lnot\varphi_k\) because \(B_1\) holds at \(M|\varphi_k,w\) and \(M|\varphi_k,s_1\). Also, \(M|\varphi_k,s_j\models\varphi_k\) for all \(2\leq j\leq k-1\).

For \(M|^2\varphi_k\), we have \(M|^2\varphi_k,w\models\lnot\varphi_k\) and \(M|^2\varphi_k,s_2\models\lnot\varphi_k\) because \(B_2\) holds at \(M|^2\varphi_k,w\) and \(M|^2\varphi_k,s_2\). Also, \(M|^2\varphi_k,s_j\models\varphi_k\) for all \(3\leq j\leq k-1\).

Continuing this reasoning, we have \(M|^n\varphi_k,w\models\lnot\varphi_k\) for all \(0\leq n\leq k-1\).

On the other hand, we have \(M|^k\varphi_k,w\models\varphi_k\) because \(\Diamond_b C_j\) is false for all \(1\leq j\leq k-1\). Thus, we have the truth pattern \(0^k1^\omega\), so \(\varphi_k\) is not \(0^{k+1}\)-valid. ◻

Proof. Fix \(k\ge 1\). Let \(A_k:=\{r,b,a_0,a_1,\dots,a_{k+1}\}\). For each \(t\in A_k\), take a new propositional letter \(P_t\), and define the formula \[\chi_t:=P_t\wedge\bigwedge_{s\in A_k\setminus\{t\}}\neg P_s.\] Then, define the \(A_k\)-type of state \(w\) in a model \(M\), denoted \(\text{type}_{A_k}\,(w)\) or simply \(\text{type}\,(w)\), to be the unique \(t\in A_k\) such that \(M,t\models\chi_t\) (if such a unique \(t\) exists). So, \(\chi_t\) says that the \(A_k\)-type of the current state is \(t\). For \(X\subseteq A_k\), define \[E_X:=\Box\bigvee_{t\in X}\chi_t\;\wedge\;\bigwedge_{t\in X}\Diamond\chi_t.\] \(E_X\) says that the current successor set contains exactly the types in \(X\). For \(0\le i\le k+1\), let \(X_i:=\{b,a_i,a_{i+1},\dots,a_{k+1}\}\), \(X_{k+2}:=\{b\}\), and \(Y_0:=X_0\cup\{r\}\). Now define \[B_k:= \bigl(\chi_r\wedge(E_{Y_0}\vee E_{X_{k+1}})\bigr) \vee (\chi_{a_0}\lor E_{Y_0}) \lor\bigvee_{i=1}^{k+1}\bigl(\chi_{a_i}\wedge E_{X_i}\bigr),\] and finally \(\varphi_k:=\neg B_k\). \(B_k\) says that either (a) the current state has type \(r\) and the successor types are exactly in \(Y_0\), (b) the current state has type \(r\) and the successor types are exactly in \(X_{k+1}\), (c) the current state has type \(a_0\) and the successor types are exactly in \(Y_0\), or (d) the current state has type \(a_i\) and the successor types are exactly in \(X_i\) for some \(1\leq i \leq k+1\).

\(\varphi_k\) is \(01^k\)-valid We prove that \(\varphi_k\) is \(01^k\)-valid. Let \(M=(W,\{R_i\}_{i\in G},V)\) be any K45 model and suppose \(M,w\models\neg\varphi_k\), i.e., \(M,w\models B_k\). Note that if \(wR_iv\), then \(R_i(w)=R_i(v)\) for all \(i\in G\) and \(w,v\in W\) by Lemma 1, so the successor types of \(w\) agree with those of \(v\).

(a) If \(\text{type}\,(w)=r\) and \(M,w\models E_{Y_0}\), \(\varphi_k\) is false only at \(r\) and \(a_0\) among the types in \(Y_0\) (see the model \(M\) in Figure [fig:type95transition95for95a959501k95but95not9501kplus1]). Thus, after the announcement of \(\varphi_k\), only the types \(r\) and \(a_0\) are deleted, changing the successor type \(Y_0\) to \(X_1\). Also, \(M|\varphi_k,w\models\varphi_k\) since \(\text{type}\,(w)=r\) but \(w\) satisfies neither \(E_{Y_0}\) nor \(E_{X_{k+1}}\). Repeating this, the successor type eventually becomes \(X_{k+2}=\{b\}\) and stabilizes there. In this process, we have the truth pattern \(01^k01^\omega\) at \(w\).

(b) If \(\text{type}\,(w)=r\) and \(M,w\models E_{X_{k+1}}\), we have the truth pattern \(01^\omega\) as in Figure [fig:type95transition95for95b9501k95but95not9501kplus1].

(c) If \(\text{type}\,(w)=a_0\) and \(M,w\models E_{Y_0}\), we have the truth pattern \(01^\omega\) as in Figure [fig:type95transition95for95c9501k95but95not9501kplus1] (with some modification to the figure).

(d) If \(\text{type}\,(w)=a_i\) and \(M,w\models E_{X_i}\) for some \(0\leq i\leq k+1\), we have the truth pattern \(01^\omega\) as in Figure [fig:type95transition95for95c9501k95but95not9501kplus1].

Therefore, \(\varphi_k\) is indeed \(01^k\)-valid.

\(\varphi_k\) is not \(01^{k+1}\)-valid Next, we show that \(\varphi_k\) is not \(01^{k+1}\)-valid. Define the S5 model \(M=(W,R, V)\) by \(W=\{w_r, w_{b},w_{a_0},\ldots,w_{a_{k+1}}\}\), \(R=W\times W\), and \(V(P_t)=\{w_t\}\) for each \(t\in A_k\). Then, the truth of \(\varphi_k\) at \(w_r\) follows \(01^k01^\omega\) as in Figure [fig:type95transition95for95a959501k95but95not9501kplus1], so \(\varphi_k\) is not \(01^{k+1}\)-valid.

Thus, there is a formula that is non-trivially \(01^k\)-valid but not \(01^{k+1}\)-valid. ◻

Proof. Fix \(k \geq 2\) and let \(A_k := \{a_0,a_1,\ldots,a_k\}\). For each \(t\in A_k\), take a new propositional letter \(P_t\), and define \(\chi_t := P_t \wedge \bigwedge_{s\in A_k\setminus\{t\}}\neg P_s\). For each \(X\subseteq A_k\), define \(E_X := \Box \bigvee_{t\in X}\chi_t \wedge \bigwedge_{t\in X}\Diamond\chi_t\) with the convention that \(E_\emptyset := \Box\bot\). For \(0\leq i\leq k\), let \(X_i := \{a_i,a_{i+1},\ldots,a_k\}\) and \(X_{k+1}:=\emptyset\). Define the formula \[B_k := \left( \chi_{a_0}\wedge \bigvee_{\ell=0}^{k-1} E_{X_\ell} \right) \vee \left(\chi_{a_1}\land\bigvee_{\ell=1}^k E_{X_\ell}\right)\lor\bigvee_{i=2}^{k} \left( \chi_{a_i}\wedge \bigvee_{\ell=i}^{k+1} E_{X_\ell} \right)\] and finally let \(\varphi_k := \neg B_k\).

\(\varphi_k\) is \(0^k\)-valid We first show that \(\varphi_k\) is \(0^k\)-valid. Let \(M\) be any S5 model and suppose that \(M,w\models\neg\varphi_k\), i.e. \(M,w\models B_k\). Note that for all \(0\leq i\leq k\), if \(\text{type}(w)=a_i\), then we actually have \[M,w\models\chi_{a_i}\land E_{X_i}\] since the successor type set of \(w\) must contain \(a_i\) by reflexivity.

(a) If \(\text{type}(w)=a_0\) and \(M,w\models E_{X_0}\), \(\varphi_k\) is false exactly at \(w\) and \(a_0\) in \(M\) so after the announcement of \(\varphi_k\), the successor type set of \(w\) becomes \(X_1\) as in Figure [fig:0k-valid95but95not95095kplus1-valid95a]. Repeating this, we have the truth pattern \(0^k1^\omega\)-valid.

(b) If \(\text{type}(w)=a_1\) and \(M,w\models E_{X_1}\), we have the truth pattern \(0^k1^\omega\) as in Figure [fig:0k-valid95but95not95095kplus1-valid95b].

(c) If \(\text{type}(w)=a_i\) and \(M,w\models E_{X_\ell}\) for some \(2\leq i\leq k\) and \(i\leq \ell\leq k+1\), we have the truth pattern \(0^\omega\) as in Figure [fig:0k-valid95but95not95095kplus1-valid95c].

Thus, \(\varphi_k\) is \(0^k\)-valid.

\(\varphi_k\) is not \(0^{k+1}\)-valid It remains to show that \(\varphi_k\) is \(0^k\)-satisfiable but not \(0^{k+1}\)-valid. Take the S5 model \(M=(W,R,V)\) such that \(W=\{w_{a_0},w_{a_1},\ldots,w_{a_k}\}\), \(R=W\times W\), and \(V(P_{a_i})=\{w_{a_i}\}\) for all \(0\leq i\leq k\). Then, the announcements proceed as in case (a) so that \(\varphi_k\) is \(0^k\)-satisfiable but not \(0^{k+1}\)-valid.

Thus, \(\varphi_k\) is non-trivially \(0^k\)-valid but not \(0^{k+1}\)-valid in multi-agent S5. ◻

Proof. See the footnote in Lemma 4. ◻