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.
 A: Are you referring to axiom K ? That is: $\quad \Box (\varphi\to \phi) \to (\Box \varphi\to\Box \phi)$
This is axiomatic because it's a reasonably self-evident proposition given the definitions of necessity and implication in the Kripke semantics, but it isn't derived from anything else.
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.
A: I have found two proofs of the distribution proposition □(p→q)→(□p→□q). One is through proof by contradiction and the other is through direct proof using the absorption equipollence (logical equivalence)(p→q)::[p→(p●q)]  and [□(p→q)→(□p→□q)]::{[□(p→q)●□p]→□q}. The proof through contradiction uses the proof of (□p→p)from modal semantics and the definitions of the necessity □ and possibility (diamond) modal operators alone. So there is no circular reasoning. Accordingly, the proof by contradiction is as follows. Suppose that the distribution proposition is false. Therefore, by definition of the conditional proposition, □(p→q) is true but (□p→□q) is false. Therefore, again by definition of the conditional proposition, □p is true but □q is false. By [□(p→q)→(p→q)] from (□p→p) and the truth of □(p→q) using modus ponens, (p→q) is true. Similarly, using (□p→p) and the truth of □p through modus ponens, p is true. Consequently, by modus ponens again on (p→q) and using the truth of p, q is true. Therefore, the truth of q has been logically proven. Consequently, q is logically necessary, because of the Necessitation Rule. Therefore, □q is true and as seen previously □q is false. This is the contradiction. Therefore, through proof by contradiction, the proof of the distribution proposition □(p→q)→(□p→□q) is complete. The direct proof is as follows. It presupposes the proof of absorption (p→q)::[p→(p●q)] in propositional logic and of [□(p→q)→(□p→□q)]::{[□(p→q)●□p]→□q} (name this the lemma to this proof) through proof by contradiction and biconditional proof. Now suppose that (□(p→q)●□p) is true. Therefore, by definition of a conjunctive proposition, both □(p→q) and □p are true. Consequently, by the absorption equivalence □(p→q)::□[p→(p●q)]. Therefore, by formal implication, □[p→(p●q)] is true. Next, using □[p→(p●q)]→[p→(p●q)](true by uniform substitution of p→(p●q) into (□p→p), which is proven without use of the distribution proposition as stated previously) and the truth of □[p→(p●q)] through modus ponens, [p→(p●q)] is true. Consequently, using (□p→p) and the truth of □p through modus ponens, p is true. Therefore, [p→(p●q)] and p are true so that by modus ponens again,(p●q) is true. By definition of a conjunctive proposition, q is true. Therefore,the truth of q has been logically proven. Consequently, q is logically necessary, because of the Necessitation Rule. Therefore, □q is true. By direct proof, {[□(p→q)●□p]→□q}has been proven to be true. Consequently, by the lemma {[□(p→q)●□p]→□q}: [□(p→q)→(□p→□q)], the proof of the distribution proposition [□(p→q)→(□p→□q)] is complete. Please provide any corrections or advice if needed, but I am now certain that the distribution proposition is not an axiom but a proven conclusion (theorem) of modal logic according to these two proofs. The proof by contradiction is the most simple and elegant and the one that I will use in the future.If you have any questions on this topic, then feel free to send them my way!
