Modal logic K4 (source code)

= Modal logic K4
{c}
{title2=$\mathrm{K4}$}

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