Show $\vdash_{KL} \Box p\to \Box \Box p$?

Question

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.

Answer 1

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*}

Answer 2

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