Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. For the direction from left to right, suppose that . Then there are $w,w^{\prime }\in W$ and a valuation V such that , and $Rww^{\prime }$ . By the semantics, it holds that $Rw^{\prime }w$ . Now we have $Rww^{\prime }$ and $Rw^{\prime }w$ . However, by $w\not \in V(q)$ and $w^{\prime }\in V(q)$ , it follows that $w\not =w^{\prime }$ . Therefore, .

For the converse direction, assume that . Then there are $w,w^{\prime }\in W$ such that $w\not =w^{\prime }$ , $Rww^{\prime }$ and $Rw^{\prime }w$ . Define a valuation V such that $V(p)=\{w\}$ and $V(q)=\{w^{\prime }\}$ . Consequently, we obtain and . Thus, . The proof is completed.

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. For the direction from left to right, suppose that $\mathcal {F}\nvDash \neg p\land \Diamond \blacksquare p\to \Diamond \Box \neg p$ . Then there exist $w\in W$ and a valuation V such that . Consequently, there exists $w_{1}\in R(w)$ such that . Thus it holds that $\neg Rw_{1}w$ . Furthermore, from , we know that each $v\in R(w)$ overlaps $w_{1}$ . Thus, we do not have .

For the direction from right to left, assume that and . Then there are $w,w_{1}\in W$ such that $Rww_{1}$ , $\neg Rw_{1}w$ , and for all $o\in R(w)$ , there exists $o^{\prime }\in W$ with $Rw_{1}o^{\prime }\land Roo^{\prime }$ . Define a valuation V such that $V(p)=R(w_{1})$ . Then we obtain . By , it holds that . Namely, there exists $v\in R(w)$ such that , so v is disjoint from $w_{1}$ . This completes the proof.

Proof. Consider two frames $\mathcal {F}_{1}=\langle W_{1},R_{1} \rangle $ and $\mathcal {F}_{2}=\langle W_{2},R_{2} \rangle $ depicted in Figure 1. Define a function $f:W_{1}\to W_{2}$ such that $f(w_{1})=v_{1}$ and $f(w_{2})=f(w_{3})=v_{2}$ . Then, for any $s,t\in W_{1}$ and $v\in W_{2}$ , if $R_{1}st$ , then $R_{2}f(s)f(t)$ ; if $R_{2}f(s)v$ , then there exists $u\in W_{1}$ such that $f(u)=v$ and $R_{1}sv$ . Hence, f is a bounded morphism from $\mathcal {F}_{1}$ to $\mathcal {F}_{2}$ (cf. [Reference Blackburn, de Rijke and Venema1, sec. 3.3]). So, for any $\varphi \in \mathcal {L}_{\Box }$ , if then . If Supplementation can be defined by some formula $\varphi ^{\prime }$ of $\mathcal {L}_{\Box }$ , then for each frame $\mathcal {F}$ , iff . However, since and , we know and $\mathcal {F}_{2}\nvDash \varphi ^{\prime }$ . By the Goldblatt-Thomason Theorem, Supplementation cannot be defined by $\mathcal {L}_{\Box }$ .

Fig. 1 A bounded morphism (for Supplementation).

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. From left to right, suppose that $\mathcal {F}\nvDash \blacksquare p\to \Box _{u}(\neg p\to \Diamond \Box \neg p)$ . Then there exist $w\in W$ and a valuation V such that and $\langle \mathcal {F},V \rangle ,w\nvDash \Box _{u}(\neg p\to \Diamond \Box \neg p)$ . Thus, there exists $w_{1}\in W$ with . Since , we have $\neg Rww_{1}$ . Moreover, for any $v_{1}\in R(w_{1})$ , there exists $v_{2}\in R(v_{1})$ such that $Rwv_{2}$ .

Now, we have $\neg Rww_{1}$ , and for all $v_{1}\in W$ , if $Rw_{1}v_{1}$ , then there exists $v_{2}\in W$ such that $Rv_{1}v_{2}$ and $Rwv_{2}$ . Consequently, .

For the converse direction, assume that . Therefore, there are $w,w_{1}\in W$ with $\neg Rww_{1}\land \forall z(Rw_{1}z\to \exists v(Rzv\land Rwv)))$ .

Define a valuation V such that $V(p)=R(w)$ ; hence . By $\neg Rww_{1}$ , it holds that . Furthermore, for all $v_{1}\in R(w_{1})$ , there exists $v_{2}\in R(v_{1})$ such that $Rwv_{2}$ . By $V(p)$ , it follows that . Consequently, $\langle \mathcal {F},V \rangle ,w\nvDash \Box _{u}(\neg p\to \Diamond \Box \neg p)$ . Thus, $\langle \mathcal {F},V \rangle ,w\nvDash \blacksquare p\to \Box _{u}(\neg p\to \Diamond \Box \neg p)$ .

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. From left to right, suppose that and $\mathcal {F}\nvDash \blacksquare p\land \Diamond _{u} \blacksquare q\land \Diamond (p\land q)\to \Diamond _{u}\blacksquare (p\land q)$ . Then there exist $w\in W$ and a valuation V such that . Therefore, there exists $v\in W$ with . Additionally, for any $o\in W$ , it holds that $\langle \mathcal {F},V \rangle ,o\nvDash \blacksquare (p\land q)$ , i.e., .

From , we know that w overlaps v. By , there exists $s\in W$ such that for any $t\in W$ , $Rst\leftrightarrow (Rwt\land Rvt)$ . Now let us consider the two cases of s. First, when , there exists $s^{\prime }\in R(s)$ such that . We now conclude that $\neg Rws^{\prime }\lor \neg Rvs^{\prime }$ , which entails a contradiction. Next, if , then there exists $s^{\prime }\in W$ such that and $\neg Rss^{\prime }$ . However, by , we obtain $Rws^{\prime }\land Rvs^{\prime }$ which also contradicts .

