How do I solve exercise 2.2.4 Blackburn/de Rijke/Venema’s “Modal Logic”

Question

Here’s a transcript of the original exercise. (There‘s even a hint given by the authors in the textbook as you can see. But precisely this hint confuses me).

2.2.4 Consider the binary until operator $U$. In a model $\mathfrak{M} = (W,R,V)$ its truth definition reads:

$$ \begin{align} &\mathfrak{M},t \Vdash U(\phi, \psi) &\text{iff} & &\text{there is a $v$ such that $Rtv$ and $v \Vdash \phi$, and} \\ & & & &\text{for all $u$ such that $Rtu$ and $Ruv$: $u \Vdash \psi$.} \end{align} $$

Prove that $U$ is not definable in the basic modal language. Hint: think about the following two models, but with arrows added to make sure the relations are transitive:

I’m unsure how to prove this. I would probably attempt something like this:

In order to show that the operator $U$ is not definable you’d need to show that there’s a bisimulation between these two models (which is easy) and then you’d need to argue that only in one of them $U(\phi, \psi)$ holds (Which I don’t see. Doesn’t it hold in both models?). Then it follows that ‘$U$’ is not definable, because bisimilar models are invariant i.e. they make exactly the same transitions possible and couldn’t be distinguished by someone who operates on them.

So my main issue is seeing how these models are bisimilar yet only in one of them $U$ is the case.

Answer 1

Welcome to mse!

You have exactly the right idea, there's a bisimulation between these two models where we relate

• the $s_i$ worlds with $s'$
• the $t_i$ worlds with $t'$
• $u$ with $u'$
• the $v_i$ worlds with $v'$

It seems like you're comfortable with this, so I won't belabor the point.

Now, I claim that $s_0 \Vdash U(q,p)$ while $s' \not \Vdash U(q,p)$. As you've pointed out, this means that $U(q,p)$ is not definable in the basic modal language.

Now that you know what the correct worlds/formulas are, you might want to try to check this yourself. If you get stuck, I'll leave a solution below the fold:

To show $s_0 \Vdash U(q,p)$ we must find a $q$-world that $s_0$ sees, so that every world along the way is a $p$ world. Then $v_1$ works, since it's a $q$-world and the only world between $s_0$ and $v_1$ is $u$ (a $p$-world).

However, note $s' \not \Vdash U(q,p)$. Indeed, $v'$ is the only $q$-world it sees, so it's our only choice. But unfortunately $t'$ lies between $s'$, and $v'$, and $t' \not \Vdash p$. So $s' \not \Vdash U(q,p)$.

---

I hope this helps ^_^

Answer 2

Your proof idea is basically correct. There is a point $w$ from the left model $M_l$, some point $w'$ from the right model $M_r$, a bisimulation $R$ between $M_l$ and $M_r$ and formulas $\varphi, \psi$ such that $wRw'$, $M_l, w \models U(\varphi, \psi)$, but $M_r, w' \not \models U(\varphi, \psi)$.

Here is one way to proof this. It is easy to see that there is a bisimulation $R$ between $M_l$ and $M_r$ with $s_1Rs'$. Then we have that $s_1 R v_0, M_l, v_0 \models q$ and $M_l, u \models p$. Since $u$ is the only point lying between $s_1$ and $v_0$, it follows that $M_l, s_1 \models U(q,p)$.

On the other hand, $M_r, s' \not \models U(q,p)$. This is because $s'R v'$, $M_r, v' \models q, s'Rt'$ and $M_r, t' \not \models p$