# Is this a contradiction in system K?

I'm trying to prove that M(p implies p) implies (Lq implies Mq) where M is possibility and L is necessity. So obviously p&~p is a contradiction but is L(p&~p) a contradiction? At first glance, it seems like it must be because this says that for any world w it is the case that for all w' such that wRw' it is the case that p&~p in world w', and so this would be a contradiction in world w'. And presumably it suffices to demonstrate just one world where there is a contradiction.... the problem is that in system K, I don't see why there is any need for any world to be related to any world. It seems my proof is fine, except in the degenerate case where for all w there does not exist w' such wRw'. But maybe the statement can be proved in this case seperately ? Otherwise, thoughts on my proof?

EDIT: I get the feeling my proof is correct, but I would like some confirmation. We can consider any arbitrary frame (W,R,V) (where W is the set of worlds, R is our relation, and V is the valuation function). Since we are proving a theorem we fix our frame and now consider two cases: Case (1): Consider a world w in W such that there exists m in W such that wRm; in this case use the proof below and L(p&~p) means that V(L(p&~p),w)=1 which implies that V(p&~p,m)=1 a clear contradiction. Case (2): Consider a world w in W such that there does not exist any world m such that wRm. In this case V(M(p implies p),w)=0 because there is no relation, M(*) will always be false... in this case the theorem is vacuously true.

Here's my proof:

1 Show M(p implies p) implies (Lq implies Mq)

2 M(p implies p). Assumption for Conditional Derivation

3 Show (Lq implies Mq)

`````` 4 Lq. Assumption for Conditional Derivation

5 Show Mq

6 ~Mq. Assumption for Indirect Derivation

7 L~q. Line (6) plus the fact that M is equivalent to ~L~ plus double negation.

8 Lq Repition of line 4

9 L(A & B) iff L(A) & L(B). a theorem of K

10 L(p & ~p) iff L(p) & L(~p). Line 9 with A set to p and B set to ~p.

11 L(q) & L(~p). Adjuction of lines 7 and 8

12 L(p & ~p) by line 11 and 10 with Modus Ponens
``````