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.

  • 3
    $\begingroup$ 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. $\endgroup$
    – user557
    Mar 11, 2019 at 3:46
  • $\begingroup$ @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... $\endgroup$
    – user557
    Mar 11, 2019 at 4:23
  • $\begingroup$ 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. $\endgroup$ Mar 11, 2019 at 4:42

1 Answer 1


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.

It's interesting that I had to use distribution to prove your axiom from B, and conversely I had to use necessitation to prove B from your axiom. Probably there would be a good explanation for this if I understood modal logic better...


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .