# Showing $\vdash \phi\to \square \diamond \phi$

I'm trying to prove the converse of what was shown here.

Namely, I'm trying to prove B-axioms of modal logic ($$\vdash \phi\to \square \diamond \phi$$ or $$\vdash\diamond\square\phi\to\phi$$, whatever is easier) in K if $$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$$ is given, and one is allowed to use any propositional tautology and standard inference rules.

I suppose I need to apply the distribution axiom in a clever way. Originally I was been trying to prove what I need without it (the distribution axiom); it took quite a few pages, but I don't think I made any progress. But after seeing the answer in the question cited, I believe I have to use that axiom (however, again, I'm not sure which sentences to apply it to). Any help is appreciated.

• I don't know why this is considered off-topic. I've edited the question to include more details, but I don't think this made it any clearer. And I definitely don't think it's reasonable to type pages of my attempts to prove this. Mar 11, 2019 at 3:46
• @AlexKruckman Thank you, I understood your proof. Again, I don't think I would come up with such a proof by myself. Or, I would, but only if I knew which two formulas should be contradictory. But there's no way to know this in advance, I guess... Mar 11, 2019 at 4:23
• Well, I came up with this proof, and the one for your previous question, just by "messing around" with the assumptions. And I'm definitely not an expert in modal logic! So there's hope: I think there's an intuition for formal proof strategies that you can build up by practice and port into unfamiliar situations. Mar 11, 2019 at 4:42

Suppose for contradiction that $$\varphi\land \lozenge\square\lnot\varphi$$. Then by our assumption, $$\lozenge(\square\lnot\varphi\land \lozenge\varphi)$$, equivalently $$\lozenge\lnot(\square\lnot\varphi\rightarrow\square\lnot\varphi)$$, equivalently $$\lnot\square(\square\lnot\varphi\rightarrow\square\lnot\varphi)$$.
But we have $$\square\lnot\varphi\rightarrow\square\lnot\varphi$$, so by necessitation $$\square(\square\lnot\varphi\rightarrow\square\lnot\varphi)$$, contradiction.