For the converse direction, assume for reductio that and . Then there are $w_{1},w_{2},w_{3}\in W$ with $Rw_{1}w_{3}$ and $Rw_{2}w_{3}$ , and for each $u\in W$ there exists $t\in W$ such that $\neg (Rut\leftrightarrow (Rw_{1}t\land Rw_{2}t))$ .

Define a valuation V such that $V(p)=R(w_{1})$ and $V(q)=R(w_{2})$ , thus . By $Rw_{1}w_{3}$ and $Rw_{2}w_{3}$ , it holds that . By assumption, there exists $w\in W$ such that . Moreover, there exists $w^{\prime }\in W$ such that $\neg (Rww^{\prime }\leftrightarrow (Rw_{1}w^{\prime }\land Rw_{2}w^{\prime }))$ .

When $\neg Rww^{\prime }\land Rw_{1}w^{\prime }\land Rw_{2}w^{\prime }$ , it holds that . Also, we can obtain $\langle \mathcal {F},V \rangle ,w\nvDash \Box (p\land q)$ if $Rww^{\prime }\land \neg (Rw_{1}w^{\prime }\land Rw_{2}w^{\prime })$ . Each of them implies a contradiction. Now the proof is completed.

Proof. Consider the two frames $\mathcal {F}=\langle W,R \rangle $ and $\mathcal {F}^{\prime }=\langle W^{\prime },R^{\prime } \rangle $ depicted in Figure 2. Observe that $\mathcal {F}^{\prime }=\langle W^{\prime },R^{\prime } \rangle $ is a subframe of $\mathcal {F}$ . Moreover, for any $s\in W^{\prime }$ , if $Rst$ , then $t\in W^{\prime }$ . Therefore, $\mathcal {F}^{\prime }$ is a generated subframe of $\mathcal {F}$ . By the well-known Goldblatt–Thomason Theorem, for any $\varphi \in \mathcal {L}_{\Box }$ , follows from (see, e.g., [Reference Blackburn, de Rijke and Venema1, sec. 3.3]). However, we have and . Specifically, in frame $\mathcal {F}^{\prime }$ , $w_{2}$ and $w_{3}$ overlap, but they have no product. Hence the property cannot be defined by $\mathcal {L}_{\Box }$ .

Fig. 2 A generated subframe (for Finite Product).

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. From left to right, suppose that . Then there are $w_{1},w_{2},w_{3}\in W$ such that $Rw_{3}w_{1}$ , $Rw_{3}w_{2}$ , and for each $o\in W$ , there is a $w\in W$ with $\neg (Row\leftrightarrow (Rw_{1}w\lor Rw_{2}w))$ .

Define a valuation V such that $V(p)=R(w_{1})$ and $V(q)=R(w_{2})$ . Now it holds that , and . Furthermore, for all $o\in W$ , if there exists $w\in W$ such that $Row$ and $\neg Rw_{1}w\land \neg Rw_{2}w$ , then , and if there exists $w\in W$ with $\neg Row$ and $Rw_{1}w\lor Rw_{2}w$ , then . Each of them shows that for all $o\in W$ , . Thus we conclude that .

For the converse direction, assume that . Then there exist $w,w_{1},w_{2}\in W$ and a valuation V such that $Rww_{1}$ , $Rww_{2}$ , $V(p)=R(w_{1})$ and $V(q)=R(w_{2})$ . For all $o\in W$ , it holds that .

If , then there exists $o^{\prime }\in W$ such that $Roo^{\prime }$ , $\neg Rw_{1}o^{\prime }$ and $\neg Rw_{2}o^{\prime }$ . Thus, $\neg (Roo^{\prime }\to (Rw_{1}o^{\prime }\lor Rw_{2}o^{\prime }))$ . If , then there exists $o^{\prime }\in W$ with $\neg Roo^{\prime }$ and $(Rw_{1}o^{\prime }\lor Rw_{2}o^{\prime })$ ; consequently, $\neg ((Rw_{1}o^{\prime }\lor Rw_{2}o^{\prime })\to Roo^{\prime })$ . So we have $\forall o\exists o^{\prime }\neg (Roo^{\prime }\leftrightarrow (Rw_{1}o^{\prime }\lor Rw_{2}o^{\prime }))$ . This completes the proof.

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be an EM-frame. For the direction from left to right, suppose that . Then there exist $w\in W$ and a valuation V such that .

By , there are $w_{1},w_{2}\in R(w)$ such that and . By , for all $o\in W$ , either or . Now given an arbitrary $w^{\prime }\in W$ , we consider these two cases.

If , then there exists $w^{\prime \prime }\in R(w^{\prime })$ such that . Thus $w^{\prime \prime }$ is disjoint from both $w_{1}$ and $w_{2}$ . Furthermore, by Reflexivity, $Rw^{\prime }w^{\prime \prime }$ entails that objects $w^{\prime }$ and $w^{\prime \prime }$ overlap.

If , then there exists $w^{\prime \prime }\in V(p)\cup V(q)$ such that $\neg Rw^{\prime }w^{\prime \prime }$ . W.l.o.g., suppose $w^{\prime \prime }\in V(p)$ . It follows that $Rw_{1}w^{\prime \prime }$ since . By Strong Supplementation, $w^{\prime \prime }$ has a successor $w^{\prime \prime }_{1}$ that is disjoint from $w^{\prime }$ . By Transitivity, $Rw_{1}w^{\prime \prime }_{1}$ . Thus, $w^{\prime \prime }_{1}$ overlaps $w_{1}$ but $w^{\prime \prime }_{1}$ is disjoint from $w^{\prime }$ . The case for supposing $w^{\prime \prime }\in V(q)$ is similar.

