# Thread: Modal logic: correct proof?

1. ## Modal logic: correct proof?

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 called NK? 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.

http://plato.stanford.edu/entries/logic-modal/
http://en.wikipedia.org/wiki/Modal_logic

2. I heard about the modal logic K, but I am not sure about NK -- what additional axioms it has.

I don't understand how line 4 was obtained. I guess, one has to prove □p \/ □q -> □(p \/ q). For this, one proves □p -> □(p \/ q) and □q -> □(p \/ q). This follows from p -> p \/ q, q -> p \/ q and the Nec rule and distributivity.

I also don't see how to get line 6 -- this is at least not a one-step transition.

3. Originally Posted by emakarov
I don't understand how line 4 was obtained. I guess, one has to prove □p \/ □q -> □(p \/ q). For this, one proves □p -> □(p \/ q) and □q -> □(p \/ q). This follows from p -> p \/ q, q -> p \/ q and the Nec rule and distributivity.
I also don't see how to get line 6 -- this is at least not a one-step transition.
Me neither. I was a kind of guess.

As I said, you have to use propositional logic, add the neccissitation (N) and inference rule Modus Ponens (MP) and finally add the Distribution Axiom.

In modal logic, neccesarily (the □-operator) is defined as ¬◊¬. So □P is equivalent to ¬◊¬P. ◊P is (as you might expected) defined exactly the other way around: ¬□¬P.

From those building blocks I have to figure out how to prove the beginning wff.

4. I don't have much time now to test this, but here's what I would try.

Maybe proving □(p /\ q) <-> □p /\ □q is easier. It is got from the axioms of conjunction:

p /\ q -> p
p /\ q -> q
p -> q -> p /\ q

Then one need to add □ and distribute them.

Having proved this thing for conjunction, insert negations everywhere so that □ turn to diamond and /\ to \/ via De Morgan.