Name of “inverse distribution” axiom?

Question

We may speak of a function distributing over another, e.g.,

$$ f(a,g(b,c)) = g(f(a,b),f(a,c)) \qquad a \cdot (b + c) = a \cdot b + a\cdot c$$

Some logical operators have similar distribution rules, such as:

$$ \left(P \land (Q \lor R) \right) \leftrightarrow ((P \land Q) \lor (P \land R))$$

In the logical case, we can can break the distribution relationship into the left and the right (or forward and backward) directions, i.e.,

\begin{eqnarray} \left(P \land (Q \lor R) \right) & \to & ((P \land Q) \lor (P \land R))\\ ((P \land Q) \lor (P \land R)) &\to & \left(P \land (Q \lor R) \right) \end{eqnarray}

In modal logic, the axiom K, also called distribution, states that the necessity modality, $\Box$, distributes over the material conditional:

$$ \Box(P \to Q) \to (\Box P \to \Box Q) \tag{K}$$

I am interested in the relationships between different truth-functional operators and the $\Box$ modality. In general, for a truth-functional operator $\otimes$ we can consider the two sentences:

\begin{eqnarray} \Box(P \otimes Q) &\to& (\Box P \otimes \Box Q) \tag{left$_\otimes$} \\ (\Box P \otimes \Box Q) &\to& \Box(P \otimes Q) \tag{right$_\otimes$} \end{eqnarray}

In normal modal logics, left$_\otimes$ holds for $\otimes \in \{\land,\to\}$ and right$_\otimes$ holds for $\otimes \in \{\land,\lor\}$.

When left$_\otimes$ holds for an operator $\otimes$, I am comfortable saying that $\Box$ distributes over $\otimes$, even if (as in the case of $\lor$) right$_\otimes$ does not hold. Is this a standard terminology? In the case of functions, $\to$ is replaced by equality, so each side is equal to the other, but with logical operators, we can have one side imply the other, but not vice versa. If left$_\otimes$ is distrbution for an operator, then what is right$_\otimes$ called? “Accumulation?” Is there a standard set of names for these relationships?

Other examples and references

The modal operator $\Box$ in modal logics with Kripke semantics is a univeral quantifier in disguise, so it's no surprise that this behavior appears in first-order quantifiers. As discussed in Distribution of Quantifiers over Conjunction and Disjunction, it's easy to see that

$$\forall x.(P(x) \lor Q(x)) \leftrightarrow (\forall x.P(x) \lor \forall x.Q(x)) $$

is not valid. That site concludes that “universal quantification does not distribute over disjunction.” However, the leftward direction of this is valid. We could say that “universal quantification accumulates over disjunction,” perhaps? This fact is also discussed in the question Distribution of Universal Quantifiers.

Answer 1

There are four kinds of possible distributivity between binary operators $\triangle$ and $\otimes$.

Left-distributivity of $\triangle$ over $\otimes$ is: $x \triangle (y \otimes z) = (x \triangle y) \otimes (x \triangle z)$

Right-distributivity of $\triangle$ over $\otimes$ is: $(x \otimes y) \triangle z = (x \triangle z) \otimes (y \triangle z)$

Left-distributivity of $\otimes$ over $\triangle$ is: $x \otimes (y \triangle z) = (x \otimes y) \triangle (x \otimes z)$

Right-distributivity of $\otimes$ over $\triangle$ is: $(x \triangle y) \otimes z = (x \otimes z) \triangle (y \otimes z)$

If the first two hold we say $\triangle$ distributes over $\otimes$; when the second two hold: $\otimes$ distributes over $\triangle$.

Finally, for every option above, as you noted, there are two, since we can be interested not only in $=$, but also in $\rightarrow$.

---

Now, you are interested not in binary operators (for which we use the definitions above), but in a combination of unary and binary operator. For this purpose, we can imagine that $\square P$ is actually $\square(P, c)$, where $c$ is something we don't care about.

Left-distributivity for $\square$-over-$\otimes$, and both left- and right-distributivity for $\otimes$-over-$\square$ are unusual properties, and can hardly be expected to hold in order to call the relationship distributive. So I'd say we can't speak of "distributivity over" at all, if we want our terminology for unary-binary combinations to directly follow from binary-binary definitions.

If you agree with the above, then there is a terminology issue even before noticing that $\rightarrow$ gives space for further fineness. Since we can't speak of "distribution over" at all [unless we want to talk about properties that do follow from binary-binary cases, but that are so weird that we probably wouldn't call them distribution properties in the first place], whenever we say "distributes over" we are bound to make compromises. I'd say it's ok to say "$\square$ distributes over $\rightarrow$" even if only axiom K holds, partly because it's a tradition, partly because in strong sense [above] we don't really want to say "distributes over", partly because in logic(s), lots of things work only one way.