It is a well-known result that the canonical models for some temporal logics, e.g, $K_t4.3$ and $K_tQ$, contain proper clusters (equivalent class of points seeing each other). As a result, we need to use model transformation to prove some completeness results (such as $K4.3$ is complete over the class of strict linear order). I'm wondering how to show that these canonical models contain proper clusters. The question is similar to Excercise 4.5.4 of Modal Logic by Blackburn et al.
My preliminary guess is to find a point $w$ and construct a consistent set $\Gamma$ using formulas in $w$. Then I can extend $\Gamma$ to a MCS $v$ and show that $w$ sees $v$ and $v$ also sees $w$. But two question remains:
- The starting point $w$ should not be arbitrarily selected, because the model also contains irreflexive and reflexive points.
- What conditions should be used to construct $\Gamma$.