By these two cases, we can conclude that for all $o\in W$ , there exists $o^{\prime }\in W$ such that either o overlaps $o^{\prime }$ that is disjoint from both $w_{1}$ and $w_{2}$ , or that $o^{\prime }$ is disjoint from o and overlaps $w_{1}$ or $w_{2}$ . Each of them indicates that .

For the other direction, assume that and . Then there are $w,w_{1},w_{2}\in W$ with $Rww_{1}$ and $Rww_{2}$ . Moreover, for all $o\in W$ , there exists $o^{\prime }\in W$ such that o overlaps $o^{\prime }$ , and $o^{\prime }$ is disjoint from both $w_{1}$ and $w_{2}$ ; or that $o^{\prime }$ overlaps $w_{1}$ or $w_{2}$ , and o is disjoint from $o^{\prime }$ ( $\star $ ).

Define a valuation V such that $V(p)=R(w_{1})$ and $V(q)=R(w_{2})$ . Then, . By the assumption, there exists $o_{1}\in W$ such that . By ( $\star $ ), there is an $o^{\prime }$ for this $o_{1}$ . Now we consider the two cases stated in ( $\star $ ).

First, $o_{1}$ overlaps $o^{\prime }$ , and $o^{\prime }$ is disjoint from both $w_{1}$ and $w_{2}$ . It holds directly that . Additionally, since $o_{1}$ overlaps $o^{\prime }$ , by Transitivity, we have .

Next, $o^{\prime }$ overlaps $w_{1}$ or $w_{2}$ , and $o^{\prime }$ is disjoint from $o_{1}$ . So, . Furthermore, since $o^{\prime }$ is disjoint from $o_{1}$ , we can obtain .

Each of these two cases entails a contradiction. Thus we conclude that if , then .

Proof. Consider the two frames $\mathcal {F}=\langle W,R \rangle $ and $\mathcal {F}^{\prime }=\langle W^{\prime },R^{\prime } \rangle $ depicted in Figure 3. As an observation, notice $\mathcal {F}^{\prime }=\langle W^{\prime },R^{\prime } \rangle $ is a generated subframe of $\mathcal {F}$ . However, we have and . For instance, in the frame $\mathcal {F}^{\prime }$ , $s_{3}$ underlaps $s_{4}$ , and both of them are parts of $s_{6}$ . However, $s_{6}$ also overlaps $s_{5}$ which is disjoint from both $s_{3}$ and $s_{4}$ . Hence it cannot be defined by $\mathcal {L}_{\Box }$ .

Fig. 3 A generated subframe (for Finite Sum).

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be an EM-frame. From left to right, assume towards a contradiction that and . Then there exist $w\in W$ and a valuation V such that and . Consequently, for every $o\in W$ , either (1) or (2) holds: (1) ; and (2) o has a successor $o^{\prime }\in W$ such that and every $v\in V(p)$ has no q-successors. Now, consider $V(p)$ as the extension for the predicate S in $\mathcal {F}$ , clearly the antecedent $\exists x Sx$ of SO-Fusion holds; thus we have $\exists z \forall y(Oyz\leftrightarrow \exists x(Sx\land Oyx)) (\star )$ , too. Given an arbitrary $o\in W$ , let us consider the above two cases to see whether o can be the witness for z in $(\star )$ .

For (1), if , then there exists $o_{1}\in V(p)$ such that $\neg Roo_{1}$ . By Strong Supplementation, $o_{1}$ has a successor $o_{1}^{\prime }$ that is disjoint from o. Therefore, we have $\neg O o_{1}^{\prime }o$ , but $(So_{1}\land Oo_{1}^{\prime }o_{1})$ . Thus, o cannot be the witness for z in $(\star )$ .

For (2), consider the case that $Roo^{\prime }$ , , and for each $v\in W$ , . Since $o^{\prime }\in R(o)$ , the two objects overlap trivially. Moreover, for any $v\in V(p)$ , it is not hard to see that $o^{\prime }$ is disjoint from v. Therefore we have $Oo^{\prime }o$ but $\neg \exists x (Sx\land Oo^{\prime }x)$ . Thus o cannot be the witness for z in $(\star )$ either.

In sum, no $o\in W$ can be the witness of z in $(\star )$ , contradiction.

From right to left, suppose that and . From the latter there is a non-empty set $X\subseteq W$ such that $\forall z\exists y\neg (Oyz\leftrightarrow \exists x(Sx \land Oyx)) (\dagger )$ holds when assigning S to X. Now, pick one $w\in X$ , let $V(p)=X$ , $V(q)=\{o\in W\mid \neg \exists x(Xx\land Oxo)\}$ , and we have . Thus there is a $v\in W$ , such that . Now by $(\dagger )$ , there is $v^{\prime }$ such that either (1) $(\neg Ovv^{\prime }\land \exists x(Sx \land Ov^{\prime }x))$ or (2) $Ovv^{\prime }\land \forall x(Sx \to \neg Ov^{\prime }x)$ .

Now consider case (1). Formula $\exists x(Sx \land Ov^{\prime }x)$ states that there exists $o\in X$ such that $Oov^{\prime }$ , i.e., there is some $o^{\prime }$ such that $Rv^{\prime }o^{\prime }$ and $Roo^{\prime }$ . Furthermore, since , we have $Rvo$ . Now by Transitivity of EM, $Rvo^{\prime }$ . However then we obtain $Ovv^{\prime }$ , contradicting the first conjunct of (1).

For case (2), by the second conjunct, we have $v^{\prime }\in V(q)$ . Moreover, from the definition of the valuation V, it follows that . Now due to the first conjunct of (2), there is an o such that $Rvo$ and $Rv^{\prime }o$ . Then, by Transitivity, we have . Thus, . Now by $(\circ )$ , , which indicates that there exists an $o^{\prime }\in X$ that has a successor disjoint from any X-point. However, this is impossible since due to Reflexivity, $o^{\prime }$ overlaps with any successor. Now we have arrived at a contradiction. This completes the proof.

Proof. To prove this result, we consider a special case where $\alpha $ is $Rxx$ . Define three frames as follows: $\mathcal {F}_{1}=\langle \{w_{1}\},\{\langle w_{1},w_{1} \rangle \} \rangle $ , $\mathcal {F}_{2}=\langle \{w_{2}\},\{\langle w_{2},w_{2} \rangle \} \rangle $ and $\mathcal {F}_{3}=\langle \{w_{1},w_{2}\},\{\langle w_{1},w_{1} \rangle ,\langle w_{2},w_{2} \rangle \} \rangle $ . Each of $\mathcal {F}_{1}$ and $\mathcal {F}_{2}$ consists of a reflexive point, and frame $\mathcal {F}_{3}$ is the disjoint union of $\mathcal {F}_{1}$ and $\mathcal {F}_{2}$ . Now it is not hard to see that when $i\in \{1,2\}$ , we have . However, in frame $\mathcal {F}_{3}$ both $w_{1}$ and $w_{2}$ satisfy the property $Rxx$ but they are disjoint from each other. So, . Again, by the Goldblatt–Thomason Theorem, the property cannot be defined by $\mathcal {L}_{\Box }$ .

Proof. To prove this, by the Goldblatt–Thomason Theorem, it suffices to give an example showing that the class of Atomicity-frames does not reflect Footnote ¹⁸ ultrafilter extensions. Consider the frame $\mathcal {F}=\langle \mathbb {N},< \rangle $ (the natural numbers with the usual $<$ relation) and its ultrafilter extension $ue(\mathcal {F})$ (cf. [Reference Blackburn, de Rijke and Venema1, sec. 3.3]). It is a matter of direct checking that and . Now the proof is completed.

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. For the direction from left to right, suppose for reductio that and . Then there exist $w\in W$ and a valuation V such that . Since , there exists $v\in W$ with $Rwv\land \neg Rvw$ . By $Rwv$ , it holds that . However, from $\neg Rvw$ and $w\in V(p)$ , we know , which entails a contradiction.

For the other direction, suppose that and . Then there exists $w\in W$ such that for all $w^{\prime }\in W$ , $Rww^{\prime }$ entails $Rw^{\prime }w$ . Now define a valuation V such that $V(p)=\{w\}$ . Since formula is valid, there exists $v\in R(w)$ such that v is not . Then we conclude that $\neg Rvw$ , which entails a contradiction, too. This completes the proof.

Proof. Consider frames $\mathcal {F}_{1}=\langle W_{1},R_{1} \rangle $ and $\mathcal {F}_{2}=\langle W_{2},R_{2} \rangle $ depicted in Figure 4. Define a function $f:W_{1}\to W_{2}$ such that $f(w)=v$ for all $w\in W_{1}$ . Then f is a bounded morphism from $\mathcal {F}_{1}$ to $\mathcal {F}_{2}$ . However, we have and ; therefore by the Goldblatt–Thomason Theorem, Atomlessness is not definable in $\mathcal {L}_{\Box }$ .

Fig. 4 A bounded morphism (for Atomlessness).

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a frame. From left to right, suppose that $\mathcal {F}\nvDash p\land \Diamond _{u} q\to \Diamond _{u}(\Diamond p\land \Diamond q )$ . Then there exist $w,v\in W$ and a valuation V such that , , and for all $o\in W$ , $\langle \mathcal {F},V \rangle ,o \nvDash \Diamond p\land \Diamond q$ . We conclude that w and v have no common predecessor, i.e., .

From right to left, assume that and . Then there are $w,v\in W$ that have not common predecessor. Define the valuation V such that $V(p)=\{w\}$ and $V(q)=\{v\}$ . Consequently, . Since , there exists $o\in W$ with , i.e., o is a common predecessor of w and v, which entails a contradiction.

Proof. First, we prove that all inference rules of $K^{*}$ are derivable in $K^{\sim }$ . To do so, we only need to show that $R^{*}2$ is derivable in $K^{\sim }$ . Suppose that $\neg \varphi $ , i.e., $\varphi \to \bot $ . From $R3$ , it follows that . As is $A7$ , we conclude by $R1$ .

Next, we show that :

Moreover, $K^{*}$ has no formula containing modality $\Box $ , but $K^{\sim }$ has $R2$ as an inference rule. Thus the proof is completed.

Proof.

Proof. Let $\mathcal {F}=\langle W,R \rangle $ be a GM-frame, V a valuation and $w\in W$ . Suppose that . Then there exists $v\in R(w)$ such that for any $u\in W$ , if u is $\varphi $ , then $Rvu$ . By Transitivity, all $\varphi $ -points are successors of w. Therefore, . This completes the proof.

Proof. Consider the generalized frame $\mathcal {F}_{g}$ depicted in Figure 5. It holds that $R_{1}\cup R_{2}=W\times W$ . Let $\varphi :=p$ . We now show that . Define a valuation V such that $V(p)=\{v\}$ . Then it follows that and . Also, we have . Consequently, .

Fig. 5 A generalized frame ( $R_{1}$ is labelled with ‘ $1$ ’, and $R_{2}$ with ‘ $2$ ’).

Next, we show that MGM is valid on $\mathcal {F}_{g}$ . Here we only prove that formulas $A3$ , $A6$ and ) are valid on $\mathcal {F}_{g}$ , and that the validity of -formulas is invariant under $R3$ in $\mathcal {F}_{g}$ .

(1) For each $x\in \{u,v\}$ , suppose that x is $\Box _{u}\varphi $ . Thus, x is $\Box \varphi $ . Since $R_{1}$ in the frame $\mathcal {F}_{g}$ is reflexive, x is $\varphi $ . Consequently, x is $\Box _{u}\varphi \to \varphi $ . Thus, $A3$ is valid on $\mathcal {F}_{g}$ .

