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

Question

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)

Answer 1

Let's see if I can give you a hint for a strategy, rather than a complete proof. Let's take your second proposition as the candidate for proof:

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

1. Start by proving ◇(p ∧ q) → ◇p and also ◇(p ∧ q) → ◇q. It is easy to prove the ◻ counterparts of these: (p ∧ q) → p is a tautology of PC, so you can derive ◻((p ∧ q) → p) and hence by the K-axiom ◻(p ∧ q) → ◻p. The proof of the ◇ counterparts involves extra steps, because you need to use the equivalence of ◇φ and ¬◻¬φ and prove the contrapositive. In general, it is always the case that if φ → ψ then ◇φ → ◇ψ, though this isn't needed as a separate axiom within K, because it can be derived from the others.

2. Now that we have ◇p and ◇q we need to get to ◇p ∧ ◇q. If we were allowed to help ourselves to the rules of PC, this would be easy, because this is simply the introduction rule for ∧. But your problem specifies that we may only use the tautologies of PC, not its rules. A useful tip is that a rule of PC corresponds to a conditional tautology. So in general, if in PC we can prove ψ from φ then the material conditional φ → ψ is a tautology. So the introduction rule for ∧ implies the following is a tautology: φ → (ψ → (φ ∧ ψ)) and hence ◇p → (◇q → (◇p ∧ ◇q)).

3. You should now be able to show that ◇(p ∧ q) implies each of ◇p and ◇q and hence by transitivity that it implies ◇p ∧ ◇q.