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!
