Neighbourhood Contingency Bisimulation

Abstract

We introduce a notion of bisimulation for contingency logic interpreted on neighbourhood structures, characterise this logic as bisimulation-invariant fragment of modal logic and of first-order logic, and compare it with existing notions in the literature.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

A proposition is non-contingent if it is necessarily true or necessarily false, and otherwise it contingent. The notion of (non-)contingency goes back to Aristotle [1]. The modal logic of contingency goes back to Montgomery and Routley [14]. They captured non-contingency by an operator $\varDelta$ such that $\varDelta \varphi$ means that formula $\varphi$ is non-contingent (and where $\nabla \varphi$ means that $\varphi$ is contingent). In an epistemic modal logic, ‘$\varphi$ is non-contingent’ means that you know whether $\varphi$, and ‘$\varphi$ is contingent’ means that you are ignorant about $\varphi$ [8, 10, 18]. Contingency is definable with necessity: $\varDelta \varphi$ is definable as $\Box \varphi \vee \Box \lnot \varphi$. But necessity cannot always be defined with non-contingency. The definability of $\Box$ with $\varDelta$ has been explored in various studies [7, 14, 16]. In [7] the almost-definability schema $\nabla \psi \rightarrow (\Box \varphi \leftrightarrow (\varDelta \varphi \wedge \varDelta (\psi \rightarrow \varphi )))$ is proposed — as long as there is a contingent proposition $\psi$, $\Box$ is definable with $\varDelta$; which inspired a matching notion of contingency bisimulation: back and forth only apply when non-bisimilar accessible worlds exist.

Schemas such as $\varDelta (\varphi \wedge \psi ) \rightarrow (\varDelta \varphi \wedge \varDelta \psi )$ are invalid for the non-contingency operator. The operator $\varDelta$ is therefore not monotone, and the logic of contingency is not a normal modal logic. Non-normal logics are standardly interpreted on neighbourhood models [2, 13, 17]. Fan and Van Ditmarsch proposed in [6] to interpret the contingency operator on neighbourhood models. They left as an open question what a suitable notion of contingency bisimulation would be over neighbourhood models. We answer this question here.

We introduce a notion of neighbourhood $\varDelta$ -bisimilarity, inspired by the semantics of the $\varDelta$-modality and [9], where different notions of structural invariance among neighbourhood models were studied. By way of augmented neighbourhood models and their correspondence to Kripke models we can provide a detailed comparison to the bisimulations of [7]. We show that the two notions differ at the level of relations, but the ensuing bisimilarity notions coincide. Furthermore, we investigate the notions of $\varDelta$-morphisms and $\varDelta$-quotients and prove some analogues of results from [9]. These are instrumental in proving our two characterisation theorems (similar to [7, Theorems 4.4 and 4.5]): neighbourhood contingency logic is the $\varDelta$-bisimulation invariant fragment of classical modal logic, and of first-order logic.

Section 2 provides preliminaries. Section 3 recalls contingency logic over Kripke models and introduces different perspectives on relational contingency bisimulation. Section 4 introduces neighbourhood contingency bisimulation and studies its properties, and it is followed by the characterisation results in Sect. 5. The concluding Sect. 6 reflects on the relevance of our work and indicates future directions. Due to space limitations, some proofs have been omitted. They will be included in the extended version.

2 Coherence

We assume that the reader is familiar with the standard notions of sets, functions and relations. The following is merely to recall notation and to introduce the crucial notion of coherence. Given $U\subseteq X$, we denote by $U^c$ the complement of U in X. The disjoint union of two sets $X_1$ and $X_2$ is denoted by $X_1+X_2$ and the inclusion maps by $\iota _i :X_i \rightarrow X_1 + X_2$, $i=1,2$. Given a function $f :X \rightarrow Y$, the f-image of $U \subseteq X$ is $f[U] =\{f(x) \in Y \mid x \in U\}$, and the inverse f-image of $V \subseteq Y$ is $f^{-1}[V] = \{x \in X \mid f(x) \in V \}$. The graph of f is the relation $Gr (f) = \{(x,f(x)) \subseteq X \times Y \mid x \in X\}$. The kernel of f is the relation $\ker (f) = \{(x,y) \in X \times X \mid f(x) = f(y) \}$. Let $R \subseteq X\times Y$ be a relation. The R-image of $U \subseteq X$ is the set $R[U] = \{y \in Y \mid \exists x \in U: (x,y) \in R \}$, and the inverse R-image of $V \subseteq Y$ is $R^{-1}[V] = \{x \in X \mid \exists y \in V: (x,y) \in R \}$.

Given a relation $R \subseteq X\times Y$, the converse of R is written $R^{-1} \subseteq Y \times X$, the composition of R and $S \subseteq Y \times Z$ is $R; S \subseteq X \times Z$. For the reflexive, symmetric, and transitive closure we employ, respectively, $R^r$, $R^s$, and $R^+$ such that the equivalence closure can be defined as $R^e=((R^r)^s)^+$. If R is an equivalence relation, we often write $[x]_R$ (or simply [x]) instead of R(x).

Definition 1

( R -coherent pairs). Let $R \subseteq X\times Y$ be a relation, $U\subseteq X$ and $V\subseteq Y$. The pair (U, V) is R-coherent if $R[U]\subseteq V$ and $R^{-1}[V]\subseteq U$, or equivalently, for all $(x,y) \in R$, $x \in U$ iff $y \in V$. Given a relation $R \subseteq X \times X$, we say that $U \subseteq X$ is R-closed if (U, U) is R-coherent.

Note that if R is reflexive and $(U,U')$ is R-coherent, then $U=U'$.

3 Contingency Logic

In this section we introduce basic modal logic and contingency logic on Kripke models, and contingency bisimulation following [7, 8]. We also compare that to a novel notion of relational contingency bisimulation in terms of coherence.

Definition 2 (Languages)

Let $\mathsf {AtProp}$ be a set of atomic propositions. The languages $\mathcal {L}_{\Box }$ and $\mathcal {L}_{\varDelta }$ are generated by the following grammars:

$\begin{array}{llcl} \qquad \qquad &{} \mathcal {L}_{\Box }\ni \varphi &{}\quad {:}{:}= \quad &{} \;p \in \mathsf {AtProp}\;|\; \lnot \varphi \;|\; \varphi \wedge \varphi \;|\; \Box \varphi \\ &{} \mathcal {L}_{\varDelta }\ni \varphi &{}\quad {:}{:}= \quad &{} \;p \in \mathsf {AtProp}\;|\; \lnot \varphi \;|\; \varphi \wedge \varphi \;|\; \varDelta \varphi \end{array}$

The other Boolean connectives $\bot , \top$, $\vee$ and $\leftrightarrow$ are defined in the usual way.

The formula $\Box \varphi$ should be read as “$\varphi$ is necessarily true”, and the formula $\varDelta \varphi$ as “$\varphi$ is non-contingent”. The language $\mathcal {L}_{\varDelta }$ can be viewed as a fragment of $\mathcal {L}_{\Box }$ via an inductively defined translation $(-)^t: \mathcal {L}_{\varDelta }\rightarrow \mathcal {L}_{\Box }$ with only non-trivial clause $(\varDelta \varphi )^t = \Box \varphi ^t \vee \Box \lnot \varphi ^t$.

Definition 3 (Kripke models)

A (Kripke) frame is a pair $F = (S,R)$ where $S$ is a set (of states), and $R \subseteq S\times S$ is an accessibility relation. A Kripke model is a triple $M = (S,R,V)$ where $(S,R)$ is a frame and where $V:\mathsf {AtProp}\rightarrow \mathcal {P}(S)$ is a valuation. Given , a pair (M, s) is a pointed model.

Definition 4

Let $M = (S,R,V)$ be a Kripke model, and $s \in S$. The interpretation of formulas from $\mathcal {L}_{\Box }$ and $\mathcal {L}_{\varDelta }$ is defined inductively in the usual manner:

where $p\in \mathsf {AtProp}$. We say that (M, s) and $(M',{s'})$ are modally $\mathcal {L}_{\varDelta }$-equivalent (notation: $(M,s) \equiv _{\varDelta }(M',{s'})$) if for all $\varphi \in \mathcal {L}_{\varDelta }$, $M, s \, \models \, \varphi$ iff $M',{s'} \, \models \, \varphi$.

For all Kripke models M, states s in M, and all $\varphi \in \mathcal {L}_{\varDelta }$, $M,s \, \models \, \varphi$ iff $M,s \, \models \, \varphi ^t$.

We assume the reader is familiar with standard relational bisimulations (for $\Box$). In [7], Fan, Wang and Van Ditmarsch defined a weaker notion (for $\varDelta$) which we refer to as o- $\varDelta$ -bisimulation for “original $\varDelta$-bisimulation”.

Definition 5

(o- $\varDelta$ -bisimulation [7]). Let $M=(S, R, V)$ be a Kripke model. A relation $Z \subseteq S \times S$ is an o- $\varDelta$ -bisimulation on M, if whenever $(s,s')\in Z$:

$\mathbf {(Atoms)}$ s and $s'$ satisfy the same propositional variables;

$\mathbf {(}\varDelta \mathbf {-Zig)}$ for all $t\in R(s)$, if there are $t_1, t_2 \in R(s)$ such that $(t_1, t_2)\notin Z$, then there is a $t' \in R(s')$ such that $(t,t')\in Z$;

$\mathbf {(}\varDelta \mathbf {-Zag)}$ for all $t'\in R(s')$, if there are $t'_1, t'_2 \in R(s')$ such that $(t'_1, t'_2)\notin Z$, then there is a $t \in R(s)$ such that $(t,t')\in Z$.

