 Modal logic K4

Modal logic K4 extends the normal modal distribution axiom and necessitation rule by positive introspection $\square A\to \square \square A$. Its Kripke semantics uses transitive accessibility relations. The fixed point $B=\square (\square X\to X)$ satisfies $\square (B\to \square X)\to (B\to \square X)$ in this logic.