# Prove ◇(p ∨ q) → (◇p ∨ ◇q) and ◇(p ∧ q) → (◇p ∧ ◇q) in Modal Logic K

I would really appreciate a rundown of a proof of one of the formulas or both:

1) ◇(p ∨ q) → (◇p ∨ ◇q)

2) ◇(p ∧ q) → (◇p ∧ ◇q)

I'm allowed to use following proof procedures of modal logic K:

1) Tautologies of Propositional Logic PC

2) Axiom K: ◻(φ → ψ) → (◻φ → ◻ψ)

3) Modus ponens, rule of detachment: (p → q), p ⊢ q

4) Godel translation G: if φ then ◻φ

5) ◇φ = ¬◻¬φ

6) if φ → ψ and ψ → ϑ then φ → ϑ

7) if φ → ψ then ◻φ → ◻ψ

I managed to prove (◇p ∨ ◇q) → ◇(p ∨ q) but I have problems with these two formulas.

EDIT: What I've come up with so far (there are several steps missing in the middle still):

1. (¬p ∧ ¬q) → ¬p (tautology of PC)

2. (¬p ∧ ¬q) → ¬q (tautology of PC)

3. ◻(¬p ∧ ¬q) → ◻¬p (if φ → ψ then ◻φ → ◻ψ)

4. ◻(¬p ∧ ¬q) → ◻¬q (if φ → ψ then ◻φ → ◻ψ)

5. (◻(¬p ∧ ¬q) → ◻¬p) → [(◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q))] (tautology of PC)

6. (◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q)) (modus ponens (3, 5))

7. ◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q) (modus ponens (4, 6))

8. missing steps

9. (◻¬p ∧ ◻¬q) → ◻¬(p ∧ q) (THIS IS WHAT I WANT)

10. [(◻¬p ∧ ◻¬q) → ◻¬(p ∧ q)] → [¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q)] (tautology of PC: (p → q) → (¬q → ¬p))

11. ¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q) (modus ponens (9, 10))

12. ◇(p ∧ q) → (◇p ∧ ◇q)

• To be honest, I don't know how to start. In (◇p ∨ ◇q) → ◇(p ∨ q) example I started with ¬(p ∨ q) → ¬p and ¬(p ∨ q) → ¬q. 1) ◻¬(p ∨ q) → ◻¬p 2) ◻¬(p ∨ q) → ◻¬q 3) (◻¬(p ∨ q) → ◻¬p) → [(◻¬(p ∨ q) → ◻¬q) → (◻¬(p ∨ q) → ◻¬(p ∧ q))] 4) ... modus ponens x 2 5) (◻¬(p ∨ q) → (◻¬p ∧ ◻¬q)) → ((¬◻¬p ∨ ¬◻¬q) → ¬◻¬(p ∨ q)) 6) (¬◻¬p ∨ ¬◻¬q) → ¬◻¬(p ∨ q) However, I really don't know how to prove ◇(p ∨ q) → (◇p ∨ ◇q) – Pvniep Niepiniep Oct 16 '16 at 9:10
• Here's a hint. Assume ◇(p ∨ q), then assume ¬(◇p ∨ ◇q) and derive a contradiction. If you get a contradiction, that means that if ◇(p ∨ q) then (◇p ∨ ◇q). – Eliran Oct 16 '16 at 9:41
• @EliranH Thank you for your reply, but I'm afraid that it won't help. I'm supposed to give a direct proof based on basic tautologies like ¬(p ∨ q) → ¬p. I might, however, understand your hint wrongly. If that's the case, could you please elaborate on how to apply your reasoning. – Pvniep Niepiniep Oct 16 '16 at 10:01
• @Keelan I edited my original post and added what I have come up with so far, there are several steps missing in the middle still. Could you please review my proof and help me with missing steps? – Pvniep Niepiniep Oct 16 '16 at 18:45