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$).

Could you please help me to prove this fact. Thank you!

  • $\begingroup$ What’s the substitution instance in K4? $\endgroup$
    – PW_246
    Feb 23 at 15:27
  • $\begingroup$ 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$. $\endgroup$
    – lnv619
    Feb 23 at 15:45

1 Answer 1


The key is that the modal logic K is complete for the class of well-founded frames (even for the class of finite trees!). And on the class of well-founded frames, Löb's rule is valid.

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.

  • $\begingroup$ Thank you very much for your answer! Frankly speaking, I have found this solution by myself, but I thought that it is a little bit complicated (using a completeness for K w.r.t well-founded trees). Anyway, I am really happy that I am not alone on this thoughts :) $\endgroup$
    – lnv619
    Feb 24 at 12:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .