Hi! Could anyone tell me how you prove the wfff (well-formed formula) (◊p V ◊q) → ◊(p V q) in the minimal modal propositional logic system calledNK? You can only use two rules (the Necessitation Rule (If A is a theorem of K, then so is □A) and the Modus Ponens inference rule (If P, then Q. - P. - Therefore, Q.)) and one axiom (Distribution Axiom: □(A→B) → (□A→□B)).

I've got this far:

1. (p V q) → (p V q) [pL]

2. □((p V q) → (p V q)) [1, N]

3. □ (p V q) → □(p V q) [2, K]

4. (□p V □q) → □(p V q) [3, K]

5. (¬◊¬p v ¬◊¬q) → ¬◊¬(p V q) [4, def □]

6. (◊p V ◊q) → ◊(p V q) [pL]

I thought this was the correct proof, but I could be wrong.

You can find more information on modal logic on the following links:

http://plato.stanford.edu/entries/logic-modal/

http://en.wikipedia.org/wiki/Modal_logic

Thanks in advance!