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

Question

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?

Answer 1

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.