So I'm trying to prove that, in a language with two diamonds <1>,<2>, the formula p -> [2]<1> p is valid just in case for any x,y and R2(x,y) then R1(y,x). I have the "if" direction easily, that is to say, I've show that if the relations have this property then the formula is valid. But I'm stuck on the "only if". What I have so far is:

Suppose p -> [2]<1>p is valid and w,w' are in W such that R2(w,w'). Let p = Av~A so that w ||- p and therefore w ||- [2]<1>p so that w' ||- <1>p. So of course w' "accesses some world in which p is true" but how could you pin down that the world in question is w?

I wonder, are worlds distinguished by the sentences that are true in them? So could I form the sentence that is the conjunction of all true atomic sentences, or something like it, in or order to be able to infer at this point in the proof that the world which w' accesses wherein p is true, is the world w?

  • Maybe have a look at how the equivalent is proved when there is only one type of diamond. I think that such proof exists (the axiom p-> []<>p being equivalent to the symetry of the accesibility relation). It seems to me that the same problem arises. Jun 10, 2015 at 21:18

1 Answer 1


So I did it by contraposition which is not my favorite--I'd like to prove it directly but this will suffice.

Let w,w' in W such that R2(w,w') but not R1(w',w) and take the valuation V(p)={w}. In this case w ||- p but not w' ||- <1>p which implies not w ||- [2]<1>p and so w not ||- p -> [2]<1>p hence it's not valid.

You must log in to answer this question.

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