Axiomatic proof in modal system B

Question

I am trying to prove the statement $\Box(P \rightarrow \Box P) \rightarrow (\Diamond P \rightarrow P)$ within B

I already checked that this statement is valid semantically in B. And by completeness there has to be an axiomatic proof in B using the Axioms K,T,B,mp,nec.

I also have the following derived rules as well

1. $\phi \rightarrow \Box \Diamond \phi$.

2. $\phi \rightarrow \Diamond \phi$

3. $\Box(\phi \rightarrow \psi) \rightarrow (\Diamond \phi \rightarrow \Diamond \phi)$

And of course trivial deductive moves from propositional logic of course and tautologies relating negation of $\Diamond$ and $\Box$ to each other.

I am just wondering if there is a simple proof within B for this system using the above axioms and derived rules, or if I am missing some derived rules that could make the proof easier?

I've tried proving the contrapositive and then simplifying using equivalences of negation and $\Diamond$ and $\Box$, but I couldn't eliminate all of the negations.

Answer 1

Here is the proof of (K $\Diamond$) gives in logic for philosophy by Sider \begin{align} 1.&~~(\phi\to\psi)\to(\lnot\psi\to\lnot\phi)\tag*{PL(contraposition)}\\ 2.&~~\square(\phi\to\psi)\to\square(\lnot\psi\to\lnot\phi)\tag*{1,NEC,K,MP}\\ 3.&~~\square(\lnot\psi\to\lnot\phi)\to(\square\lnot\psi\to\square\lnot\phi)\tag*{K}\\ 4.&~~\square(\phi\to\psi)\to(\square\lnot\psi\to\square\lnot\phi)\tag*{2,3,PL (syllogism)}\\ 5.&~~\square(\phi\to\psi)\to(\lnot\square\lnot\phi\to\lnot\square\lnot\psi)\tag*{4,PL (contraposition)} \end{align}

which shows $\square(\phi\to\psi)\to(\Diamond\phi\to\Diamond\psi)$, with this result, the statement in the question can be easily proved:

\begin{align} 1.&~~\square(P\to\square P)\to(\Diamond P\to\Diamond\square P)\tag*{K $\Diamond$}\\ 2.&~~\Diamond\square P\to P\tag*{B}\\ 3.&~~\square(P\to\square P)\to(\Diamond P\to P)\tag*{1,2, PL} \end{align}

Answer 2

In my answer here, I gave a proof of $(\varphi\land \lozenge\psi)\rightarrow \lozenge(\psi\land \lozenge \varphi)$ in system B.

If we take $\varphi = \lnot P$ and $\psi = P$, we get $(\lnot P\land \lozenge P)\rightarrow \lozenge(P\land \lozenge \lnot P)$. The contrapositive of this is $\square(\lnot P \lor \square P)\rightarrow (P\lor \lnot \lozenge P)$. And replacing disjunctions by implications, this is equivalent to $\square(P\rightarrow \square P)\rightarrow (\lozenge P\rightarrow P)$, which is what you wanted to prove.

Note that the linked proof also involves passing to the contrapositive and turning negated implications into conjunctions, and we had to reverse those steps to get the statement you wanted to prove. I'll leave it as an exercise for you to give a more direct proof. (Edit: Actually, it looks like Manx has done just that.)