In Cresswell and Hughes: "A new introduction to Modal Logic" they in question 2.4 ask to show that $L(M(\alpha))$ isn't a theorem of $K$ system (where L is the necessary operator and M the possible operator).

Here's what I thought, I can substitute $\alpha$ for p&~p

So I get:

  1. L(M(p&~p)) assumption ad absurdum.

  2. L(Mp & M~p) 1, K8+N+K+MP

  3. LM(p) & LM(~p) 2, K3.

Here's where I got stuck, and I am not sure how to deduce a contradiction.

Any hints or thoughts?

Thanks in advance.

  • 1
    I see that you are active on math.sx. Could you perhaps give us some context as to why you posted this question here instead of there? (It would seem a good fit for math.sx to me.)
    – DBK
    Nov 23 '12 at 21:13
  • 1
    I think you've spotted a useful trick with using p&~p as a test case, but C/H's proof system doesn't let you use proof by contradiction for its modal component. In fact, it doesn't let you make assumptions at all. Everything needs to be a formal inference from axiomatic starting points. Your best bet is to actually try to prove ~L(M(p&~p)) as a theorem; is it possible to show that L(~p) -> ~L(p), for example?.
    – Paul Ross
    Nov 23 '12 at 21:43
  • @DBK, I don't think there are experts in modal logic there, but I will try. I know that in CS Theory there's a stackexchange and they have modal logic tag. (though it has only two followers). Nov 24 '12 at 19:16
  • Why are you distributing your possibilitation operator? Can't you show that L(M(φ)) => M(φ) under $K$? As a rule of thumb, it's advisable to reduce the number of modal operators on a sentence first- M(p & ~p) should be simpler to prove. (I'm perplexed though- what rule or schema are you applying with K8 - and why N? I'm using Chellas's 'old' introduction to ML here, so maybe I'm missing out)
    – Ryder
    Nov 24 '12 at 23:04

There is a simple model theoretic proof. We build a model where the formula is false in for a possible world. This implies that the formula is not valid and hence not a theorem.

Consider a model M, where the set of possible worlds is {w1,w2}, and the accessibility relation R={(w1,w2)}. Then since there are no possible worlds accessible from w2, for any formula A, M(A) is false at w2. Therefore, L(M(A)) is false at w1; hence L(M(A)) is not valid. Given that K is complete, then L(M(A)) is not a theorem for any formula A.

In general one cannot prove using proof-theoretic techniques that a formula is not a theorem.

  • Let me see if I understand this. We can have a model where W={w1,w2}, and a relation R={(w1,w2)}. We can assume that in this model w1 and w2 don't satisfy p, i.e p is false in both of them. In this case Mp isn't a theorem in this model, cause if it were then either w1|= Mp or w2|=Mp , but in either case the other world should satisfy p which they don't. Then Mp isn't a theorem in this model, and thus in the same semantics approach also LMp isn't a theorem. Am I right? Nov 25 '12 at 11:13
  • There are no assumptions about the truth values of any atomic propositions. w2 |= ~Mp simply because there no worlds related to w2. The valuation function for M is w|= Mp iff there exists a world x such that wRx and x|=p. Thus in w2 every formula M(A) is false.
    – Guido
    Nov 25 '12 at 12:08
  • But if we have: w1Rw2, then w1|= Mp iff w2|= p (and vice versa by changing 1 with 2). So it depends on if w2 or w1 satisfy p or not. So if I assume that w1 and w2 don't satisfy p then I conclude that Mp isn't satisfied by either of them. Nov 25 '12 at 18:45
  • @MathematicalPhysicist R is not symmetric, it is just a binary relation. Here, we have |- A iff |= A. |= A iff for all models M, M |= A. M |= A iff for all worlds w in M, w |= A. Thus to show that A is not theorem, we have to find a model and a world where A is false. In the model I gave, for all formulas B, M(B) is false at w2 ( w2 |= ~M(B) ).
    – Guido
    Nov 25 '12 at 19:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.