(2) If u is , then v is $\neg \varphi \land \neg \psi $ , i.e., $\neg (\varphi \lor \psi )$ . So u is . Similarly, when v is , we can also prove that v is . Thus, $A6$ is valid on $\mathcal {F}_{g}$ .

(3) Suppose that u is . Then, at least one of u and v is . If u is , u is $\psi $ . Thus, is true at u. If v is , then u is $\neg \varphi $ . So formula is always true at u. Similarly, we can prove that is also true at v.

(4). Assume that $\varphi \to \psi $ is valid on $\mathcal {F}_{g}$ . If u is , then v is $\neg \psi \land \varphi $ , i.e., $\neg (\varphi \to \psi )$ , which contradicts our assumption. Similarly, we can prove that v is also . Therefore the validity of -formulas is invariant under $R3$ in $\mathcal {F}_{g}$ .

Hence we conclude that all formulas provable in MGM are valid on $\mathcal {F}_{g}$ , but is not. Now the proof is completed.

Proof. From left to right, suppose for reductio that and . Then there are $w_{1},w_{2},w_{3}\in W$ such that $R_{1}w_{1}w_{2}$ , $R_{2}w_{1}w_{3}$ and $\neg R_{2}w_{2}w_{3}$ . Define a valuation V such that $V(p)=\{w\in W\mid \neg R_{2}w_{2}w\}$ . Consequently, $w_{2}$ is . Since $R_{1}w_{1}w_{2}$ , $w_{1}$ is . Consequently, $w_{1}$ is . Then, from $R_{2}w_{1}w_{3}$ we know that $w_{3}$ is $\neg p$ . Therefore, it holds that $R_{2}w_{2}w_{3}$ , contradiction.

From right to left, assume that . There exist a valuation V and $w_{1}\in W$ such that . So there exists $w_{2}\in W$ such that $R_{1}w_{1}w_{2}$ and $w_{2}$ is . Moreover, as $w_{1}$ is , there exists $w_{3}\in W$ with $R_{2}w_{1}w_{3}$ and $w_{3}\in V(p)$ . However, since $w_{2}$ and $w_{3}$ are, respectively, and p, it holds that $\neg R_{2}w_{2}w_{3}$ . Thus, . Now the proof is completed.

Proof. Let $\mathcal {F}_{g}=\langle W,R_{1},R_{2} \rangle $ be a generalized frame. From left to right, suppose that and . Then there are $w_{1},w_{2}\in W$ such that $R_{1}w_{1}w_{2}$ , $R_{1}w_{2}w_{1}$ , $w_{1}\not =w_{2}$ and $\neg R_{2}w_{2}w_{1}$ . Define a valuation V such that $V(p)=\{w_{1}\}$ and $V(q)=\{w_{2}\}$ . Then, $w_{1}$ is $p\land \neg q$ , and $w_{2}$ is . Therefore, . Consequently, , which entails a contradiction.

From right to left, suppose that . Then there exist a valuation V and $w_{1}\in W$ such that . Therefore, there exists $w_{2}\in W$ such that $R_{1}w_{1}w_{2}$ and $w_{2}$ is . Also, we have $w_{1}\not =w_{2}$ . Furthermore, since $w_{2}$ is , we know $\neg R_{2}w_{2}w_{1}$ from $w_{1}\in V(p)$ . With Definition 4.34, $R_{1}\cup R_{2}=W\times W$ . Thus we obtain $R_{1}w_{2}w_{1}$ . Immediately, we conclude that . The proof is completed.

Proof. 1. Assume that $\Diamond \varphi \in w$ , i.e., $\neg \Box \neg \varphi \in w$ . If $\Box w\cup \{\varphi \}$ is inconsistent, then there exists a finite subset $\{\varphi _{1},\cdots ,\varphi _{n}\} ( n\in \mathbb {N})$ of $\Box w$ such that . If $n=0$ , then by $R2$ , it holds that , which contradicts $\neg \Box \neg \varphi \in w$ . If $n>0$ , then it holds that . However, from $\Box \varphi _{1},\ldots ,\Box \varphi _{n}\in w$ , we can obtain $\Box \neg \varphi \in w$ , which contradicts $\neg \Box \neg \varphi \in w$ . Thus, $\Box w\cup \{\varphi \}$ is consistent. Consequently, there exists a maximal consistent set v with $\Box w\cup \{\varphi \}\subseteq v$ . Therefore, we conclude that w has an $R_{1}^{c}$ -subordinate set v with $\varphi \in v$ .

2. Suppose that . If is inconsistent, then there exists a finite subset $\{\varphi _{1},\ldots ,\varphi _{n}\} (n\in \mathbb {N})$ of such that . If $n=0$ , then , i.e., . By $R3$ , it holds that . From $A7$ and $R1$ , we know , which contradicts . If $n>0$ , then by Theorem 4.26 and the rule $R^{*}2$ , it holds that . By Proposition 4.28, it follows that . Moreover, given Theorem 4.27, it is not hard to see that . Therefore, we have . However, since , it holds that , which contradicts . So is consistent, and there exists a maximal consistent set v with . Thus, w has an $R_{2}^{c}$ -subordinate set v such that $\neg \varphi \in v$ .

Proof. Assume towards a contradiction that there are $w_{1},w_{2},w_{3}\in W^{c}$ such that $R_{1}^{c}w_{1}w_{2}\land R_{2}^{c}w_{1}w_{3}\land \neg R_{2}^{c}w_{2}w_{3}$ . Consequently, there exist formulas and $\varphi $ such that and $\varphi \in w_{3}$ . Also, from $R_{1}^{c}w_{1}w_{2}$ we know . Since , it holds that . In addition, by $R_{2}^{c}w_{1}w_{3}$ , it follows that $\neg \varphi \in w_{3}$ . Now we have arrived at a contradiction.

