2. Bisimulation Between Verbrugge and Veltman Models

The alphabet of interpretability logic consists of countably many propositional variables and symbols $\bot$ , $\to$ and $\rhd$ . Formulas are given by

\begin{equation*}\varphi ::=p\,|\,\bot \,|\,\varphi _1\to \varphi _2\,|\,\varphi _1\rhd \varphi _2,\end{equation*}

where $p$ ranges over the set of propositional variables. We use the usual abbreviations $\top :=\neg \bot$ , $\neg \varphi :=\varphi \to \bot$ , $\varphi _1\vee \varphi _2:=\neg \varphi _1\to \varphi _2$ , $\varphi _1\wedge \varphi _2:=\neg (\neg \varphi _1\vee \neg \varphi _2)$ , $\varphi _1\leftrightarrow \varphi _2:=(\varphi _1\to \varphi _2)\wedge (\varphi _2\to \varphi _1)$ , $\Box \varphi :=\neg \varphi \rhd \bot$ , $\Diamond \varphi :=\neg \Box \neg \varphi$ .

A Veltman model is a tuple $(W,R,\{S_w:w\in W\},\Vdash )$ such that:

• • $W\neq \emptyset$ is a set called the domain, whose elements are called worlds

• • $R\subseteq W\times W$ is a transitive and converse well-founded relation called the accessibility relation

• • $S_w\subseteq R[w]\times R[w]$ , where $R[w]=\{u\in W:wRu\}$ , is a reflexive and transitive relation such that $wRuRv$ always implies $uS_wv$ , for each $w\in W$

• • $\Vdash$ is a relation between worlds and formulas such that for all $w\in W$ we have $w\not \Vdash \bot$ , $w\Vdash \varphi _1\to \varphi _2$ if and only if $w\not \Vdash \varphi _1$ or $w\Vdash \varphi _2$ , and $w\Vdash \varphi _1\rhd \varphi _2$ if and only of for all $u\in W$ such that $wRu$ and $u\Vdash \varphi _1$ there is $v\in W$ such that $uS_w v$ and $v\Vdash \varphi _2$ .

A Verbrugge model is a tuple $(W,R,\{S_w:w\in W\},\Vdash )$ , where $W$ and $R$ are as in the definition of Veltman models, while $S_w\subseteq R[w]\times (\mathscr{P}(R[w])\setminus \{\emptyset \})$ such that:

• • if $wRu$ , then $uS_w\{u\}$ (quasi-reflexivity)

• • if $uS_wV$ and $vS_wZ_v$ for all $v\in V$ , then $uS_w\bigcup _{v\in V}Z_v$ (quasi-transitivity)

• • if $wRuRv$ , then $uS_w\{v\}$

• • if $uS_wV$ and $V\subseteq Z\subseteq R[w]$ , then $uS_wZ$ (monotonicity),

while $\Vdash$ is defined similarly as in the definition of Veltman model, except the following: $w\Vdash \varphi _1\rhd \varphi _2$ if and only if for all $u$ such that $wRu$ and $u\Vdash \varphi _1$ there is $V$ such that $uS_wV$ and for all $v\in V$ we have $v\Vdash \varphi _2$ (we write $V\Vdash \varphi _2$ ).

When we need to emphasize that $w\Vdash \varphi$ is observed in the context of a structure $\mathfrak{M}$ , we will write $\mathfrak{M},w\Vdash \varphi$ .

As aforementioned, there are other variants of Verbrugge models in the literature, which differ from the above one only in the definition of quasi-transitivity and in some cases in omitting monotonicity. In this paper, we work only with the above definition since it is predominant in the literature (cf. the recent overview Joosten et al. (Reference Joosten, Mas Rovira, Mikec, Vuković and Bezhanishvili2024), which includes a discussion on other possibilities).

Bisimulation is the basic equivalence between modal models. It has three defining conditions: atomic equivalence between related worlds (at), the condition describing how the first model is simulated in the second one (forth), and the condition describing how the second model is simulated in the first one (back). When we work with the same kind of structures, (forth) and (back) are mutually symmetric. But now we will define the notion of bisimulation between different kinds of structures, which will therefore lack this symmetry. In fact, the direction from Verbrugge model to Veltman model (forth) will be much more complex than the opposite one.

