Is this a contradiction in system K?

Question

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

Answer 1

The sentence you are trying to prove is provable in system K, but your proof is not valid. L(p & ¬p) is not a contradiction. Lp & ¬Lp is a contradiction. System K is sufficiently weak that Lq → Mq is not a theorem. To understand this, it is perhaps better to think in terms of Kripke semantics. Lq says that q is true in every PW that is accessible from the given world, while Mq says that q is true in at least one such PW. While it might seem that Lq entails Mq, there is one way that this can fail, namely if there are no PWs that are accessible to the given world. In that case, Lq is trivially true for any q, while Mq is false. This is similar to the feature of ordinary quantifier logic under which it can be true that all unicorns are white, but false that there is at least one white unicorn. The weak nature of system K manifests itself in that there are no constraints on the accessibility relation between PWs. In particular, the relation is not serial and not reflexive, so there is no guarantee that any PWs are accessible.

But the sentence you are trying to prove has an antecedent M(p → p). This does assert the existence of at least one PW that is accessible to the given world. So given this, Lq → Mq follows. Your proof does not make use of M(p → p) anywhere - there is no reference to line 2. Lines 4 through 12 attempt to prove Lq → Mq unconditionally, which cannot be done.