5

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.

4
  • 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
    Commented Nov 23, 2012 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
    Commented Nov 23, 2012 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). Commented Nov 24, 2012 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
    Commented Nov 24, 2012 at 23:04

1 Answer 1

3

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.

4
  • 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? Commented Nov 25, 2012 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
    Commented Nov 25, 2012 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. Commented Nov 25, 2012 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
    Commented Nov 25, 2012 at 19:27

You must log in to answer this question.

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