Show $\vdash_{KL} \Box p\to \Box \Box p$? KL=K+Lob formula ($\Box (\Box p\to p)\to \Box p$). How to show $\vdash_{KL} \Box p\to \Box \Box p$? It is exercise 1.6.5 in Blackburn's Modal Logic.
 A: Oh, I got afflatus! Put the proof here to someone has same question.
To begin with, we show a lemma-$\vdash \Box (p\wedge q)\leftrightarrow (\Box p\wedge \Box q)$.
\begin{align*}
 &1.\vdash (p\wedge q)\to p& &&\text{tautology}\\
 &2.\vdash \Box ((p\wedge q)\to p)& &&\text{Gen: 1}\\
 &3.\vdash \Box ((p\wedge q)\to p)\to (\Box (p\wedge q)\to \Box p)& &&\text{K}\\
 &4.\vdash (\Box (p\wedge q)\to \Box p)& &&\text{MP: 2,3}\\
 &5.\vdash (p\wedge q)\to q& &&\text{tau.}\\
 &6.\vdash \Box ((p\wedge q)\to q)& &&\text{Gen: 5}\\
 &7.\vdash \Box ((p\wedge q)\to q)\to (\Box (p\wedge q)\to \Box q)& &&\text{K}\\
 &8.\vdash (\Box (p\wedge q)\to \Box q)& &&\text{MP: 6,7}\\
 &9.\vdash \Box (p\wedge q)\to (\Box p\wedge \Box q)& &&\text{4,8}\\
\end{align*}
Note example 1.40 in Blackburn's Modal Logic, we have $\vdash (\Box p\wedge \Box q)\to \Box (p\wedge q)$. Therefore $\vdash \Box (p\wedge q)\leftrightarrow (\Box p\wedge \Box q)$. Then we use the lemma to prove.
\begin{align*}
&1.p\to ((\Box p\wedge \Box \Box p)\to (p\wedge \Box p))& &&\text{tau.}\\
&2.\Box(p\to ((\Box p\wedge \Box \Box p)\to (p\wedge \Box p)))& &&\text{Gen: 1}\\
&3.\Box(p\to ((\Box p\wedge \Box \Box p)\to (p\wedge \Box p)))\to (\Box p\to \Box ((\Box p\wedge \Box \Box p)\to (p\wedge \Box p)))& &&\text{K}\\
&4.\Box p\to \Box ((\Box p\wedge \Box \Box p)\to (p\wedge \Box p))& &&\text{MP: 2,3}\\
&5.(\Box p\wedge \Box \Box p)\iff \Box (p\wedge \Box p)& &&\text{lemma}\\
&6.\Box p\to \Box (\Box (p\wedge \Box p)\to (p\wedge \Box p))& &&\text{4,5}\\
&7.\Box (\Box (p\wedge \Box p)\to (p\wedge \Box p))\to \Box (p\wedge \Box p)& &&\text{Lob}\\
&8.\Box (p\wedge \Box p)\iff (\Box p\wedge \Box \Box p)& &&\text{lemma}\\
&9.(\Box p\wedge \Box \Box p)\to \Box \Box p& &&\text{tau.}\\
&10.\Box p\to \Box \Box p& &&\text{HS: 6,7,8,9}
\end{align*}
A: The trick here is to substitute $p\land \square p$ for $p$ in Löb's axiom.
First note that for any $a$ and $b$, since $(a\land b)\rightarrow a$ is a theorem, by necessitation and K we have a theorem $$(*)_1\colon\square (a\land b)\rightarrow \square a.$$ Similarly, we have $$(*)_2\colon \square (a\land b)\rightarrow \square b.$$
Now we want to show $$(1)\colon \square p\rightarrow  \square(\square(p\land \square p)\rightarrow (p\land \square p)).$$ We have $$(2)\colon \square(\square(p\land \square p)\rightarrow (p\land \square p))\rightarrow \square(p\land \square p)$$ as an instance of Löb's axiom, and $$(3)\colon\square(p\land \square p)\rightarrow \square\square p$$ as an instance of $(*)_2$. Composing these implications gives $\square p\rightarrow \square\square p$, as desired.
So it remains to prove $(1)$. Assume $p$. Now assume $\square(p\land \square p)$. By $(*)_1$, we get $\square p$. So we get $p\land \square p$. Discharging our second assumption, we get $\square(p\land \square p)\rightarrow (p\land \square p)$. Discharging our first assumption, we get $p\rightarrow \square(p\land \square p)\rightarrow (p\land \square p)$. By necessitation and K, we get $(1)$.