Proof. If not, then there are $w,v\in W^{c}$ such that $R_{1}^{c}wv\land R_{1}^{c}vw\land \neg R_{2}^{c}vw\land \neg w\equiv v$ . Since $\neg w\equiv v$ , there exists a formula $\psi $ such that $\neg \psi \in w$ and $\psi \in v$ . By $\neg R_{2}^{c}vw$ , there exist formulas and $\varphi $ such that and $\varphi \in w$ . So, , which contradicts the assumption.

Proof. 1. We now prove that $T^{c}=R_{1}^{c}\cup R_{2}^{c}$ . From left to right, suppose that there exist $w,v\in W^{c}$ such that $T^{c}wv$ , $\neg R_{1}^{c}wv$ and $\neg R_{2}^{c}wv$ . Then it holds that $\Box _{u} w\subseteq v$ , $\Box w\not \subseteq v$ and . So there exist such that $\varphi ,\psi \not \in v$ . Since both w and v are maximal consistent sets, we have and $\neg \varphi \land \neg \psi \in v$ . Furthermore, by Proposition 4.29, it holds that $\Box _{u}(\neg \psi \to \varphi )\in w$ . However, from $\Box _{u} w\subseteq v$ , we know $\neg \psi \to \varphi \in v$ , which contradicts $\neg \varphi \land \neg \psi \in v$ .

From right to left, we first consider the case that there exist $w,v\in W^{c}$ with $R_{1}^{c}wv$ and $\neg T^{c}wv$ . Then we have $\Box w\subseteq v$ and $\Box _{u} w\not \subseteq v$ . So there exist $\Box _{u}\varphi \in w$ and $\neg \varphi \in v$ . However, from , $\Box \varphi \in w$ and $\neg \varphi \in v$ , we obtain $\neg R_{1}^{c}wv$ , which entails a contradiction. Similarly, when $R_{2}^{c}wv$ , we can also obtain $T^{c}wv$ .

2. Next we show that $T^{c}$ is an equivalence relation. For each $w\in W^{c}$ , if $\Box _{u}\varphi \in w$ , then by $A3$ , we have $\varphi \in w$ . Thus $T^{c}$ is reflexive. For any $w_{1},w_{2},w_{3}\in W^{c}$ , if $T^{c}w_{1}w_{2}$ and $T^{c}w_{2}w_{3}$ , then $\Box _{u} w_{1}\subseteq w_{2}$ and $\Box _{u} w_{2}\subseteq w_{3}$ . For each $\Box _{u}\varphi \in w_{1}$ , by $A4$ it follows $\Box _{u}\Box _{u}\varphi \in w_{1}$ . Consequently, $\Box _{u}\varphi \in w_{2}$ . Then we have $\varphi \in w_{3}$ , i.e., $T^{c}w_{1}w_{3}$ . So, $T^{c}$ is transitive. For any $w,v\in W^{c}$ , if $T^{c}wv$ and $\neg T^{c}vw$ , then $\Box _{u}w\subseteq v$ and $\Box _{u}v\not \subseteq w$ . By $\Box _{u}v\not \subseteq w$ , there exists $\varphi $ such that $\Box _{u}\varphi \in v$ and $\varphi \not \in w$ . Since both w and v are maximal consistent sets, we have $\Diamond _{u}\neg \varphi \not \in v$ and $\neg \varphi \in w$ . Moreover, from $\neg \varphi \in w$ and $A5$ , it follows that $\Box _{u}\Diamond _{u}\neg \varphi \in w$ . Furthermore, $\Diamond _{u}\neg \varphi \in v$ follows from $T^{c}wv$ , which entails contradiction. Therefore, the relation $T^{c}$ is symmetric. Now the proof is completed.

Proof. Instead of a precise proof for the result, we merely give a few hints why we still have the results for the generated generalized canonical frame. Let $\mathcal {F}_{g}^{c}=\langle W^{c},R_{1}^{c},R_{2}^{c} \rangle $ be the generalized canonical frame, $w\in W^{c}$ , and $\mathcal {F}_{gw}^{c}=\langle W^{c}_{w},R_{1w}^{c},R_{2w}^{c} \rangle $ the generated generalized canonical frame. Let $s\in W^{c}_{w}$ and .

Let $\Diamond \varphi \in s$ . With Lemma 4.40, there exists some $t\in W^{c}$ such that $R_{1}^{c}st$ and $\varphi \in t$ . Therefore, by Proposition 4.45, it follows that $T^{c}ws$ and $T^{c}wt$ . So, $t\in W^{c}_{w}$ . Now, it is easy to see $R_{1w}^{c}st$ . Similarly, we can show the case for .

Proof. We first prove the result given $k=3$ and then show the general case can be reduced to this basic case.

Suppose $\mathcal {R} \langle s_{1}, i_{1} \rangle \langle s_{2}, i_{2} \rangle $ , $\mathcal {R} \langle s_{2}, i_{2} \rangle \langle s_{3}, i_{3} \rangle $ , but not $\mathcal {R} \langle s_{1}, i_{1} \rangle \langle s_{3}, i_{3} \rangle $ . Then by the definition of $\mathcal {R}$ , $R_{1w}^{c}s_{1}s_{2}$ and $R_{1w}^{c}s_{2}s_{3}$ . By the canonicity of Axiom 4 w.r.t. the generalized canonical $\mathcal {F}^{c}_{gw}$ , we have $R_{1w}^{c}s_{1}s_{3}$ . In the following, we show that $R_{2w}^{c}s_{1}s_{3}$ , $R_{2w}^{c}s_{2}s_{3}$ but not $R_{2w}^{c}s_{1}s_{2}$ , namely, the edges between $s_{1}, s_{2}, s_{3}$ are illustrated as below:

