# Modal system K - prove ⊢ (□p ∨ □q) → □(p ∨ q)

I am trying to prove the following:

⊢ (□p ∨ □q) → □(p ∨ q)

However, I think that I am lacking the knowledge of a tautology in classical logic that would help me prove this.

I tried something, but it seems too contrived to work and I'm thinking there's an easier solution.

``````1.    p → (p ∨ q)            tautology
2.    □(p → (p ∨ q))         necessity axiom
3.    □p → □(p ∨ q)          distribution axiom *
4.    q → (p ∨ q)            tautology
5.    □(q → (p ∨ q))         necessity axiom
6.    □q → □(p ∨ q)          distribution axiom **
``````

Now, I wanted to use the following tautology from classical logic:

⊢ (A → C) → (B → C) → ((A ∨ B) → C)

Where I would substitute A=□p, B=□q, C=□(p ∨ q) which I think would get me the result I want. However, I am unable to get □p and □q alone.

Even more, if I'm to use this in my test, I'd need to prove the tautology via natural deduction first and then use it. Since this is the case, I thought that there had to be another, more easier way to do it.

Could someone help?

• you don't need to get ☐p or ☐q alone. You already have the desired results from 3 and 5 of your answer so you may conclude directly Jun 23 at 20:01
• Your proof is very nearly complete. Many systems of natural deduction contain the disjunction elimination rule: A ∨ B; A ⊢ C; B ⊢ C; therefore C. You just need to convert your lines 3 and 6 from conditional sentences into proofs, i.e. with 3, go from □p → □(p ∨ q) to □p ⊢ □(p ∨ q) using modus ponens. Jun 24 at 0:42
• @Bumble but wouldn't I need to have (□p ∨ □q) as a premise for disjunction elmination to work? Jun 24 at 0:52
• Yes. Just assume (□p ∨ □q) and then discharge your assumption at the end to introduce the conditional. Speaking quite generally, a good rule of thumb for proving conditional sentences is to assume the antecedent, derive the consequent and discharge the assumption using the rule of conditional proof. Jun 24 at 0:59