Consider the following example of thus defined bisimulation. The example is illustrated in Figure 1.

Figure 1.

Illustration of Example1 – a bisimulation between Verbrugge model $\mathfrak{M}$ and Veltman model $\mathfrak{M}'$ .

The following proposition shows that the necessary requirement on any notion of bisimulation is satisfied: bisimilar worlds are modally equivalent.

3. Hennessy–Milner Theorem

As aforementioned, the first requirement of any notion of bisimulation is that it implies modal equivalence. That requirement shows that the definition is not too weak, that is, the structural relation between two models is strong enough to ensure that modal formulas cannot distinguish them. But on the other hand, some proposed relation between models can be too strong. For example, isomorphism of course implies modal equivalence, but it is obviously unnecessarily strong, that is, much weaker structural relations can imply modal equivalence. In other words, one would like to have a converse of the previous proposition, to see that the defined notion of bisimulation is exactly enough strong. Unfortunately, it is well known that the direct converse never holds (a counterexample can easily be constructed from some of the known counterexamples for basic modal logic). But, there are some approximations, notably Hennessy-Milner-like theorems, which say that the converse holds in case of image-finite models. If a Hennessy–Milner analog holds for some proposed notion, then it is a good sign that the notion is just about as strong as bisimulation should be.

Now we show that such an analog holds for bisimulations of Definition1.

The reader may be surprised to see that, in the definition of bisimulations between Verbrugge models and Veltman models, the condition (forth) demands the existence of a set of worlds $U'$ instead of just the existence of at least one world as usual. But without this, the notion of bisimulation would not be useful. To see this, note that a seemingly more natural (forth) would demand: if $wZw'$ and $wRu$ , then there is $u'$ such that $w'R'u'$ , $uZu'$ and for all $v'$ such that $u'S^{\prime}_{w'}v'$ there is $V$ such that $uS_wV$ and $vZv'$ for all $v\in V$ . It is easily checked that this does imply modal equivalence, but nevertheless it is too restrictive, since it has a consequence that all worlds in $V$ are mutually modally equivalent, which practically collapses Verbrugge semantics to Veltman semantics.

The following example illustrates why we need (forth) to be as complex as it is and also provides an idea how to proceed with the main goal of the paper: find a bisimilar Veltman model for a given Verbrugge model.

4. Obtaining a Veltman Model Bisimilar to a Given Verbrugge Model

It is straightforward to obtain a Verbrugge model from a given Veltman model $\mathfrak{M}=(W,R,\{S_w:w\in W\},\Vdash )$ : we use the same $W$ and $R$ , and define $uS^{\prime}_wV$ if and only if $uS_wv$ for some $v\in V$ . It is very easy to see that $Z=\{(w,w):w\in W\}$ is a bisimulation between the thus obtained Verbrugge model and $\mathfrak{M}$ .

Although it is very simple, our running example already illustrates that the opposite direction is much more involved. The basic idea is that each world from a given Verbrugge model will have multiple copies in the associated Veltman model, to make it possible for $S_w$ -connections with sets of worlds to be simulated by connections with worlds which are representatives of these sets.

So, let $\mathfrak{M}=(W,R,\{S_w:w\in W\},\Vdash )$ be a Verbrugge model. We will define a Veltman model associated with $\mathfrak{M}$ , which we will denote by $Vel(\mathfrak{M})=(W',R',\{S^{\prime}_{w'}:w'\in W'\},\Vdash )$ .

First, we introduce some notation and terminology.

4.3 A Veltman model associated with a given Verbrugge model

Now we are ready to define $Vel(\mathfrak{M})$ and to prove that it is indeed a Veltman model.

Definition 5. Let $\mathfrak{M}=(W,R,\{S_w:w\in W\},\Vdash )$ be a Verbrugge model. By $Vel(\mathfrak{M})=(W',R',\{S^{\prime}_{w'}:w'\in W'\},\Vdash )$ , we denote a structure associated with $\mathfrak{M}$ , defined as follows:

• • $W'$ consists of all ordered pairs $(w,f)$ , where $w\in W$ , and $f$ is a function which maps each $x\in W$ such that $xRw$ to a function $f_x$ , which is a well-defined choice of representatives of $\overline {S_x}$ -paths starting with $w$

• • $(w,f)R'(u,g)$ if and only if $wRu$ and for all $x$ such that $xRw$ , for each $\overline {S_x}$ -path $\overline {\{u\}},\overline {V_1},\dots, \overline {V_k}$ (observe that then $\overline {\{w\}},\overline {\{u\}},\overline {V_1},\dots, \overline {V_k}$ is an $\overline {S_x}$ -path starting with $w$ ), we have

  \begin{equation*}f_x(\overline {\{w\}},\overline {\{u\}},\overline {V_1},\dots, \overline {V_k})_{i+1}=g_x(\overline {\{u\}},\overline {V_1},\dots, \overline {V_k})_i,\quad i=1,\dots, k\end{equation*}

• • $(u,g)S^{\prime}_{(w,f)}(v,h)$ if and only if $(w,f)R'(u,g)$ , $(w,f)R'(v,h)$ and there is an $\overline {S_w}$ -path $\overline {\{u\}},\overline {V_1},\dots, \overline {V_k}$ such that $v=g_w(\overline {\{u\}},\overline {V_1},\dots, \overline {V_k})_k$ , for some $k\geqslant 0$ , and for any continuation, that is, for any $\overline {S_w}$ -path $\overline {\{u\}},\overline {V_1},\dots, \overline {V_k},\overline {V_{k+1}},\dots, \overline {V_{k+l}}$ , we have

  \begin{equation*}g_w(\overline {\{u\}},\overline {V_1},\dots, \overline {V_{k+l}})_{k+i}=h_w(\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'})_i,\quad i=1,\dots, l\end{equation*}
  where $\overline {S_w}$ -path $\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'}$ is induced by $v$

• • $Vel(\mathfrak{M}),(w,f)\Vdash p$ if and only if $\mathfrak{M},w\Vdash p$ , for all $(w,f)\in W'$ , for each propositional variable $p$

Proposition 6. Let $\mathfrak{M}$ be a Verbrugge model. Then $Vel(\mathfrak{M})$ is a Veltman model.

Proof. Obviously $R'$ is converse well-founded. To show that it is also transitive, let $(w,f)R'(u,g)R'(v,h)$ . Then $wRuRv$ and therefore $wRv$ . Furthermore, for an arbitrary $x$ such that $xRw$ and an arbitrary $\overline {S_x}$ -path $\overline {\{v\}},\overline {V_1},\dots, \overline {V_k}$ , we have

\begin{equation*}h_x(\overline {\{v\}},\overline {V_1},\dots, \overline {V_k})_i=g_x(\overline {\{u\}},\overline {\{v\}},\overline {V_1},\dots, \overline {V_k})_{i+1}\end{equation*}

\begin{equation*}=f_x(\overline {\{w\}},\overline {\{u\}},\overline {\{v\}},\overline {V_1},\dots, \overline {V_k})_{i+2}=f_x(\overline {\{w\}},\overline {\{v\}},\overline {V_1},\dots, \overline {V_k})_{i+1},\quad i=1,\dots, k\end{equation*}

(the last equality holds since $f_x$ is a well-defined choice of representatives).

Now we verify the desired properties of the relation $S_{(w,f)}'$ for an arbitrary $(w,f)$ . The reflexivity trivially follows from the convention that $\overline {\{u\}}$ is considered to be an $\overline {S_w}$ -path of length 0. To prove the transitivity, assume $(u,g)S_{(w,f)}'(v,h)S_{(w,f)}'(z,s)$ . Since $(u,g)S_{(w,f)}'(v,h)$ , there is an $\overline {S_w}$ -path $\overline {\{u\}},\overline {V_1},\dots, \overline {V_k}$ such that $v=v_k=g_w(\overline {\{u\}},\overline {V_1},\dots, \overline {V_k})_k$ and other properties from the definition of the relation $S_{(w,f)}'$ hold. Also, since $(v,h)S_{(w,f)}'(z,s)$ , there is an $\overline {S_w}$ -path $\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'}$ such that $z=z_l=h_w(\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'})_l$ , with other properties from the definition of $S_{(w,f)}'$ .

Put $V_{k+j}=(V_k\setminus \{v\})\cup V_j'$ and $\overline {V_{k+j}}=\{\{x\}:x\in V_k\setminus \{v\}\}\cup \overline {V_j'}$ , $j=1,\dots, l$ . Since $vS_wV_1'$ and $xS_w\{x\}$ for all $x\in V_k\setminus \{v\}$ , we have $\overline {V_k}\,\overline {S_w}\,\overline {V_{k+1}}$ . Similarly, since $\overline {V_j'}\,\overline {S_w}\,\overline {V_{j+1}'}$ for $j=1,\dots, l$ , we have that $\overline {\{u\}},\overline {V_1},\dots, \overline {V_{k+l}}$ is an $\overline {S_w}$ -path. Then $(u,g)S_{(w,f)}'(v,h)$ implies $g_w(\overline {\{u\}},\overline {V_1},\dots, \overline {V_{k+l}})_{k+l}=h_w(\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'})_l=z$ .

To check the remaining condition needed to conclude $(u,g)S_{(w,f)}'(z,s)$ , take any finite sequence $\overline {Z_1},\dots, \overline {Z_m}$ such that $\overline {\{u\}},\overline {V_1},\dots, \overline {V_{k+l}},\overline {Z_1},\dots, \overline {Z_m}$ is an $\overline {S_w}$ -path. Consider the $\overline {S_w}$ -path $\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'},\overline {Z_1'},\dots, \overline {Z_m'}$ induced by $v$ and the $\overline {S_w}$ -path $\overline {\{z\}},\overline {Z_1''},\dots, \overline {Z_m''}$ induced by $z$ . Then $(u,g)S_{(w,f)}'(v,h)S_{(w,f)}'(z,s)$ implies $g_w(\overline {\{u\}},\overline {V_1},\dots, \overline {V_{k+l}},\overline {Z_1},\dots, \overline {Z_m})_{k+l+j}=h_w(\overline {\{v\}},\overline {V_1'},\dots, \overline {V_l'},\overline {Z_1'},\dots, \overline {Z_m'})_{l+j}=s_w(\overline {\{z\}},\overline {Z_1''},\dots, \overline {Z_m''})_j$ , for all $j=1,\dots, m$ .

Finally, assume $(w,f)R'(u,g)R'(v,h)$ . We want to show $(u,g)S_{(w,f)}'(v,h)$ . First, we have $wRuRv$ , so $uS_w\{v\}$ , that is, $\overline {\{u\}},\overline {\{v\}}$ is an $\overline {S_w}$ -path and obviously it must be $g_w(\overline {\{u\}},\overline {\{v\}})_1=v$ . Note that for any continuation $\overline {\{ u\}},\overline {\{ v\}}, \overline {V}_2,\ldots, \overline {V_{l+1}}$ , the $\overline {S_w}$ -path induced by $v$ is actually $\overline {\{ v\}}, \overline {V}_2,\ldots, \overline {V_{l+1}}$ . Furthermore, since $(u,g)R'(v,h)$ , by the definition of the relation $R'$ applied to the path $\overline {\{ v\}}, \overline {V}_2,\ldots, \overline {V_{l+1}}$ , we have $g_w(\overline {\{u\}},\overline {\{v\}},\overline {V_2},\dots, \overline {V_{l+1}})_{i+1}=h_w(\overline {\{v\}},\overline {V_2},\dots, \overline {V_{l+1}})_i$ , $i=1,\dots, l$ , which is exactly what we need to conclude, namely, $(u,g)S_{(w,f)}'(v,h)$ .

5. Bisimulations Between Verbrugge and Veltman Models and w-Bisimulations Between Verbrugge Models

Alternatively, we can generalize conditions in the definition of bisimulation between a Verbrugge model and a Veltman model to develop an analogous notion of bisimulation between Verbrugge models, and then establish a connection between a Verbrugge model and a Veltman model by composing a simple transformation from the Veltman model to a Verbrugge model, described at the beginning of Section 4, and a bisimulation between two Verbrugge models. Indeed, an analogous notion of bisimulation between Verbrugge models is of independent interest and is thoroughly studied in Horvat et al. (Reference Horvat, Perkov and Vuković2023), where it is termed w-bisimulation, in order to make it clearly distinct to other notions of bisimulation between Verbrugge models studied in the literature (cf. Vuković Reference Vuković2000,Reference Vuković2005; Vrgoč and Vuković Reference Vrgoč and Vuković2010). In Horvat et al. (Reference Horvat, Perkov and Vuković2023) detailed arguments are given why w-bisimulation can be considered to be the proper notion of bisimulation between Verbrugge models.

The approach of the previous sections has an advantage that the already complex (forth) condition has an additional quantifier in case of two Verbrugge models, and the (back) condition is symmetric to (forth) when observed between two Verbrugge models, while in the present approach it is much simpler.

Nevertheless, in this section, we will briefly overview the notion of w-bisimulation and establish this connection with bisimulation between Verbrugge and Veltman models. We will make use of this connection in the next section, where we transfer results on finite approximations of w-bisimulations from Horvat et al. (Reference Horvat, Perkov and Vuković2023) to bisimulations between Verbrugge and Veltman models developed in this paper.

It is easy to see that w-bisimilarity implies modal equivalence. We refer the reader to Horvat et al. (Reference Horvat, Perkov and Vuković2023) for other properties of w-bisimulations and their finite approximations.

Now, for a given Veltman model $\mathfrak{M}$ , let $Ver(\mathfrak{M})$ denote the Verbrugge model obtained from $\mathfrak{M}$ by using the same domain and accessibility relation, and by putting $uS^{\prime}_wV$ if and only if $uS_wv$ for some $v\in V$ .

So now, alternatively, one can omit defining bisimulation between Verbrugge and Veltman models and state the main result accordingly: $Z$ is a w-bisimulation between $\mathfrak{M}$ and $Ver(Vel(\mathfrak{M}))$ .

6. Finite Bisimulations

In this section, we show that finite approximations of bisimulations, so-called $n$ -bisimulations, where $n$ is a natural number, can be defined, with desirable properties, analogous to those holding for other notions of bisimulations in modal logic: $n$ -bisimilarity implies $n$ -modal equivalence, that is, the equivalence w.r.t. formulas of modal depth at most $n$ , and furthermore, the converse in the case of finite alphabet also holds. Together with the Hennessy–Milner analog, we proved in Section 3, these results round up arguments in favor of the definition of bisimulation between Verbrugge and Veltman models presented in this paper.

To prove these results, we will use analogous results from Horvat et al. (Reference Horvat, Perkov and Vuković2023) and the link established in the previous section.

The following result can be proved similarly as Proposition 9, just using $Z_i$ and $Z_{i-1}$ instead of $Z$ , as appropriate.

In fact, similarly as in the proof of Proposition 9, the same sequence of relations can be used as both $n$ -bisimulation and $n$ -w-bisimulation.

7. Further Work

The main purpose of this paper was to show how we can transform a Verbrugge model into a bisimilar Veltman model. Important further line of research, closely related to this purpose, is to explore how this transformation behaves with respect to particular classes of Verbrugge models and Veltman models, with additional constraints related to various principles of interpretability, which are used as additional axioms of many systems of interpretability logic in the literature. For example, if a given Verbrugge model $\mathfrak{M}$ is an ILM-model, that is, belongs to the characteristic class of Verbrugge models related to so-called Montagna’s principle, does $Vel(\mathfrak{M})$ belong to the corresponding characteristic class of Veltman models? An analogous question may be addressed system by system, or more generally, if possible, conditions may be provided under which such a preservation works. Or if it does not work, can we modify the construction of $Vel(\mathfrak{M})$ for a particular principle or set of principles to make it work? Certainly, there is no general positive answer since obviously for systems complete w.r.t. Verbrugge semantics but incomplete w.r.t. Veltman semantics, a transformation from a Verbrugge model to a modally equivalent Veltman model does not exist (cf. Mikec and Vuković Reference Mikec and Vuković2020 for the case of the system ILP $_0$ ).