# $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond\phi)$ in KB

I've been trying to prove $$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$$ in natural deduction where it's allowed to use $$\phi\to \square \diamond \phi$$ and/or $$\diamond\square\phi\to\phi$$ (that is, in $$KB)$$, but I failed. How can one prove this? I'm not including my work because it consists of dozens of pages and doesn't lead anywhere...

• You've listed the axiom B, but when you say "in natural deduction", I guess you're also including the rules of the modal logic K? – Alex Kruckman Mar 10 at 22:55
• @AlexKruckman Wikipedia says "K := no conditions", so I'm not sure what rules of K you mean. – user643175 Mar 10 at 23:03
• The necessitation rule and the distribution axiom. – Alex Kruckman Mar 10 at 23:04
• @AlexKruckman Yes, they are included. By "natural deduction" I meant the natural deduction system which includes box-subproofs and diamond-subproofs; and then those axioms can be proven. – user643175 Mar 10 at 23:06
• Ok. If you want to ask for a proof in a particular system, it's good practice to include a link to the precise rules of that system. Every logic has a wide variety of proof systems! – Alex Kruckman Mar 10 at 23:09

Here's a sketch of the idea, which I'll leave to you to translate into a formal proof in your system, if you care to.

Let's assume $$\phi$$ and $$\lozenge \psi$$. From B and modus ponens, we get $$\square\lozenge \phi$$, so we get $$(\square\lozenge\phi \land \lozenge \psi)$$

Now as an instance of the distribution axiom K, we have: $$\square (\lozenge \phi \rightarrow \lnot \psi) \rightarrow (\square \lozenge \phi \rightarrow \square \lnot \psi)$$

The contrapositive of this implication is: $$\lnot (\square\lozenge \phi \rightarrow \square \lnot \psi) \rightarrow \lozenge \lnot (\lozenge \phi \rightarrow \lnot \psi)$$

Turning $$\lnot (p\rightarrow q)$$ into $$p\land \lnot q$$ in two places, we get: $$(\square\lozenge \phi \land \lozenge \psi) \rightarrow \lozenge (\psi \land \lozenge \phi)$$

Finally, by modus ponens, we get $$\lozenge (\psi \land \lozenge \phi)$$

• Thanks! It seems I'd have never come up with the idea of considering $\square (\lozenge \phi \rightarrow \lnot \psi) \rightarrow (\square \lozenge \phi \rightarrow \square \lnot \psi)$. – user643175 Mar 10 at 23:41