where we label $R_{1w}^{c}$ and $R_{2w}^{c}$ with ‘ $1$ ’ and ‘ $2$ ’, respectively, in the graph, and omit the reflexive links.

Since it is not the case that $\mathcal {R} \langle s_{1}, i_{1} \rangle \langle s_{3}, i_{3} \rangle $ but $R_{1w}^{c}s_{1}s_{3}$ , by the definition of $\mathcal {R}$ we have $R_{2w}^{c}s_{1}s_{3}$ . Now since $R_{1w}^{c}s_{1}s_{2}$ , by Proposition 4.37 we have $R_{2w}^{c}s_{2}s_{3}$ .

Finally, towards contradiction let us assume that $R_{2w}^{c}s_{1}s_{2}$ . Since $\mathcal {R} \langle s_{1}, i_{1} \rangle \langle s_{2}, i_{2} \rangle $ , we have either $\langle s_{1}, i_{1} \rangle =\langle s_{2}, i_{2} \rangle $ or $i_{1}< i_{2}$ and $i_{2}$ is even, according to the definition of $\mathcal {R}$ . The first case is not possible since $\mathcal {R} \langle s_{2}, i_{2} \rangle \langle s_{3}, i_{3} \rangle $ but it is not the case that $\mathcal {R} \langle s_{1}, i_{1} \rangle \langle s_{3}, i_{3} \rangle $ . Therefore $i_{1}< i_{2}$ and $i_{2}$ is even. Similarly, since $\mathcal {R} \langle s_{2}, i_{2} \rangle \langle s_{3}, i_{3} \rangle $ , $R_{1w}^{c}s_{2}s_{3}$ and $R_{2w}^{c}s_{2}s_{3}$ we can show that $i_{2}< i_{3}$ and $i_{3}$ is even. Therefore, $i_{1}<i_{3}$ and $i_{3}$ is even. However, this then means that $\mathcal {R} \langle s_{1}, i_{1} \rangle \langle s_{3}, i_{3} \rangle $ according to the definition of $\mathcal {R}$ , which contradicts the assumption. In sum, it cannot be the case that $R_{2w}^{c}s_{1}s_{2}$ .

For the general case, suppose there is an $\mathcal {R}$ -path from $\langle s, i \rangle $ to $\langle s^{\prime }, i^{\prime } \rangle $ in $\mathcal {F}$ such that it is not the case that $\mathcal {R}\langle s, i \rangle \langle s^{\prime }, i^{\prime } \rangle $ . Clearly we can shorten the path while keeping the starting and ending points the same, if two non-adjacent points in the path are also connected by $\mathcal {R}$ . Now let us take one of the shortest subpathsFootnote ²⁴ $\langle s_{1}, i_{1} \rangle \dots \langle s_{k}, i_{k} \rangle $ for some k, such that $\langle s_{1}, i_{1} \rangle =\langle s, i \rangle $ , $\langle s_{k}, i_{k} \rangle =\langle s^{\prime }, i^{\prime } \rangle $ , and for all $j<k$ , $\mathcal {R} \langle s_{j}, i_{j} \rangle \langle s_{j+1}, i_{j+1} \rangle $ . Note that since it is the shortest in length, it is not the case that $\mathcal {R} \langle s_{j}, i_{j} \rangle \langle s_{j^{\prime }}, i_{j^{\prime }} \rangle $ for any $j<j^{\prime }\leq k$ .

Note that $k>2$ , since it is not the case that $\mathcal {R}\langle s, i \rangle \langle s^{\prime }, i^{\prime } \rangle $ . In the following, we show that k must be $3$ , which will reduce the general case to the previous basic case. Suppose $k>3$ and the shortest subpath starts with $\langle s_{1}, i_{1} \rangle \langle s_{2}, i_{2} \rangle \langle s_{3}, i_{3} \rangle \langle s_{4}, i_{4} \rangle \dots $ Footnote ²⁵ . Since it is not the case that $\mathcal {R}\langle s_{1}, i_{1} \rangle \langle s_{3}, i_{3} \rangle $ but $\mathcal {R}\langle s_{1}, i_{1} \rangle \langle s_{2}, i_{2} \rangle $ , and $\mathcal {R}\langle s_{2}, i_{2} \rangle \langle s_{3}, i_{3} \rangle $ , we can follow the discussion for the basic 3-point case and show $R_{2w}^{c}s_{2}s_{3}$ . However, since it is also not the case that $\mathcal {R}\langle s_{2}, i_{2} \rangle \langle s_{4}, i_{4} \rangle $ but $\mathcal {R}\langle s_{2}, i_{2} \rangle \langle s_{3}, i_{3} \rangle $ , and $\mathcal {R}\langle s_{3}, i_{3} \rangle \langle s_{4}, i_{4} \rangle $ , by the conclusion of the basic 3-point case we have $\neg R_{2w}^{c}s_{2}s_{3}$ . Now we have a contradiction, thus k can only be 3 if the shortest subpaths are taken.

Proof. Since $\mathcal {{R}^{+}}$ is the transitive closure of $\mathcal {R}$ , we just need to show that $\mathcal {{R}^{+}}$ is reflexive and anti-symmetric.

We first show that $\mathcal {R}^{+}$ is reflexive. For any $v\in W_{w}^{c}$ and $i\in I_{v}$ , from $v=v$ and $i=i$ , we know $S\langle v,i \rangle \langle v,i \rangle $ . By the canonicity of Axiom T, we have $R_{1w}^{c}vv$ . Consequently, $\mathcal {R}\langle v,i \rangle \langle v,i \rangle $ . Therefore, $\mathcal {R}$ is reflexive, so is $\mathcal {R}^{+}$ .

We then prove that $\mathcal {F}^{+}$ is anti-symmetric. If not, then there are $\langle w_{1},i \rangle ,\langle w_{2},j \rangle \in \mathcal {W}$ such that $\langle w_{1},i \rangle \not =\langle w_{2},j \rangle $ , $\mathcal {R}^{+}\langle w_{1},i \rangle \langle w_{2},j \rangle $ and $\mathcal {R}^{+}\langle w_{2},j \rangle \langle w_{1},i \rangle $ . By the definition of $\mathcal {R}$ and the discussion above, we know that $R_{1w}^{c}w_{1}w_{2}$ and $R_{1w}^{c}w_{2}w_{1}$ . Consider the following situations.

First, consider the case that $\mathcal {R}\langle w_{1},i \rangle \langle w_{2},j \rangle $ and $\mathcal {R}\langle w_{2},j \rangle \langle w_{1},i \rangle $ , i.e., both the edges $\mathcal {R}^{+}\langle w_{1},i \rangle \langle w_{2},j \rangle $ and $\mathcal {R}^{+}\langle w_{2},j \rangle \langle w_{1},i \rangle $ are not new edges added to the frame when taking the transitive closure. Since $R_{1w}^{c}w_{1}w_{2}$ and $R_{1w}^{c}w_{2}w_{1}$ , from Proposition 4.43 it follows that $R_{2w}^{c}w_{2}w_{1}$ or $w_{1}\equiv w_{2}$ . If $w_{1}\equiv w_{2}$ , then from $\langle w_{1},i \rangle \not =\langle w_{2},j \rangle $ it follows that $i\not = j$ , which suggests that $w_{1}\in D_{i}(W_{w}^{c})$ for otherwise $i=j=0$ . It then means that there exists $v\in W_{w}^{c}$ such that $R_{1w}^{c}vw_{1}$ and $R_{2w}^{c}vw_{1}$ . By Proposition 4.42, $R_{2w}^{c}w_{1}w_{1}$ . W.l.o.g., assume $i<j$ . From $\mathcal {R}\langle w_{2},j \rangle \langle w_{1},i \rangle $ and $R_{2w}^{c}w_{1}w_{1}$ , we can also obtain $j<i$ , which entails a contradiction. So it can only be the case that $R_{2w}^{c}w_{2}w_{1}$ . Similarly, we have $R_{2w}^{c}w_{1}w_{2}$ . However from the definition of $\mathcal {R}$ and $\langle w_{1},i \rangle \not =\langle w_{2},j \rangle $ , it follows that $(i<j\land j/2\in \mathbb {Z})$ and $(j<i\land i/2\in \mathbb {Z})$ , which is a contradiction, too.

Next, consider the case that only one of the two edges is a new edge added when taking transitive closure. W.l.o.g., assume that $\neg \mathcal {R}\langle w_{1},i \rangle \langle w_{2},j \rangle $ and $\mathcal {R}\langle w_{2},j \rangle \langle w_{1},i \rangle $ . Then the edge from $\langle w_{1},i \rangle $ to $\langle w_{2},j \rangle $ is added in the transitive closure, i.e., there is an $\mathcal {R}$ -path (of a length greater than 2) from $\langle w_{1},i \rangle $ to $\langle w_{2},j \rangle $ in $\mathcal {F}$ . Now by Proposition 4.51, there must be some $\langle w_{3}, k \rangle $ such that $\mathcal {R}\langle w_{1},i \rangle \langle w_{3},k \rangle $ , $\mathcal {R}\langle w_{3},k \rangle \langle w_{2},j \rangle $ , and moreover $R_{1w}^{c}w_{1}w_{3}$ , $\neg R_{2w}^{c}w_{1}w_{3}$ , $R_{1w}^{c}w_{3}w_{2}$ , $R_{2w}^{c}w_{3}w_{2}$ and $R_{2w}^{c}w_{1}w_{2}$ . Since $\mathcal {R}\langle w_{2},j \rangle \langle w_{1},i \rangle $ , we have $R_{1w}^{c}w_{2}w_{1}$ . Now by $R_{1w}^{c}w_{3}w_{2}$ and $R_{1w}^{c}w_{2}w_{1}$ , we have $R_{1w}^{c}w_{3}w_{1}$ . From Proposition 4.43 and $R_{1w}^{c}w_{1}w_{3}$ , it holds that $R_{2w}^{c}w_{1}w_{3}\lor w_{1}\equiv w_{3}$ . Note that we already have $\neg R_{2w}^{c}w_{1}w_{3}$ , so $w_{1}\equiv w_{3}$ . Thus $\mathcal {R}\langle w_{1},i \rangle \langle w_{1},k \rangle $ and $\mathcal {R}\langle w_{1},k \rangle \langle w_{2},j \rangle $ . From $\neg \mathcal {R}\langle w_{1},i \rangle \langle w_{2},j \rangle $ and $\mathcal {R}\langle w_{1},k \rangle \langle w_{2},j \rangle $ , we know $i\not =k$ . Consequently, we have $w_{1}\in D_{i}(W^{c}_{w})$ , i.e., there exists $v\in W^{c}_{w}$ such that $R_{1w}^{c}vw_{1}$ and $R_{2w}^{c}vw_{1}$ . However, as $R_{1w}^{c}vw_{1}$ and $R_{2w}^{c}vw_{1}$ , by Proposition 4.42 it holds that $R_{2w}^{c}w_{1}w_{1}$ , which contradicts $\neg R_{2w}^{c}w_{1}w_{3}$ (i.e., $\neg R_{2w}^{c}w_{1}w_{1}$ ).

Finally, let us consider the case that $\neg \mathcal {R}\langle w_{1},i \rangle \langle w_{2},j \rangle $ and $\neg \mathcal {R}\langle w_{2},j \rangle \langle w_{1},i \rangle $ . Since the edges are added in the transitive closure, by Proposition 4.51 there are $w_{3},w_{4}\in W_{w}^{c}$ in the initial frame $\mathcal {F}_{gw}^{c}$ , and $k, h\in \mathbb {Z}$ , such that