For an exercise in Modal Logic I have to solve the next problem, can someone please help?
Use generated submodels to show that the backward looking modality (that is, P of the basic temporal language) cannot be defined in terms of the forward looking operator $\diamond $.
I think I have to use that a formula $\phi$ can be true in the generated submodel but not in the original model. Probably I have to assume that it is possible to define the backward looking modality in terms of $\diamond$ and then search for a contradiction.
Thanks! :)
The exercise is from Modal logic by Patrick Blackburn et al. The approach is the same as in the Example 2.4, i.e. you assume, that the backward looking modality is definable in the basic modal language (that is using $\diamond$). Then, according to the Proposition 2.6, some formula $\varphi$, which might include the new modality, is true in some state of a model if and only if it is true in the same state of the generated submodel. Let use the model and the generated submodel from the p. 55 and the state $\bf0$. We can "look backwards" in the model (i.e. $\bf{-1}R\bf0$), but we cannot do so in the generated submodel (since there is no state $s$, such that $sR\bf{0}$), which is the contradiction.