Hilbert style proof for $\Box A \vee \Box B \rightarrow \Box(A\vee B)$ in K.

318 Views Asked by At

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

  1. $A \rightarrow (A \vee B)$ Propositional Tautology.
  2. $B \rightarrow (A \vee B)$ Propositional Tautology.
  3. $\Box(A \rightarrow (A \vee B))$ Necessitation rule on 1.
  4. $\Box(A \rightarrow (A \vee B)) \rightarrow (\Box A \rightarrow \Box (A\vee B))$ Distribution Axiom on 3.
  5. $\Box A \rightarrow \Box (A\vee B)$ Modus Ponens on 3 and 4.
  6. $\Box(B \rightarrow (A \vee B))$ Necessitation rule on 2.
  7. $\Box(B \rightarrow (A \vee B)) \rightarrow (\Box B \rightarrow \Box (A\vee B))$ Distribution Axiom on 6.
  8. $\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.

  1. ($\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.
  2. $((\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.
  3. $\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.