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):
(¬p ∧ ¬q) → ¬p (tautology of PC)
(¬p ∧ ¬q) → ¬q (tautology of PC)
◻(¬p ∧ ¬q) → ◻¬p (if φ → ψ then ◻φ → ◻ψ)
◻(¬p ∧ ¬q) → ◻¬q (if φ → ψ then ◻φ → ◻ψ)
(◻(¬p ∧ ¬q) → ◻¬p) → [(◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q))] (tautology of PC)
(◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q)) (modus ponens (3, 5))
◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q) (modus ponens (4, 6))
missing steps
(◻¬p ∧ ◻¬q) → ◻¬(p ∧ q) (THIS IS WHAT I WANT)
[(◻¬p ∧ ◻¬q) → ◻¬(p ∧ q)] → [¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q)] (tautology of PC: (p → q) → (¬q → ¬p))
¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q) (modus ponens (9, 10))
◇(p ∧ q) → (◇p ∧ ◇q)