# When does $(\square P \land \square Q) \to \square (P \land Q)$ hold?

If all axioms of classical propositional calculus hold and we work in modal logic that is at least K (ie. extremely weak), it is trivial to show $$\square(P \land Q) \to (\square P \land \square Q)$$. What other modality axioms, if any, have to be added for $$(\square P \land \square Q) \to \square (P \land Q)$$ to hold?

You don't need any other axiom, $$(\square P \land \square Q) \to \square (P \land Q)$$ is derivable in the system $$\mathbf{K}$$, i.e. in the propositional calculus (with modus ponens and closure under substitution) augmented with the necessitation rule (i.e. if $$A$$ is derivable then $$\square A$$ is derivable) and the distribution axiom (i.e. $$\square (P \to Q) \to (\square P \to \square Q)$$).

A formal proof in Hilbert system for $$\mathbf{K}$$ is the following:

1. $$P \to (Q \to (P \land Q)) \qquad$$ (axiom for conjunction in propositional calculus)
2. $$\square (P \to (Q \to (P \land Q))) \qquad$$ (necessitation rule applied to 1.)
3. $$\square (P \to (Q \to (P \land Q))) \to (\square P \to \square (Q \to (P \land Q))) \qquad$$ (distribution axiom)
4. $$\square P \to \square (Q \to (P \land Q)) \qquad$$ (modus ponens of 3. and 2.)
5. $$\square (Q \to (P \land Q)) \to (\square Q \to \square (P \land Q)) \qquad$$ (distribution axiom)
6. $$(\square P \to \square(Q \to (P \land Q)) ) \to \big( ( \square(Q \to (P \land Q)) \to (\square Q \to \square(P \land Q) )) \to ((\square P \land \square Q) \to \square(P \land Q) \big) \qquad (*)$$

7. $$( \square(Q \to (P \land Q)) \to (\square Q \to \square(P \land Q) )) \to ((\square P \land \square Q) \to \square(P \land Q) \qquad$$ (modus ponens of 6. and 4.)

8. $$(\square P \land \square Q) \to \square(P \land Q) \qquad$$ (modus ponens of 7. and 5.)

where the formula in ($$*$$) is derivable because it is an instance of the tautology in propositional $$(p \to q) \to \big( (q \to (r \to s)) \to ((p \land r) \to s)\big)$$ obtained through the substitution $$\begin{equation}\begin{cases} p \mapsto \square P \\ q \mapsto \square (Q \to (P \land Q)) \\ r \mapsto \square Q \\ s \mapsto \square (P \land Q) \end{cases}\end{equation}$$

Remind that, by the completeness theorem, any tautology in propositional calculus can be derived in a formal proof system such the Hilbert system.

For a reference, you can see "A New Introduction to Modal Logic" by Hughes and Cresswell, p. 27.