I am trying to solve exercises from the book Modal Logic by Patrick Blackburn, Maarten de Rijke and Yde Venema. I am having a problem to solve one of the exercises in the section 1.6, it is the last part of exercise is 1.6.3 in page 37. Please help me.
Exercise : Give an $S5$ proof of $\diamond \square p\to \square p$
For the convenience I am here stating all the axioms of $S5$ system.
(PC axiom 1) $p\to (q\to p)$
(PC axiom 2) $(p\to (q\to r)) \to ((p\to q)\to (p\to r))$
(PC axiom 3) $(\lnot p\to \lnot q)\to (q\to p)$
(K axiom) $\square (p\to q) \to (\square p\to \square q)$
(Dual axioms) $\diamond p \to \lnot \square \lnot p$ , $\lnot \square \lnot p \to \diamond p$
(K4 axiom) $\diamond \diamond p\to \diamond p$
(S4 axiom) $p \to \diamond p$
(S5 axiom) $p\to \square \diamond p$
And the rules of inference are:
(MP) if $p$ and $p\to q$ both are true then $q$ is true
(N) if $p$ is true the $\square p $ is true
I know it is actually using these axioms efficiently but I can not make a good start and puzzled here. I am not finding a way to solve the problem.
I appologise for not showing a good effort from my end but I am completely stuck here.
Please help me to solve this problem. Thnx in advance.
Thanks for stating all those axioms! Here's a sketch.
The $K4$ scheme gives
$$\vdash\square p\to \square\square p.$$
By $N$ and the $K$ scheme it follows that
$$\vdash\lozenge\square p\to \lozenge\square\square p.$$
But this together with the instance
$$\vdash \lozenge \square\square p\to \square p$$
of the $S5$ scheme gives the desired
$$\vdash \lozenge \square p\to \square p.$$
Incidentally, one strategy for finding axiomatic proofs (besides being a machine) is to start by giving a semantic argument like that in Carl's comment above. This will give some sense of the shape of the proof, e.g., what axioms are needed.