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

Question

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…

Answer 1

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)$$