We write $(M,s) {\,\approx _{\!\varDelta }^{\mathsf {on}}} (M, s')$, if there is an o-$\varDelta$-bisimulation on M that contains $(s,s')$. Two pointed models (M, s) and $(M',s')$ are o- $\varDelta$ -bisimilar, written $(M,s) {\,\approx _{\!\varDelta }} (M',{s'})$, if $(M+M',\iota _1(s)) {\,\approx _{\!\varDelta }^{\mathsf {on}}} (M+M',\iota _2(s'))$, i.e., there is an o-$\varDelta$-bisimulation on the disjoint union of M and $M'$ linking (the injection images of) s and $s'$.

Note that $(M,s) \,\approx _{\!\varDelta }(M',s')$ is not witnessed by a relation $Z \subseteq S \times S'$ since, by definition, o-$\varDelta$-bisimulation relations always live on a single model.

We introduced the notation $\,\approx _{\!\varDelta }^{\mathsf {on}}$, since, a priori, it is not clear whether $(M,s) \,\approx _{\!\varDelta }^{\mathsf {on}}(M,s')$ iff $(M,s) \,\approx _{\!\varDelta }(M,s')$. At the end of this section (Proposition 4), we will see that, in fact, this is true, and hence we could dispense with the notation $\,\approx _{\!\varDelta }^{\mathsf {on}}$, but for now we keep writing $\,\approx _{\!\varDelta }^{\mathsf {on}}$ for clarity.

Given a model M, we will also view $\,\approx _{\!\varDelta }^{\mathsf {on}}$ as the relation on the state space of M that contains all pairs $(s,s')$ such that $(M,s) \,\approx _{\!\varDelta }^{\mathsf {on}}(M,s')$. In order to compare o-$\varDelta$-bisimilarity with our later notion (in Definition 6), we need the following result.

Proposition 1

For all Kripke models M, the relation $\,\approx _{\!\varDelta }^{\mathsf {on}}$ on M is an equivalence relation, and itself an o-$\varDelta$-bisimulation on M.

Proposition 1 follows from the stronger result that o-$\varDelta$-bisimilarity is an equivalence relation over the class of all pointed Kripke models [4, 5]. This is quite non-trivial to prove, since o-$\varDelta$-bisimulations are not closed under composition (Example 1). Our proof relies on a number of closure properties. We must omit details due to space limitations.

Lemma 1

The set of o-$\varDelta$-bisimulation relations on a Kripke model M is closed under taking unions, converse, and transitive symmetric closure.

It is now easy to prove Proposition 1 using the closure properties of Lemma 1.

Proof of Proposition 1. By definition, the relation $\,\approx _{\!\varDelta }^{\mathsf {on}}$ on M is the union of all o-$\varDelta$-bisimulations on M, and hence the largest one. Reflexivity of $\,\approx _{\!\varDelta }^{\mathsf {on}}$ follows since the identity relation is an (o-$\varDelta$-)bisimulation. Symmetry follows from closure under converse. For transitivity, we use that the composition of two bisimulations is contained in the transitive symmetric closure of their union, which is again a bisimulation.

On (relational) $\Box$-bisimilarity and o-$\varDelta$-bisimilarity it is known that $\Box$-bisimilarity implies o-$\varDelta$-bisimilarity, but not vice versa [7, Proposition 3.4]; o-$\varDelta$-bisimilarity implies $\mathcal {L}_{\varDelta }$-equivalence [7, Proposition 3.5], whereas the converse only holds over saturated Kripke models [7, Proposition 3.9]; An $\mathcal {L}_{\Box }$-formula is equivalent to an $\mathcal {L}_{\varDelta }$-formula iff it is invariant under o-$\varDelta$-bisimulation [7, Theorem 4.4]. A first-order formula is equivalent to an $\mathcal {L}_{\varDelta }$-formula iff it is invariant under o-$\varDelta$-bisimulation [7, Theorem 4.5]. o-$\varDelta$-bisimilarity is an o-$\varDelta$-bisimulation [7, Proposition 3.13].

The notion of contingency bisimulation for neighbourhood models using coherent sets, introduced later in Definition 9, has a natural analogue for Kripke models. The definition is derived from the semantics of the $\varDelta$-modality.

Definition 6

(rel- $\varDelta$ -bisimulation). Let $M=(S, R, V)$ and $M'=(S', R', V')$ be Kripke models. A relation $Z \subseteq S \times S'$ is a rel- $\varDelta$ -bisimulation (for relational $\varDelta$ -bisimulation) between M and $M'$, if whenever $(s,s')\in Z$:

$\mathbf {(Atoms)}$ s and $s'$ satisfy the same propositional variables;

$\mathbf {(Coherence)}$ for all Z-coherent pairs $(U, U')$:

$$ (R(s)\subseteq U\; or\;R(s)\subseteq U^{c}) \quad \text {iff} \quad (R'(s')\subseteq U'\;or\;R'(s')\subseteq U'^{c}) $$

We write $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M',{s'})$, if there is a rel-$\varDelta$-bisimulation between M and $M'$ that contains $(s,s')$. A rel-$\varDelta$-bisimulation on a model M is a rel-$\varDelta$-bisimulation between M and M. We define the notion of rel-$\varDelta$-bisimilarity between states in potentially different models via the disjoint union (analogously to the notion of o-$\varDelta$-bisimilarity): Two pointed models (M, s) and $(M',s')$ are rel- $\varDelta$ -bisimilar, written $(M,s) \sim _{\!\varDelta }(M',{s'})$, if $(M+M',\iota _1(s)) \sim _{\!\varDelta }^{\mathsf {betw}}(M+M',\iota _2(s'))$, i.e.,. if there is a rel-$\varDelta$-bisimulation on $M+M'$ that contains $(\iota _1(s),\iota _2(s'))$.

In Proposition 4 we will see that over a single model $\sim _{\!\varDelta }^{\mathsf {betw}}$ and $\sim _{\!\varDelta }$ coincide, but in general they differ. At first it would seem more natural to define rel-$\varDelta$-bisimilarity between pointed models as $\sim _{\!\varDelta }^{\mathsf {betw}}$. However, the following Example 1 (item 4) shows that this notion is too restrictive. The example also shows that, in general, rel-$\varDelta$-bisimulations are different from o-$\varDelta$-bisimulations.

Example 1

Consider the four figures (and matching items below) where we assume a single variable p to be false in all states of all models, except in figure where p is true at s and t.

The composition of two o- $\varDelta$ -bisimulations may not be an o- $\varDelta$ -bisimulation. $Z_1$ and $Z_2$ are o-$\varDelta$-bisimulations, but not $Z_1; Z_2=\{(s,u)\}$, as $\varDelta$-Zig fails.

A rel- $\varDelta$ -bisimulation may not be an o- $\varDelta$ -bisimulation. $Z_1$ is not an o-$\varDelta$-bisimulation, since $\varDelta$-Zig fails for $(s,t) \in Z_1$. However, $Z_1$ is a rel-$\varDelta$-bisimulation on M. The $Z_1$-coherent pairs are: $(\{s, s_1, s_2\}, U')$ and $(S, U')$ for all $U'$ with $t\in U'$, $(\{t\}, U')$ for all $U'$ with $t\notin U'$, and $(\emptyset , \emptyset )$. Since $R(s_1)=R(s_2)=R(t)=\emptyset$, (Coherence) for $(s_1, t)$ and $(s_2, t)$ is satisfied. For (s, t), e.g., for $(\{s, s_1, s_2\}, \{t\})$: $R(s)=\{s_1, s_2\}\subseteq \{s, s_1, s_2\}$ and $R(t)=\emptyset \subseteq \{t\}$, and for $(\{t\},\{s_1\})$: $R(s)=\{s_1, s_2\}\subseteq \{t\}^{c}$ and $R(t)=\emptyset \subseteq \{s_1\}$.

An o- $\varDelta$ -bisimulation may not be a rel- $\varDelta$ -bisimulation. $Z_2$ is an o-$\varDelta$-bisimulation, but not a rel-$\varDelta$-bisimulation, since $(\{s_1\}, \{s_2\})$ is $Z_2$-coherent, $(s, t)\in Z_2$, and $\emptyset = R(t)\subseteq \{s_2\}$, but $R(s)\nsubseteq \{s_1\}$ and $R(s)\nsubseteq \{s_1\}^{c}$.

A rel- $\varDelta$ -bisimulation on a disjoint union, but not between disjoints. The pictured relation is a rel-$\varDelta$-bisimulation on $M_{1}+M_2$, but there is no rel-$\varDelta$-bisimulation between $M_1$ and $M_2$ linking s and t. The only candidate is $\{(s,t)\}$, but the coherent pair $(\{s,s_1\}, \{t\})$ does not satisfy (Coherence). So $(M_{1}+M_2,\iota _1(s)) \sim _{\!\varDelta }^{\mathsf {betw}}(M_{1}+M_2,\iota _2(t))$, but not $(M_1,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M_2,t)$.

Although the two notions of contingency bisimulations differ at the level of relations, we can show that rel-$\varDelta$-bisimilarity coincides with o-$\varDelta$-bisimilarity. We will need the following lemma.

Lemma 2

Let $M=(S, R, V)$ be a Kripke model, and assume that $Z\subseteq S\times S$ is an equivalence relation. Z is an o-$\varDelta$-bisimulation iff Z is a rel-$\varDelta$-bisimulation.

Proof

First, suppose Z is an o-$\varDelta$-bisimulation and $(s, s')\in Z$. Since Z is an equivalence relation, we need to show that for all Z-closed subsets U,

$$\begin{aligned} (R(s)\subseteq U\; or\;R(s)\subseteq U^{c}) \quad \text {iff} \quad (R(s')\subseteq U\;or\;R(s')\subseteq U^{c}) \end{aligned}$$

(1)

To see that (1) holds, let $R(s)\subseteq U\; or\;R(s)\subseteq U^{c}$, where U is Z-closed. Suppose towards a contradiction that $R(s')\cap U\ne \emptyset$ and $R(s')\cap U^{c}\ne \emptyset$. Then, there are $t_1, t_2\in R(s')$ such that $t_1\in U$ and $t_2\in U^{c}$. Since U is Z-closed, $(t_1, t_2)\notin Z$. By applying $\varDelta$-Zag, there are $s_1, s_2\in R(s)$ such that $(s_1, t_1), (s_2, t_2)\in Z$. From $R(s)\subseteq U\; or\;R(s)\subseteq U^{c}$, we obtain $t_1, t_2\in U$ or $t_1, t_2\in U^{c}$, which is a contradiction. Therefore, $R(s')\subseteq U$ or $R(s')\subseteq U^{c}$. The other direction of (1) may be checked in a similar way.

Now, assume that Z is a rel-$\varDelta$-bisimulation, and let $(s,s') \in Z$. (Atoms) is immediate. For $\varDelta$-Zig, assume $t, t_1, t_2\in R(s)$ such that $(t_1, t_2)\notin Z$. Suppose towards a contradiction that there is no $t'\in R(s')$ such that $(t, t')\in Z$, then $Z(t)\cap R(s')=\emptyset$ and hence $R(s') \subseteq (Z(t))^c$. As Z(t) is Z-closed and Z is a rel-$\varDelta$-bisimulation we get by (Coherence) that $R(s)\subseteq Z(t)$ or $R(s)\subseteq (Z(t))^{c}$. But $R(s) \subseteq Z(t)$ is false since $(t_1,t_2) \notin Z$, and $R(s)\subseteq (Z(t))^{c}$ is also false since $t \in R(s) \cap Z(t)$. Hence we have a contradiction and conclude that Z satisfies the $\varDelta$-Zig condition. By a similar argument Z satisfies $\varDelta$-Zig.

We have the following analogue of Proposition 1, and it can be proved in a similar way (via closure properties). We omit a proof due to space limitations.

Proposition 2

For all Kripke models M, the relation $\sim _{\!\varDelta }^{\mathsf {betw}}$ on M is the largest rel-$\varDelta$-bisimulation on M, and it is is an equivalence relation on S.

It follows from Propositions 1 and 2, and Lemma 2 that the two notions of contingency bisimilarity coincide.

Proposition 3

Let M and $M'$ be Kripke models.

• 1. For all s, t in M: $(M,s) \,\approx _{\!\varDelta }^{\mathsf {on}}(M,t)$ iff $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M,t)$.

• 2. For all s in M and $s'$ in $M'$: $(M,s) \,\approx _{\!\varDelta }(M',s')$ iff $(M,s) \sim _{\!\varDelta }(M',s')$.

Recall that [4, 5] proved that over the class of all pointed Kripke models, o-$\varDelta$-bisimilarity $\,\approx _{\!\varDelta }$ is an equivalence. Due to Proposition 3(2), it follows that also rel-$\varDelta$-bisimilarity $\sim _{\!\varDelta }$ an equivalence.

Finally, we show that we could dispense with the notation $\,\approx _{\!\varDelta }^{\mathsf {on}}$ as item 1 of the next proposition ensures that no ambiguity can arise when writing $(M,s) \,\approx _{\!\varDelta }(M,s')$. We also clarify the similar question regarding $\sim _{\!\varDelta }^{\mathsf {betw}}$ and $\sim _{\!\varDelta }$.

Proposition 4

For all Kripke models M and $M'$:

• 1. $(M,s) \,\approx _{\!\varDelta }^{\mathsf {on}}(M,s')$ iff $(M,s) \,\approx _{\!\varDelta }(M,s')$.

• 2. $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M,s')$ iff $(M,s) \sim _{\!\varDelta }(M,s')$.

• 3. $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M',s')$ implies $(M,s) \sim _{\!\varDelta }(M',s')$. The implication is strict.

Proof

Item 1. ($\Rightarrow$): If Z is an o-$\varDelta$-bisimulation on M, then it is easy to prove that $Y := \{(\iota _1(s),\iota _2(t)) \mid (s,t) \in Z \}$ is a o-$\varDelta$-bisimulation on $M+M$.

($\Leftarrow$): Let Y be an o-$\varDelta$-bisimulation on $M+M$. Define $Z := \{(s,s') \in S \times S \mid \exists i,j \in \{1,2\} : (\iota _i(s), \iota _j(s')) \in Y \}$. To prove $\varDelta$-Zig for Z, suppose $(s,s') \in Z$ and $t, t_1, t_2 \in R(s)$ such that $(t_1,t_2) \notin Z$. This implies that $\iota _i(t), \iota _i(t_1), \iota _i(t_2) \in R_i(\iota _i(s))$, and there are $i,j \in \{1,2\}$ such that $(\iota _i(s), \iota _j(s')) \in Y$, and by definition of Z, $(\iota _i(t_1),\iota _i(t_2)) \notin Y$. By $\varDelta$-Zig for Y, there are $\iota _j(t'), \iota _j(t_1'), \iota _j(t_2') \in R_j(\iota _j(s'))$ such that $(\iota _i(t),\iota _j(t')), (\iota _i(t_1),\iota _j(t_1')), (\iota _i(t_2),\iota _j(t_2')) \in Y$. Hence $t' \in R(s')$ and $(t,t'), (t_1,t_1'), (t_2,t_2') \in Z$, which proves $\varDelta$-Zig. $\varDelta$-Zag can be proved in a similar manner.

Item 2. $\begin{array}[t]{rcll} (M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M,s') &{} \iff &{} (M,s) \,\approx _{\!\varDelta }^{\mathsf {on}}(M,s') &{} \text {Proposition 3(2)}\\ &{} {\iff } &{} (M,s) \,\approx _{\!\varDelta }(M,s') &{} \text {(Item 1)}\\ &{} \iff &{} (M,s) \sim _{\!\varDelta }(M,s') &{} \text {Proposition 3(1)} \end{array}$

Item 3. The implication can be proved using Lemma 3 and Proposition 5 of the next section. The converse fails since item 4 of Example 1 shows models $(M_1,s)$ and $(M_2,t)$ such that $(M_1,s) \sim _{\!\varDelta }(M_2,t)$, however, we do not have $(M_1,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M_2,t)$.

4 Neighbourhood Semantics of Contingency Logic

In this section we recall the neighbourhood semantics of $\mathcal {L}_{\varDelta }$ from [8], and then we proceed to introduce the notion of $\varDelta$-bisimulation between neighbourhood models, and investigate its properties.

Definition 7 (Neighbourhood models)

A neighbourhood frame is a pair $(S, \nu )$ where S is a set of states and $\nu :S\rightarrow \mathcal {P}(\mathcal {P}(S))$ is a neighbourhood function which assigns to each $s\in S$ its collection $\nu (s)$ of neighbourhoods. A neighbourhood model is a triple $M=(S, \nu , V)$ where $(S, \nu )$ is a neighbourhood frame and $V:\mathsf {AtProp}\rightarrow \mathcal {P}(S)$ is a valuation. A neighbourhood morphism between $M=(S,\nu ,V)$ and $M'=(S',\nu ',V')$ is a function $f: S \rightarrow S'$ such that (i) for all $p \in \mathsf {AtProp}$, $s \in V(p)$ iff $f(s) \in V'(p)$, and (ii) for all subsets $U \subseteq S'$, $f^{-1}(U) \in \nu (s)$ iff $U \in \nu '(f(s))$.

Neighbourhood morphisms are the neighbourhood analogue of bounded morphisms, and they indeed preserve truth of $\mathcal {L}_{\Box }$-formulas [9, Lemma 2.6], and hence also of $\mathcal {L}_{\varDelta }$-formulas. The semantics of $\mathcal {L}_{\Box }\cup \mathcal {L}_{\varDelta }$-formulas is given below in Definition 8.

In what follows, we will also use disjoint unions (or coproducts) of neighbourhood models. We recall the definition from [9, Definition 2.9]. Let $M_1=(S_1,\nu _1,V_1)$ and $M_2=(S_2,\nu _2,V_2)$ be two neighbourhood models. Their disjoint union $M_1+M_2$ is the model $M = (S,\nu ,V)$ where $S = S_1 + S_2$, $V(p) = \iota _1[V_1(p)] \cup \iota _2[V_2(p)]$, and for all $U \subseteq S_1 + S_2$, all $i=1,2$, and all $s_i \in S_i$: $U \in \nu (\iota _i(s_i))$ iff $\iota _i^{-1}[S_i] \in \nu _i(s_i)$. Being a bit sloppy and omitting explicit use of inclusion maps, this condition can be stated as: $U \in \nu (s_i)$ iff $U\cap S_i \in \nu _i(s_i)$. The definition of $\nu$ ensures that the inclusion maps $\iota _i :S_i \rightarrow S_1+S_2$ are neighbourhood morphisms, and hence preserve truth of $\mathcal {L}_{\Box }\cup \mathcal {L}_{\varDelta }$-formulas.

Definition 8 (Neighbourhood Semantics of Contingency Logic)

Given a neighbourhood model $M=(S, \nu , V)$. The interpretation of formulas from $\mathcal {L}_{\Box }$ and $\mathcal {L}_{\varDelta }$ in M is defined inductively for atomic propositions and Boolean connectives as usual. Truth of modal formulas is given by,

$\begin{array}{llcl} \qquad &{} M,s \, \models \, \Box \varphi \quad &{} \text{ iff } &{} \quad [\![ \varphi ]\!]_{M}\in \nu (s)\\ &{} M,s\, \models \, \varDelta \varphi \quad &{}\text{ iff } &{} \quad [\![ \varphi ]\!]_{M}\in \nu (s)\;or\; [\![ \varphi ]\!]^{c}_{M}\in \nu (s). \end{array}$

where $[\![ \varphi ]\!]_{M}=\{s\in S\;|\; M,s\, \models \, \varphi \}$ denotes the truth set of $\varphi$ in M. We write $(M,s) \equiv _{\varDelta }(M',{s'})$ if (M, s) and $(M',{s'})$ satisfy the same $\mathcal {L}_{\varDelta }$-formulas.

Again, it is clear that over neighbourhood models we can view $\mathcal {L}_{\varDelta }$ as a fragment of $\mathcal {L}_{\Box }$, since for all neighbourhood models M, all states s in M, and all $\varphi \in \mathcal {L}_{\varDelta }$, $M,s \, \models \, \varphi$ iff $M,s \, \models \, \varphi ^t$.

Augmented Neighbourhood Models. Neighbourhood semantics can be seen as a generalization of Kripke semantics, since every Kripke model can be turned into a pointwise equivalent neighbourhood model, cf. [2, Theorem 7.9]. For a Kripke model $K=(S,R,V)$, define $nbh (K)=(S,\nu _R,V)$ where $\nu _R(s) = \{X \subseteq S \mid R(s) \subseteq X \}$. It is straightforward to check that for all $\varphi \in \mathcal {L}_{\Box }\cup \mathcal {L}_{\varDelta }$,

$$\begin{aligned} K, s \, \models \, \varphi \quad \text {iff} \quad nbh (K), s \, \models \, \varphi . \end{aligned}$$

(2)

A neighbourhood model $(S,\nu ,V)$ is augmented (cf. [2]) if all neighbourhood collections are closed under supersets and under arbitrary intersections, that is, for all $s\in S$, if $U \in \nu (s)$ and $U \subseteq U' \subseteq S$, then $U' \in \nu (s)$; and $\bigcap \nu _R(s)\in \nu _R(s)$. For an augmented $M= (S, \nu , V)$, define a Kripke model $krp (M)=(S, R, V)$ by taking $R(s)=\bigcap \nu (s)$. Again, M and $krp (M)$ are pointwise equivalent, and we have $nbh ( krp (M)) = M$ and $krp ( nbh (K))=K$. Thus, Kripke models are in 1-1 correspondence with augmented neighbourhood models.

In [8, Theorem 19], the logic $\mathsf {CL}$ was shown to be sound and strongly complete with respect to the class of Kripke frames. From Eq. (2) it follows immediately that $\mathsf {CL}$ is sound and strongly complete with respect to the class of augmented neighbourhood frames. This question was left open in [6].

We now define the notion of $\varDelta$-bisimulation between neighbourhood models. The idea of this definition was inspired by the definition of precocongruences in [9] and the neighbourhood semantics of the $\varDelta$-modality.

Definition 9

(nbh- $\varDelta$ -bisimulation). Let $M=(S, \nu , V)$ and $M'=(S', \nu ', V')$ be neighbourhood models. A relation $Z\subseteq S\times S'$ is a nbh- $\varDelta$ -bisimulation (for “neighbourhood $\varDelta$-bisimulation”) if for all $(s,s')\in Z$, the following hold:

• $\mathbf {(Atoms)}$ s and $s'$ satisfy the same atomic propositions.

• $\mathbf {(Coherence)}$ for all Z-coherent pairs $(U, U')$:

  $$ U\in \nu (s) \text { or } U^{c}\in \nu (s) \quad \text {iff} \quad U'\in \nu '(s') \text { or } U'^{c}\in \nu '(s'). $$

We write $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M',{s'})$, if there is a nbh-$\varDelta$-bisimulation between M and $M'$ that contains $(s,s')$. A nbh-$\varDelta$-bisimulation on a model M is a nbh-$\varDelta$-bisimulation between M and M. Two pointed models (M, s) and $(M',s')$ are nbh- $\varDelta$ -bisimilar, written $(M,s) \sim _{\!\varDelta }(M',{s'})$, if $(M+M',\iota _1(s)) \sim _{\!\varDelta }^{\mathsf {betw}}(M+M',\iota _2(s'))$, i.e., if there is a nbh-$\varDelta$-bisimulation on $M+M'$ that contains $(\iota _1(s),\iota _2(s'))$.

The following proposition shows that there is no conflict between the notions of nbh-$\varDelta$-bisimulations and rel-$\varDelta$-bisimulations for augmented models. This allows us to simply speak of $\varDelta$-bisimulations, and it justifies the overloading of the notation $\sim _{\!\varDelta }$.

Proposition 5

A relation Z is a rel-$\varDelta$-bisimulation between Kripke models M and $M'$ if and only if Z is a nbh-$\varDelta$-bisimulation between $nbh (M)$ and $nbh (M')$. Consequently,

• 1. $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M',s')$ iff $( nbh (M), s) \sim _{\!\varDelta }^{\mathsf {betw}}( nbh (M'), s')$.

• 2. $(M,s) \sim _{\!\varDelta }(M',s')$ iff $( nbh (M), s) \sim _{\!\varDelta }( nbh (M'), s')$.

Proof

Item 1 is straigtforward to prove using the correspondence between Kripke models and augmented neighbourhood models. Item 2 can be proved using item 1 and the isomorphism $nbh (M+M') \cong nbh (M)+ nbh (M')$, which is easy to verify.

Over arbitrary pointed neighbourhood models, $\sim _{\!\varDelta }^{\mathsf {betw}}$ is strictly contained in $\sim _{\!\varDelta }$, but on a single neighbourhood model they coincide.

Lemma 3

For all pointed neighbourhood models (M, s) and $(M',s')$:

• 1. $(M,s) \,\sim _{\!\varDelta }^{\mathsf {betw}}(M',s')$ implies $(M,s) \,\sim _{\!\varDelta }(M',s')$. The implication is strict.

• 2. $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M,s')$ iff $(M,s) \sim _{\!\varDelta }(M,s')$.

Proof

Item 1. One can show that if Z is a nbh-$\varDelta$-bisimulation between $M_1$ and $M_2$, then the embedding $\iota (Z) = \{(\iota _1(s_1),\iota _2(s_2)) \mid (s_1,s_2) \in Z\}$ is a nbh-$\varDelta$-bisimulation on $M_1+M_2 = (S,\nu ,V)$. The implication is strict due to Example 1 (item 4) and Proposition 5.

Item 2. ($\Rightarrow$) follows from item 1. To prove ($\Leftarrow$), assume that Y is a nbh-$\varDelta$-bisimulation on $M+M$. We show that $Z := \{(s,t) \in S \times S \mid \exists i,j \in \{1,2\} : (\iota _i(s), \iota _j(t)) \in Y \}$ is a nbh-$\varDelta$-bisimulation on M. First, note that for all $s \in S$, $U \subseteq S$, and all $i\in \{1,2\}$: $\iota _i(s) \in \iota _1[U]\cup \iota _2[U]$ iff $s \in U$.

(Atoms): Let $(s,t) \in Z$ witnessed by $(\iota _i(s), \iota _j(t)) \in Y$ where $i,j \in \{1,2\}$. Since Y satisfies (Atoms), we have $\iota _i(s) \in \iota _2[V(p)] \cup \iota _1[V(p)]$ iff $\iota _j(t) \in \iota _1[V(p)] \cup \iota _2[V(p)]$, and hence $s \in V(p)$ iff $t \in V(p)$.

(Coherence): We first note that if the pair (U, V) is Z-coherent, then $(\iota _1[U]\cup \iota _2[U],\iota _1[V]\cup \iota _2[V])$ is Y-coherent. Namely, take any pair $(\iota _i(s), \iota _j(t)) \in Y$. By definition of Z, it follows that $(s,t) \in Z$. We now have $\iota _i(s) \in \iota _1[U]\cup \iota _2[U]$ iff $s \in U$ iff (by Z-coherence) $t \in V$ iff $\iota _j(t) \in \iota _1[V]\cup \iota _2[V]$. Furthermore, it is straightforward to show that for all $s\in S$, all $U \subseteq S$, and all $i\in \{1,2\}$:

$$\begin{aligned} U \in \nu (s)\iff & {} (\iota _1[U]\cup \iota _2[U]) \in \nu '(\iota _i(s)) \end{aligned}$$

(3)

$$\begin{aligned} U^c \in \nu (s)\iff & {} (\iota _1[U]\cup \iota _2[U])^c \in \nu '(\iota _i(s)) \end{aligned}$$

(4)

Coherence for Z now follows easily from (3), (4) and coherence for Y.

We state another basic fact about $\varDelta$-bisimilarity which can be proved using closure properties as for Proposition 1.

Proposition 6

For all neighbourhood models M, the $\varDelta$-bisimilarity relation $\sim _{\!\varDelta }$ on M is itself a $\varDelta$-bisimulation and an equivalence relation.

As desired, $\varDelta$-bisimilar states cannot be distinguished with the $\mathcal {L}_{\varDelta }$-language.

Proposition 7

For all pointed neighbourhood models $(M_1,s_1)$ and $(M_2,s_2)$, if $(M_1,s_1) {\;\sim _{\!\varDelta }\,} (M_2,s_2)$ then $(M_1,s_1) \equiv _{\varDelta }(M_2,s_2)$.

Proof

$(M_1,s_1) \sim _{\!\varDelta }(M_2,s_2)$ iff $(M_1+M_2,\iota _1(s_1)) \sim _{\!\varDelta }^{\mathsf {betw}}(M_1+M_2,\iota _2(s_2))$. Since the inclusion morphisms preserve truth, we have for all $\mathcal {L}_{\varDelta }$-formulas $\varphi$ that $M_1,s_1 \, \models \, \varphi$ iff $(M_1+M_2), \iota _1(s_1) \, \models \, \varphi$, and similarly for $M_2, s_2$. Hence it suffices to prove that for all models M, $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M,s')$ implies $(M,s) \equiv _{\varDelta }(M,s')$.

So assume that Z is a $\varDelta$-bisimulation on a model M. We prove that for all formulas $\varphi \in \mathcal {L}_{\varDelta }$ and all $(s,s') \in Z$, $M,s \, \models \, \varphi$ iff $M,s' \, \models \, \varphi$, by induction on $\varphi$. The base case $\varphi =p$ holds by (Atoms). The Boolean cases are routine, so lets turn to the case where $\varphi =\varDelta \psi$. By induction hypothesis, we have for all $(x,y) \in Z$, $x \in \mathopen {[\![}\psi \mathclose {]\!]}_M$ iff $y \in \mathopen {[\![}\psi \mathclose {]\!]}_{M}$. That is, the pair $(\mathopen {[\![}\psi \mathclose {]\!]}_M,\mathopen {[\![}\psi \mathclose {]\!]}_{M})$ is Z-coherent. As Z is a $\varDelta$-bisimulation, it follows that for all $(s,s') \in Z$, ($[\![ \psi ]\!]_{M}\in \nu (s)$ or $[\![ \psi ]\!]_M^{c}\in \nu (s)$) iff ($[\![ \psi ]\!]_{M}\in \nu '(s')$ or $[\![ \psi ]\!]_{M}^{c}\in \nu '(s')$), that is, $M,s \, \models \, {\varDelta \psi }$ iff $M,s' \, \models \, {\varDelta \psi }$.

As with the standard notions of Kripke and neighbourhood bisimulations, $\mathcal {L}_{\varDelta }$-equivalence does not always imply $\varDelta$-bisimilarity. Neither does $\mathcal {L}_{\varDelta }$-equivalence imply o-$\varDelta$-bisimilarity as shown in [7, Example 3.10]. The same example shows that also $\mathcal {L}_{\varDelta }$-equivalence, does not imply nbh-$\varDelta$-bisimilarity due to Propositions 3(2) and 5(2). However, a converse to Proposition 7 can be proved for an appropriate notion of saturated models following a similar line of reasoning as in [9, Sect. 4.1]. To this end, we introduce $\varDelta$-morphisms and $\varDelta$-congruences. They will play the part of neighbourhood morphisms and congruences from [9].

Definition 10

( $\varDelta$ -morphisms and $\varDelta$ -congruences). Let $M=(S,\nu ,V)$ and $M'=(S',\nu ',V')$ be neighbourhood models. A function $f:S \rightarrow S'$ is a $\varDelta$ -morphism from M to $M'$ if its graph $Gr (f)$ is a $\varDelta$-bisimulation. A relation is a $\varDelta$ -congruence if it is the kernel of some $\varDelta$-morphism.

It is natural to ask whether $\varDelta$-morphisms are a generalisation of neighbourhood morphisms (cf. Definition 7). This is indeed the case.

Lemma 4

Every neighbourhood morphism is a $\varDelta$-morphism.

As a step towards showing that $\varDelta$-congruences are $\varDelta$-bisimulations, we show that we can take quotients with respect to $\varDelta$-bisimulations that are also equivalence relations.

Proposition 8

( $\varDelta$ -quotient). Let $M=(S,\nu ,V)$ be a neighbourhood model and let Z be a $\varDelta$-bisimulation on M which is also an equivalence relation, i.e., for all Z-closed $U \subseteq S$ and all $(s,t) \in Z$,

$$ (U \in \nu (s) \text { or } U^c \in \nu (s)) \iff (U \in \nu (t) \text { or } U^c \in \nu (t)). \qquad \qquad (\dagger ) $$

We define the $\varDelta$ -quotient of M by Z as the model $M_Z = (S_Z, \nu _Z, V_Z)$ where $S_Z = \{[s] \mid s \in S\}$ is the set of Z-equivalence classes, $V_Z(p) = \{[s] \mid s \in V(p) \}$, and

$$ \nu _Z([s]) = \{U_Z \subseteq S_Z \mid q^{-1}[U_Z] \in \nu (s) \text { or } q^{-1}[U_Z]^c \in \nu (s)\}. $$

The quotient map $q:S \rightarrow S_Z$ given by $q(s)=[s]$ is a $\varDelta$-morphism, and $Z=\ker (q)$. Consequently, $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M_Z,[s])$.

We can now show that $\varDelta$-congruences are indeed a special kind of $\varDelta$-bisimulations. This will be used to prove the Hennessy-Milner theorem in a moment.

Proposition 9

Let $M=(S,\nu ,V)$ be a neighbourhood model and Z a relation on S. Z is a $\varDelta$-congruence iff Z is an equivalence relation and a $\varDelta$-bisimulation.

Proof

Assume $Z = \ker (f)$ for some $\varDelta$-morphism f from M to $M'$. Note that if U is Z-closed then (U, f[U]) is $Gr (f)$-coherent. Equation ($\dagger$) now easily follows from f being a $\varDelta$-morphism, and $Z=\ker (f)$. Conversely, if Z is an equivalence relation and a $\varDelta$-bisimulation on M, then we can form the $\varDelta$-quotient $M_Z$, and it follows that Z is a $\varDelta$-congruence.

Proposition 9 allows us to show a neighbourhood analogue of the fact that Kripke bisimilarity implies o-$\varDelta$-bisimilarity [7]. For neighbourhood models, the equivalence notion that matches the expressiveness of the language $\mathcal {L}_{\Box }$ is called behavioural equivalence [9]: Two pointed neighbourhood models (M, s) and $(M',{s'})$ are behaviourally equivalent if there exists a neighbourhood model N and neighbourhood morphisms $f:M \rightarrow N$ and $f':M' \rightarrow N$ such that $f(s) = f'(s')$.

Proposition 10

Let M be a neighbourhood model, and s, t two states in M. If (M, s) and (M, t) are behaviourally equivalent then they are $\varDelta$-bisimilar.

Proof

If (M, s) and (M, t) are behaviourally equivalent, then by [9, Proposition 3.20] the pair (s, t) is contained in a congruence, i.e. in the kernel of a neighbourhood morphism f. By Lemma 4, $\ker (f)$ is a $\varDelta$-congruence, which by Proposition 9, is a $\varDelta$-bisimulation on M, hence $(M,s) \sim _{\!\varDelta }^{\mathsf {betw}}(M,{t})$. Finally, it follows from Lemma 3 that $(M,s) \sim _{\!\varDelta }(M,{t})$.

Finally, we prove a Hennessy-Milner style theorem for an appropriate notion of saturated models which essentially comes from [9, Sect. 4.1].

Definition 11

( $\mathcal {L}_{\varDelta }$ -saturated model). Let $M=(S, \nu , V)$ be a neighbourhood model. A subset $X\subseteq S$ is $\mathcal {L}_{\varDelta }$ -compact if for all sets $\varPhi$ of $\mathcal {L}_{\varDelta }$-formulas, if any finite subset $\varPhi '\subseteq \varPhi$ is satisfiable in X, then $\varPhi$ is satisfiable in X. M is $\mathcal {L}_{\varDelta }$ -saturated, if for all $s\in S$ and all $\equiv _{\varDelta }$-closed neighbourhoods $X\in \nu (s)$, both X and $X^{c}$ are $\mathcal {L}_{\varDelta }$-compact.

Theorem 1

(Hennessy-Milner).

• 1. For all $\mathcal {L}_{\varDelta }$-saturated neighbourhood models M, and all states s, t in M: $(M,s) \equiv _{\varDelta }(M,t) \;\;\; \text {iff}\;\;\; (M, s) \;{\sim _{\!\varDelta }^{\mathsf {betw}}}\; (M, t).$

• 2. If $\mathbf {N}$ is a class of neighbourhood models in which the disjoint union of any two models is $\mathcal {L}_{\varDelta }$-saturated, then for all $M, M'$ in $\mathbf {N}$,

  $$ (M,s) \equiv _{\varDelta }(M',s') \;\;\; \text {iff}\;\;\; (M, s) \;{\sim _{\!\varDelta }}\; (M', s'). $$

Proof

Due to space limitations we only provide an outline. Item 1: Can be proved using the same line of argumentation as in the proofs of Lemma 4.3, Lemma 4.5 and Proposition 4.6 of [9]. More precisely, we can show for any neighbourhood model $M=(S,\nu ,V)$: (i) If all $\equiv _{\varDelta }$-coherent neighbourhoods $X \in \nu (s)$ are $\mathcal {L}_{\varDelta }$-definable then $\equiv _{\varDelta }$ is a $\varDelta$-congruence. (ii) If M is $\mathcal {L}_{\varDelta }$-saturated then for all $X \subseteq S$, X is $\equiv _{\varDelta }$-coherent iff X is $\mathcal {L}_{\varDelta }$-definable. The theorem follows from items (i) and (ii) together with Proposition 9.

Item 2: $(M,s) \equiv _{\varDelta }(M',s')$ implies $(M+M',s) \equiv _{\varDelta }(M+M',s')$ since the inclusion morphisms are $\varDelta$-bisimulations. By item 1, $(M+M',s) \sim _{\!\varDelta }^{\mathsf {betw}}(M+M',s')$, hence by definition, $(M,s) \sim _{\!\varDelta }(M',s')$.

As finite neighbourhood models are clearly $\mathcal {L}_{\varDelta }$-saturated, we have an immediate corollary.

Corollary 1

Over the class of finite neighbourhood models, $\mathcal {L}_{\varDelta }$-equivalence implies $\varDelta$-bisimilarity.

Frame Class (un)definability. We now use $\varDelta$-bisimulations to demonstrate that $\mathcal {L}_{\varDelta }$ is too weak to define some well-known frame classes. These results were already proved in [6, Proposition 7], but without the use of a bisimulation argument.

A frame class $\mathbf {F}$ is $\mathcal {L}_{\varDelta }$ -definable if there is a set $\varPhi \subseteq \mathcal {L}_{\varDelta }$ such that for all frames F, $F \in \mathbf {F}$ iff $F\, \models \, \varPhi$.

Let $\mathbf {M}$ be the class of (monotone) neighbourhood frames $(S, \nu )$ in which $\nu (s)$ is closed under supersets, for all $s \in S$. Let $\mathbf {C}$ be the class of neighbourhood frames $(S, \nu )$ in which $\nu (s)$ is closed under intersections, for all $s \in S$.

Example 2

Consider the neighbourhood frames shown here:

in particular, $\nu _1(s_2)=\nu _2(t_2)=\emptyset$. It can easily be checked that $Z=\{(s_1, t_1), (s_2, t_2)\}$ is a $\varDelta$-bisimulation. Note that $F_1 \in \mathbf {M}$, but $F_2 \not \in \mathbf {M}$.

Example 3

Consider the following neighbourhood frames:

in particular, $\nu _3(s_2)=\nu _4(t_2)=\emptyset$. It can easily be checked that $Z=\{(s_1, t_1),(s_2,t_2)\}$ is a $\varDelta$-bisimulation. Note that $F_3 \in \mathbf {C}$, but $F_4 \notin \mathbf {C}$.

Proposition 11

The frame classes $\mathbf {M}$ and $\mathbf {C}$ are not definable in $\mathcal {L}_{\varDelta }$.

Proof

Example 2 shows that $\mathbf {M}$ is not $\mathcal {L}_{\varDelta }$-definable, since suppose towards a contradiction that $\varPhi \subseteq \mathcal {L}_{\varDelta }$ defines $\mathbf {M}$. Then $F_1\, \models \, \varPhi$ and . Hence there is a valuation $V_2$ on $F_2$, a state $t_j$ in $F_2$ and a $\varphi \in \varPhi$ such that . We define a valuation $V_1$ on $F_1$ by $s_i \in V_1(p)$ iff $t_i \in V_2(p)$ for $i=1,2$ and all $p\in \mathsf {AtProp}$. It follows that $((F_1,V_1),s_i) \sim _{\!\varDelta }((F_2,V_2), t_i)$ for $i=1,2$, and hence that , which implies that , a contradiction.

Similarly, Example 3 can be used to show that $\mathbf {C}$ is not $\mathcal {L}_{\varDelta }$-definable.

5 Characterisation Results

We first recall the basic definition of an ultrafilter. Let S be a non-empty set. An ultrafilter over S is a collection of sets $\mathfrak {u}\subseteq \mathcal {P}(S)$ satisfying (i) $S\in \mathfrak {u}$ and $\emptyset \notin \mathfrak {u}$; (ii) $U_1, U_2\in \mathfrak {u}$ implies $U_1\cap U_2\in \mathfrak {u}$; (iii) $U_1\in \mathfrak {u}$ and $U_1\subseteq U_{2}\subseteq S$ implies $U_2\in \mathfrak {u}$; and (iv) for all $U\subseteq S$ we have $U\in \mathfrak {u}$ or $U^{c}\in \mathfrak {u}$.

The collection of all ultrafilters over S will be denoted by $Ult (S)$. For $s \in S$, the principal ultrafilter generated by s is $\mathfrak {u}_{s} =\{U\subseteq S\;|\; s\in U \}$.

Definition 12

(Ultrafilter extension [9]). Let $M=(S, \nu , V)$ be a neighbourhood model. The ultrafilter extension of M is the triple $M^{ ue }=( Ult (S), \nu ^{ue}, V^{ue})$ where $V^{ue}(p)=\{\mathfrak {u}\in Ult (S)\;|\; V(p)\in \mathfrak {u}\}$ and $\nu ^{ue}:Ult(S)\rightarrow \mathcal {P}(\mathcal {P}(Ult(S)))$ is defined by

$$ \nu ^{ue}(\mathfrak {u})=\{\hat{U} \subseteq Ult (S)\;|\; U \subseteq S, \Box (U)\in \mathfrak {u}\} $$

where $\Box (U)=\{s\in S\;|\; U\in \nu (s) \}$ and $\hat{U} = \{\mathfrak {v} \in Ult (S) \mid U \in \mathfrak {v} \}$.

Lemma 5

Let (M, s) be a pointed neighbourhood model. Then, $M^{ ue }$ is an $\mathcal {L}_{\varDelta }$-saturated model and $(M, s)\equiv _{\varDelta }(M^{ ue }, \mathfrak {u}_{s})$.

Proof

Since $\mathcal {L}_{\varDelta }$ can be seen as a fragment of $\mathcal {L}_{\Box }$, [9, Lemma 4.24] ensures that $(M, s)\equiv _{\varDelta }(M^{ ue }, \mathfrak {u}_{s})$ and [9, Proposition 4.25] ensures that $M^{ ue }$ is $\mathcal {L}_{\varDelta }$-saturated.

As in the $\mathcal {L}_{\Box }$ case, modal $\mathcal {L}_{\varDelta }$-equivalence in a model implies $\varDelta$-bisimilarity in the ultrafilter extension. (Apply Lemma 5 and Theorem 1.)

Proposition 12

Let M be a neighbourhood model and s, t states in M. Then, $(M,s)\equiv _{\varDelta }(M,t) \;\;\text {implies} \;\;(M^{ ue }, \mathfrak {u}_{s}){\;\sim _{\!\varDelta }\,} ( M^{ ue },\mathfrak {u}_{t} )$.

We are now ready to prove the characterisation theorems.

Theorem 2

An $\mathcal {L}_{\Box }$-formula is equivalent to an $\mathcal {L}_{\varDelta }$-formula over the class of neighbourhood models iff it is invariant under $\varDelta$-bisimulation.

Proof

This can be proved analogously to the characterisation result [7, Theorem 4.4] using the above notions of $\mathcal {L}_{\varDelta }$-saturation and ultrafilter extensions for neighbourhood models, together with the compactness of classical modal logic (via strong completeness), cf. [2, Sect. 9.2]. The only minor difference is that we must first take disjoint unions before taking the ultrafilter extension.

In [9], a Van Benthem style characterisation theorem was given for classical modal logic with respect to a two-sorted first-order correspondence language $\mathcal {L}_1$. The two sorts $\mathbf {s}$ and $\mathbf {n}$ correspond to states and to neighbourhoods, respectively, and the basic idea of viewing a neighbourhood model as a first-order $\mathcal {L}_1$-structure is to encode the neighbourhood function $\nu$ as a relation $R_\nu \subseteq \mathbf {s} \times \mathbf {n}$ between states and neighbourhoods, and encode subsets via the (inverse) element-of relation $R_\ni \subseteq \mathbf {n}\times \mathbf {s}$ between neighbourhoods and states. The language $\mathcal {L}_1$ is a first-order language with equality which contains a unary predicate symbol $\mathsf {P}$ (of sort $\mathbf {s}$) for each $p \in \mathsf {AtProp}$, a binary relation symbol $\mathsf {N}$ (interpreted by $R_\nu$), and a binary relation symbol $\mathsf {E}$ (interpreted by $R_\ni$). A translation $(-)^\sharp :\mathcal {L}_{\Box }\rightarrow \mathcal {L}_1$ is defined recursively over the Boolean connectives and atomic propositions, and by $(\Box \varphi )^\sharp = \exists u \;(\; x\mathsf {N}u \;\wedge \; \forall y \,(\, u \mathsf {E}y \leftrightarrow \varphi ^\sharp \;)).$ We refer to [9, Sect. 5] for further details.

Theorem 3

A first-order $\mathcal {L}_1$-formula is equivalent to an $\mathcal {L}_{\varDelta }$-formula over the class of neighbourhood models iff it is invariant under $\varDelta$-bisimulation.

Proof

Let $\alpha \in \mathcal {L}_1$ be invariant under $\varDelta$-bisimulations. It follows from Lemma 4 that $\alpha$ is invariant under neighbourhood morphisms, and hence under behavioural equivalence. From the characterisation theorem [9, Theorem 5.5] it follows that $\alpha$ is equivalent to $\varphi ^\sharp$ for some formula $\varphi \in \mathcal {L}_{\Box }$ which is necessarily also invariant under $\varDelta$-bisimulations. Hence by our Theorem 2, $\varphi$ is equivalent to $\psi ^t$ for some $\psi \in \mathcal {L}_{\varDelta }$.

6 Discussion and Future Work

We proposed a notion of contingency bisimulation on neighbourhood models, we related it to an existing notion of contingency bisimulation on Kripke models, and also provided the characterization of (neighbourhood) contingency logic as a fragment of the modal logic of necessity, and of first-order logic. Our work contributes to a research program aiming at generalizing knowing that to knowing whether, knowing how, knowing value, etc. [19], including weaker modal notions than knowledge.

In [8], the $\mathcal {L}_{\varDelta }$-theory of all Kripke frames was axiomatized by the logic $\mathsf {CL}$ (going back to [10,11,12, 20]). We observed (below (2)) that $\mathsf {CL}$ is sound and complete with respect to the class of augmented neighbourhood frames (which answers an open question in [7]). In [7] an axiomatization $\mathsf {CCL}$ of classical contingency logic (i.e., the $\mathcal {L}_{\varDelta }$-theory of all neighbourhood frames) is also given. This raises the questions of what the axiomatizations are of monotone contingency logic and regular contingency logic. Proposition 11 means that one cannot fill these gaps with the axioms $\varDelta \varphi \rightarrow \varDelta (\varphi \rightarrow \psi ) \vee \varDelta (\lnot \varphi \rightarrow \chi )$ and $\varDelta (\psi \rightarrow \varphi ) \wedge \varDelta (\lnot \psi \rightarrow \varphi ) \rightarrow \varDelta \varphi$ that are in $\mathsf {CL}$ but not in $\mathsf {CCL}$. So these questions remain open.

The (Coherence) condition in our definition of $\varDelta$-bisimulation is a non-local property, since one needs to check all Z-coherent pairs, so over large Kripke models the $\varDelta$-Zig and $\varDelta$-Zag conditions of o-$\varDelta$-bisimulations will be easier to check. As we proved that $\varDelta$-bisimilarity coincides with o-$\varDelta$-bisimilarity, one can view the $\varDelta$-Zig and $\varDelta$-Zag conditions as a back-forth characterisation of $\varDelta$-bisimilarity over Kripke models. We would like to find local zig-zag conditions also for $\varDelta$-bisimilarity over neighbourhood models.

The notion of $\varDelta$-bisimulation was based on the semantics of the modality $\varDelta$. It has a natural generalisation to the framework of coalgebraic modal logic [3, 15]. Many of our results hold at this general coalgebraic level. We are preparing a separate paper in which the coalgebraic perspective will be worked out.