Löb axiom implies positive introspection
= Löb axiom implies positive introspection
{c}
{title2=$\Box X\to\Box\Box X$}
The Löb axiom $\Box(\Box A\to A)\to\Box A$ over normal <modal logic> already implies $\Box X\to\Box\Box X$. Put $C=\Box X\wedge X$. Distribution gives $\Box C\to\Box X$, hence $X\to(\Box C\to C)$. Necessitation and distribution give $\Box X\to\Box(\Box C\to C)$; the Löb axiom gives $\Box C$, which implies $\Box\Box X$.