I have to find a formal Hilbert style proof for $\Box A \vee \Box B \rightarrow \Box(A\vee B)$ on modal logic, K. I can use all classical propositional tautologies, Modus Ponens and Distribution axiom. This far I have
- $A \rightarrow (A \vee B)$ Propositional Tautology.
- $B \rightarrow (A \vee B)$ Propositional Tautology.
- $\Box(A \rightarrow (A \vee B))$ Necessitation rule on 1.
- $\Box(A \rightarrow (A \vee B)) \rightarrow (\Box A \rightarrow \Box (A\vee B))$ Distribution Axiom on 3.
- $\Box A \rightarrow \Box (A\vee B)$ Modus Ponens on 3 and 4.
- $\Box(B \rightarrow (A \vee B))$ Necessitation rule on 2.
- $\Box(B \rightarrow (A \vee B)) \rightarrow (\Box B \rightarrow \Box (A\vee B))$ Distribution Axiom on 6.
- $\Box B \rightarrow \Box (A\vee B)$ Modus Ponens on 6 and 7.
9*.$(p \rightarrow q) \rightarrow ((s \rightarrow q) \rightarrow ((p\vee s) \rightarrow q)) $ Is a propositional tautology, expressed in propositional variables for clarification purposes. We will take: $p= \Box A$, $q = \Box(A\vee B)$, $s = \Box B$ in step 9.
- ($\Box A \rightarrow \Box (A\vee B)) \rightarrow ((\Box B \rightarrow \Box(A \vee B)) \rightarrow ((\Box A \vee \Box B)\rightarrow \Box (A \vee B)))$ Propositional Tautology.
- $((\Box B \rightarrow \Box(A \vee B)) \rightarrow ((\Box A \vee \Box B)\rightarrow \Box (A \vee B)))$ By Modus Ponens of 5 and 9.
- $\Box A \vee \Box B \rightarrow \Box (A \vee B))$ By Modus Ponens on 8 and 10.
Edit: I figured out how to solve it, as I have seen few examples of Hilbert calculus proofs with detail I finished it and will leave it as a future resource.