Is there a modal operator which distributes over the implication?

Question

Is there any notable modal operator $\Box$, so that if $P,Q$ are proposition

$$\left(\Box(P\implies Q)\right)\Leftrightarrow\left(\Box P\implies \Box Q\right)$$

Answer 1

The -> direction is the distribution axiom of K.

Sources: http://plato.stanford.edu/entries/logic-modal/#ModLog

Answer 2

Consider a two-world model: in the actual world (say) $P$ is true and $Q$ is false. In the only other possible world $P$ is false and $Q$ is true. Assume every world is accessible from every other world (so this is an S5 model)

(i) Since $P$ is true and $Q$ is false at the actual world, $P \to Q$ is false, so isn't necessarily true, i.e. $\Box(P \to Q)$ is false at the actual world. [Assuming a world is accessible from itself.]

(ii) Since $P$ is false at the other world, $P$ is not necessarily true, so $\Box P$ is false at the actual world, hence $(\Box P \to \Box Q)$ is true there.

So that's a model that shows that $(\Box P \to \Box Q)$ does not logically entail $\Box(P \to Q)$ in S5. So it won't follow in weaker-than-S5 modal logics either, including ones where the box doesn't mean "necessary".

Answer 3

Adding this axiom to the axioms for normal modal logic K based on classical propositional logic is equivalent (using propositional logic) to adding the normality axiom (as mentioned before) together with the two axioms $\Box Q \rightarrow \Box (\neg P \vee Q)$ and $\Box P \vee \Box (P \rightarrow Q)$. The first one follows from monotonicity of $\Box$, while the second one is the axiom $Alt_1$. This gives you the logic $KAlt_1$ of frames where every world sees at most one world (see e.g. Hughes & Cresswell, "A New Introduction to Modal Logic", 1996, p.142).