Admissibility of Löb's rule in basic modal logic K

While I was preparing a talk on the admissible rules of modal logic, I found the following fact in Wikipedia (see https://en.wikipedia.org/wiki/Admissible_rule#Examples).

It says that Löb's rule $$(\square p \to p)/p$$ is admissible in minimal modal logic K (а rule $$\phi/\psi$$ is called admissible in logic $$L$$, if for all substitution $$\sigma$$, such that $$\vdash_L\sigma(\phi)$$, also $$\vdash_L\sigma(\psi)$$).

This is a really interesting result, since in logic $$K4$$, for instance, it is no longer true (in $$K4$$ we can deduce a substitution instance of $$\square p \to p$$ for Löb's axiom $$\square(\square p \to p) \to \square p$$).

• Let in $\square p \to p$ a variable $p= \square(\square q \to q) \to \square q$. It is a well-known that the obtained formula is deducible in $K4$. Feb 23 at 15:45
Suppose $$\varphi$$ is a sentence such that $$\square\varphi\to \varphi$$ is a theorem of K. We would like to show that $$\varphi$$ is a theorem of K. Suppose not. Then there is a Kripke frame $$M$$ and a world $$w\in M$$ such that $$\varphi$$ is false at $$w$$. If the modal depth of $$\varphi$$ is $$d$$, then we can replace $$(M,w)$$ by a tree $$T$$ of height at most $$d$$ rooted at $$r$$ such that $$(M,w)$$ and $$(T,r)$$ are $$d$$-bisimilar, and hence $$\varphi$$ is false at $$r$$ in $$T$$.
Now since $$\square\varphi\to \varphi$$ is a theorem of $$K$$, $$\lnot \varphi\to \lozenge\lnot\varphi$$ is also a theorem, so there exists a child of $$r$$ in $$T$$ at which $$\varphi$$ is false. Repeating at most $$d$$ times, we arrive at a leaf of $$T$$ at which $$\varphi$$ is false. But now there are no worlds accessible from this leaf, so $$\square\varphi\to \varphi$$ is false here, which is a contradiction.