# Distribution Axiom of Modal Logic

Is it possible to prove the distribution axiom of modal logic? I have proven all the conclusions of propositional modal logic using this axiom, the definitions of the four standard modal operators, and the postulate that some contingent proposition is true. I wanted to know if it was possible to prove this distribution proposition (also called Kripke property):

$$\square (p \rightarrow q) \rightarrow (\square p \rightarrow \square q)$$ It basically distributes the necessity operator over the components of every necessary conditional proposition. Most modal logic books accept this as an axiom in addition to others, but I want the fewest axioms possible as I have already reduced them to the distribution axiom, modal semantics and definitions, and (some contingent proposition is true). Is there any further reduction possible by proving the distribution axiom. And if so please provide a natural deduction proof of this distribution statement from previous principles in modal logic.

• I have looked everywhere and can find no proof of this distribution principle of modal logic – Eric Brown Jun 9 '15 at 9:05
• There's no proof of it simply because K it is taken as an (arguably) modal principle: if it is necessary that $p$ implies $q$, then if $p$ is necessary, $q$ is necessary as well. But if one judges axioms by their fruitfulness, K certainly well-justified: as you saw yourself proving some theorems by means of it. – Bruno Bentzen Jun 9 '15 at 10:43
• Looking from a semantic perspective, for this axiom to fail, Modus ponens would have to fail also wouldn't it? Since if $p \rightarrow q$ and $p$ hold at all accessible states, one would expect $q$ to hold at all accessible states too (by appealing to a principle like Modus ponens). – prime4567 Jun 9 '15 at 14:32
• @prime4567 Somewhat. The logically equivalent restatement is: $$\Box(\varphi\to\phi)\to(\Box\varphi\to \Box\phi) \;\iff\; (\Box(\varphi\to\phi)\wedge\Box\varphi)\to\Box\phi$$ – Graham Kemp Jun 9 '15 at 15:01

Are you referring to axiom K ? That is: $\quad \Box (\varphi\to \phi) \to (\Box \varphi\to\Box \phi)$
If the implication that $\varphi\to\phi$ is $\overbrace{\text{true in all accessible nodes}}^\text{necessary}$, then $\phi$ is true in all accessible nodes whenever $\varphi$ is true in all accessible nodes.