Cfrgtkky

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.