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

1 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.

  • did you read my edit? I actually do use the assumption M(p → p) in my edit. You said "While it may seem that Lq entails Mq, there is one way that this can fail, namely if there are no Pos that are accessible to the given world" call that given world w. I don't disagree, in that case, V(M(p → p),w)=0 in which case V{[(M(p → p))→( Lq → Mq)],w}=1 nevertheless, right?
    – Clclstdnt
    Nov 7, 2017 at 15:57
  • 1
    Yes, that's fine. I mean that it doesn't show in your proof in steps 1 to 12. I think what your proof needs to show is that if there are no accessible PWs, then the antecedent M(p→p) is false, so the sentence is true simply by virtue of having a false antecedent, while if there are accessible PWs, then Lq→Mq is true and so the sentence is true by virtue of having a true consequent.
    – Bumble
    Nov 7, 2017 at 17:07
  • The style of proofs in modal logic feels very different than the style in "normal" PC logic. So is it normal to fix the world you are considering like I did above in my Case 1 and Case 2, and then do a proof?
    – Clclstdnt
    Nov 7, 2017 at 17:22
  • 'Normal' proofs are still possible in modal logic, and there are theorem provers that can work with modal logic. It is a bit weird in some ways. Just be grateful you are not using quantifiers: quantifiers mixed with modals is very weird.
    – Bumble
    Nov 7, 2017 at 18:05

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .