Axiomatic proof in modal system $⊢_{K5} □(□p → p)$

Question

I’m having a hard time proving $⊢_{K5} □(□p → p)$. Proving validity in Euclidean frames.in this from axiom 5 is valid $◇p → □◇p$

I’m able to derive

$□p → □(□p → p)$

I,m also able to derive from Axiom 5

$◇□p → □p$

And

$◇□p → □□p$

But I’m not able to make the final derivation. Help would be greatly appreciated

Answer 1

You already have an important lemma, namely that

$□p → □(□p → p)$.

Another lemma you’ll need is

$\Box (\Diamond \neg p \to (\Box p \to p))$.

Using axiom K, the second lemma yields

$\Box \Diamond \neg p \to \Box (\Box p \to p))$.

Using the inter-definability of $\Box$ and $\Diamond$ and propositional logic, our lemmas give us

$\neg \Box (\Box p \to p) \to (\neg \Box p \land \Diamond \Box p)$

which by axiom 5 and propositional logic yields the result.