Which Semantics for Neighbourhood Semantics?

1 Epistemic Logic and Neighbourhood Semantics

Epistemic logic, the logic that studies notions like agents's beliefs and knowledge, is an important and long-standing area of research in artificial intelligence [Fagin et al., 1995].

In epistemic logic, the formula [α]ϕ is used to represent that agent α believes or knows that ϕ is the case. When the agent α is understood by context, or when we are not interested on modelling the behaviour of different agents at the same time, we will usually write [ ]ϕ instead of [α]ϕ. In the rest of this article we will discuss the case for a single agent. By adding the [ ] operator to classical propositional logic, we can already express a number of interesting properties. For example, the formula [ ](ϕ ∧ ψ) → ([ ]ϕ ∧ [ ]ψ) intuitively says that if an agent believes or knows the conjunction of two facts ϕ and ψ, then it also knows both ϕ and ψ.

Epistemic logic is usually considered a member of the large family of modal logics [Blackburn et al., 2001], and as we will discuss in this article, it shares with them many of their properties (e.g., characterizations in terms of bisimulations, good computational behavior, etc.). But, as it is well known (see [Vardi, 1986]), semantics specified over standard Kripke models in terms of possible worlds and accessibility relations [Blackburn et al., 2001] have some undesired epistemic properties. The reason is that even the weakest logic definable in terms of Kripke models (i.e., the modal logic K defined as

∗Work partially done while Master's student at Departamento de Computaci´on, FCEyN, UBA, Argentina.

Diego Figueira∗

INRIA, LSV, ENS Cachan, France

the set of those modal formulas valid on the class of all Kripke structures) may be already too strong for modeling knowledge or belief. For example, Kripke semantics makes valid all instances of the formula scheme ([ ]ϕ ∧ [ ](ϕ → ψ)) → [ ]ψ and the inference rule |= ϕ then |= [ ]ϕ, while both are unintuitive under an epistemic interpretation of [ ]. If we read [ ] as knowledge, they would require an agent to know all tautologies, and to be able to effectively draw all consequences of its knowledge. This is what is called the logical omniscience problem, and it was already discussed in [Hintikka, 1975].

[Vardi, 1986] proposes to adopt a different semantics, originally introduced in [Montague, 1968; 1970] and [Scott, 1968] in a different setup. This alternative semantics uses the notion of neighbourhoods to define the meaning of the epistemic operator. The intuitive idea is that an agent's knowledge is characterized not by a set of possible worlds but rather by an explicit set of propositions known by the agent. More precisely, we can define epistemic structures as follows.

Definition 1 (Epistemic Structure). An epistemic structure is a tuple M = 〈W, N, ‖ · ‖M〉 where

• W ̸= ∅ is a set (of possible worlds).
• N is a function mapping elements from W to sets of subsets of W (i.e., N(w) ⊆ ℘(W), for each w in W). We will usually write Nw instead of N(w) and call Nw the neighbourhoods of w.
• ‖ · ‖M is an assignment function from the set of propositional symbol to subsets of W (i.e., ‖p‖M ⊆ W, for each propositional symbol p ∈ PROP). ✸

Throughout the paper, letMbe the model 〈W,N, ‖ · ‖M〉 andM′ be the model 〈W ′ , N ′ , ‖ · ‖M′ 〉.

Notice that, instead of the standard accessibility relation between worlds in a Kripke model, an epistemic structure specifies, for each world w ∈ W, a set of sets Nw. As we can represent a proposition P by a set of possible worlds, the intuition is that if P ∈ Nw then P is known in w.

Given a model Mwe can extend ‖ · ‖M to all formulas in the language. The boolean cases are standard:

The [ ] operator, on the other hand, has been defined in two different ways in the literature, giving origin to two different operators that we will note [⊆] and [=]:

The [=] operator is the most widely used, and it is the one originally introduced in [Vardi, 1986]. We will call this semantics the strict neighbourhood semantics N=, because for [=]ϕ to be true at w, ‖ϕ‖M should be one of the neighbourhoods of w, i.e., ‖ϕ‖M ∈ Nw. The [⊆] operator on the other hand, is slightly weaker. We only require ‖ϕ‖M to cover at least one of the neighbourhoods of w and not to exactly coincide with it. We will call this weaker semantics the loose neighbourhood semantics N⊆, and it has been mentioned by van Benthem in a number of articles (e.g., [Aiello and van Benthem, 2002]).

It is easy to see that the two semantics are indeed different:

Example 2. Consider the epistemic structure

Actually, the following property can easily be proved.

Proposition 3. In any epistemic structure M, and for any formula ϕ, ‖[=]ϕ‖M ⊆ ‖[⊆]ϕ‖M.

We will investigate the difference between these two operators by means of bisimulations. In the next section we will show that while an elegant notion of bisimulation exists for N⊆, the required bisimulation for N= is rather involved. We will propose in Section 3 a simple extension of N= that we call N=(E), which comes together with a natural notion of bisimulation. Finally, we close the paper in Section 4 investigating the complexity of the satisfiability problem of N⊆ and N=(E), and show that they are both NP-complete.

2 Bisimulations for N⊆ and N=

It is easy to define an adequate notion of bisimulation for N⊆. Definition 4 (N⊆-bisimulation). Let M and M′ be two epistemic structures. An N⊆-bisimulation between M and M′ is a non-empty relation Z ⊆ W ×W ′ such that if xZx′ then:

We will use the notation 〈M, w〉 when w is an element of the epistemic structure M. Then we can write 〈M, w〉 ↔⊆ 〈M′ , w′ 〉 if there is an N⊆-bisimulation betweenMandM′ linking w and w′ . N⊆-bisimulations satisfy the expected properties: they preserve formulas in N⊆, and exactly characterize formula equivalence on finite models.

Definition 5 (Pointwise equivalence). Given 〈M,w〉 and 〈M′ ,w′ 〉 we say that they are pointwise equivalent for a semantics S (notation: 〈M,w〉 ≡S 〈M′ ,w′ 〉) iff ∀ϕ ∈ S : w ∈ ‖ϕ‖M iff w′ ∈ ‖ϕ‖M′ . ✸

Proposition 6. Given epistemic structuresMandM′ then: 〈M,w〉 ↔⊆ 〈M′ ,w′ 〉 implies 〈M,w〉 ≡N⊆ 〈M′ ,w′ 〉. If MandM′ are finite then the converse also holds.

The case for N= is more complex. Given that the semantic condition for N= is very similar to N⊆ we could try to use the following definition:

Definition 7 (Symmetric N=-bisimulation). Let M and M′ be two epistemic structures. A symmetric N=- bisimulation between M and M′ is a non-empty relation Z ⊆W ×W ′ such that if xZx′ then:

Prop: ∀p ∈ PROP, x ∈ ‖p‖M iff x′ ∈ ‖p‖M′ .

Zig: ∀T ∈ Nx ∃T ′ ∈ N ′x′ that verifies:

Zig 1: ∀w′ ∈ T ′ ∃w ∈ T s.t. wZw′ , and

Zig 2: ∀w′ ∈W ′ \ T ′ ∃w ∈W \ T s.t. wZw′ .

Zag: ∀T ′ ∈ N ′x′ ∃T ∈ Nx that verifies:

We will write 〈M, w〉 ↔s= 〈M′ , w〉 if there is a symmetric N=-bisimulation betweenMandM′ linking w and w′ .

Note that Definition 7 is an extension of the definition of N⊆-bisimulation with the symmetric conditions Zig 2 and Zag 2. Now, symmetric N=-bisimulations do preserve satisfiability of N= formulas (so do isomorphism, for that matter), but we will argue that it is too strong, and that they do not match the limited expressive power of N=.

Proposition 8. There exist finite epistemic structures which are pointwise equivalent and not symmetric N=-bisimilar.

Proof. Let us consider the following two models:

That is, M = 〈{w0, w1}, N, ‖ · ‖M〉, where ‖p‖M = {w1}, Nw0 = {{w1}}. And M′ = 〈{w′0 ,w′1 ,w′2 },N ′ , ‖ · ‖M′ 〉, where ‖p‖M′ = {w′1 ,w′2 }, ‖q‖M′ = {w′2 }, and N ′w′0 = {{w′1 }, {w′1 ,w′2 }}. w0 and w′0 satisfy the same formulas in N= but, even thoughMandM′ are finite, it is not possible to define a symmetric N=-bisimulation that links them .

Actually M and M′ in Proposition 8 are even differentiated, a notion we will introduce now, and that will be useful to define the adecuate notion of bisimulation for N=.

Definition 9 (Differentiation). The class D of differentiated epistemic structures is defined as

I.e., D is the class of epistemic structures where every neighbourhood is the extension of a formula. We say that T is differentiable inM if for some ϕ, ‖ϕ‖M = T , and that ϕ is a characteristic formula of T . The differentiation of M is the structureMd = 〈W,N d , ‖ · ‖M〉

I.e., N d is obtained by eliminating all sets in N which are not differentiable. ✸

It should be clear that the operation of differentiation does not affect satifiability of N= formulas as stated next (see [Areces and Figueira, 2008] for details).

Given Proposition 10, we can define the notion of N=- bisimulation only for differentiated epistemic structures.

Definition 11 (N=-bisimulation). Let M and M′ be two differentiated epistemic structures. An N=-bisimulation betweenMandM′ is a non-empty relation Z ⊆W×W ′ such that if wZw′ then:

Prop: ∀p ∈ PROP, w ∈ ‖p‖M iff w′ ∈ ‖p‖M′

Zig: ∀T ∈ Nw ∃T ′ ∈ N ′w′ that verifies:

Zig 1: ∀w′ ∈ T ′ ∃w ∈ T s.t. wZw′ , and

Zig 2: ∀X′ /∈ N ′w′ differentiable inM′ s.t. T ′ ⊊ X′ ⊆W ′ , then there are w′ ∈ X′ \ T ′ , w ∈ W \ T s.t. wZw′

Zag: ∀T ′ en N ′w′ ∃T ∈ Nw that verifies:

Zag 1: ∀w ∈ T ∃w′ ∈ T ′ s.t. wZw′ and

Zag 2: ∀X /∈ Nw differentiable in M s.t. T ⊊ X ⊆ W, then there are w ∈ X \ T,w′ ∈W ′ \ T ′ s.t. wZw′ ✸

We write 〈M,w〉 ↔= 〈M′ ,w′ 〉 if there is an N=- bisimulation betweenMandM′ linking w and w′ . We first check that N=-bisimulations preserve satisfiability.

Proposition 12. Given epistemic structuresMandM′ then: 〈M, w〉 ↔= 〈M′ ,w′ 〉 implies 〈M,w〉 ≡N= 〈M′ , w′ 〉.

Proof. The Boolean cases are easy. We only discuss the case [=]ψ. Let Z be an N=-bisimulation linking w and w′ . [⇒] If w ∈ ‖[=]ψ‖M, then ‖ψ‖M ∈ Nw. By condition Zig 1, there must be a T ′ ∈ N ′w′ such that ∀x′ ∈ T ′ ∃x ∈ ‖ψ‖M such that xZx′ . Let x′ ∈ T ′ ∈ N ′w′ , as x ∈ ‖ψ‖M and xZx′ , by inductive hypothesis: x′ ∈ ‖ψ‖M′ . Hence T ′ ⊆ ‖ψ‖M′ .

To show that ‖ψ‖M′ ∈ N ′w′ , notice first that every world in ‖ψ‖M′ \ T ′ is not bisimilar to any other in W \ ‖ψ‖M because if any of these worlds s′ was bisimilar to another s ∈ W \ ‖ψ‖M, it would mean that s ̸∈ ‖ψ‖M but s′ ∈ ‖ψ‖M′ , which by inductive hypothesis is absurd. Now, if T ′ = ‖ψ‖M′ we are done, if T ′ ⊊ ‖ψ‖M′ , we know by bisimulation condition Zig 2 (taking X′ as ‖ψ‖M′ ), that necessarily T ′ ∪ (‖ψ‖M′ \ T ′ ) ∈ N ′w′ , for T ′ ∈ N ′w′ and all elements in ‖ψ‖M′ \ T ′ are not bisimilar to any other from W \ ‖ψ‖M. As T ′ ⊂ ‖ψ‖M′ , then T ′ ∪ (‖ψ‖M′ \ T ′ ) = ‖ψ‖M′ , this set is therefore differentiable (by the formula ψ), so ‖ψ‖M′ ∈ N ′w′ , i.e., w′ ∈ ‖[=]ψ‖M′ .

[⇐] The converse is analogous using Zag 1 and Zag 2.

Over finite models N= equivalence is precisely characterized by the notion of N=-bisimilarity as stated next.

Proposition 13. Let M and M′ be finite, differentiable epistemic structures then: 〈M,w〉 ≡N= 〈M′ ,w′ 〉 implies 〈M, w〉 ↔= 〈M′ , w′ 〉.

Proof. The required bisimulation Z is defined as wZw′ iff 〈M,w〉 ≡N= 〈M′ ,w′ 〉. By definition, (w,w′ ) ∈ Z and hence Z is non-empty. Prop also holds by definition.

Zig. Assume that Zig does not hold, i.e., wZw′ , T ∈ Nw yet ∀T ′ ∈ N ′w′ either Zig 1 or Zig 2 fail. Let N ′w′ = {T ′1 , . . . , T ′ t } ∪ {S′1 , . . . , S′ l } where all the elements from the first set fail Zig 1 and those from the second fail Zig 2. Let T = {h1, . . . , hn} and W \ T = {¯h1, . . . , ¯hm}.

Set ψ0 := ϕT where ϕT is a characteristic formula of T. As w ∈ ‖[=]ψ0‖M, w′ ∈ ‖[=]ψ0‖M′ and ‖ψ0‖M′ ∈ N ′w′ . Let us repeat the following reasoning argument taking as an invariant that at step r, ‖ψr‖M′ ∈ N ′w′ . We show that in every step, ‖ψr‖M′ ⊊ ‖ψr+1‖M′ . In a finite number of steps q ≤ #W ′ we will obtain ψq s.t. w ∈ ‖[=]ψq‖M but w′ ̸∈ ‖[=]ψq‖M′ , which contradicts the hypothesis. At step r:

If ‖ψr-1‖M′ = T ′k . Then there is h′k ∈ T ′k s.t. for every hi ∈ T there is ψk i where hi ∈ ‖ψk i ‖M but h′k ̸∈ ‖ψk i ‖M′ . Let ψr := ψr-1 ∧ (∨nj=1 ψk j ). It can be easily showed that w ∈ ‖[=]ψr‖M. If w′ ̸∈ ‖[=]ψr‖M′ , absurd. This is something that will happen if we have r = #W ′ , as ‖[=]ψ‖M′ will necessarily be the empty set. If not, iterate taking into account that ‖ψr‖M′ ⊊ ‖ψr-1‖M′ (because h′k no longer satisfies ψr), and besides ‖ψr-1‖M = ‖ψr‖M = T .

If ‖ψr-1‖M′ = S′k . Then, there exists ¯X′ = S′k ∪ {¯x′1 , . . . , ¯x′z } /∈ N ′w′ such that S′k ∩ {¯x′1 , . . . , ¯x′z } = ∅, differentiable by its characteristic formula (let it be η), where for every ¯x′i ∈ ¯X′ \ S′k and ¯hj ∈ W \ T there is a ¯ ψk i,j where ¯hj ∈ ‖ ¯ ψk i,j ‖M but ¯x′i ̸∈ ‖ ¯ ψk i,j ‖M′ . Let ψr := ψr-1 ∨ (η ∧ ∨zi=1 ∧mj=1 ¬ ¯ ψk i,j ). As there is no element x ∈ W \ T where M, x |= ∧mj=0 ¬ ¯ ψk i,j for any i, then there is no element x ∈ W \ T where M, x |= ∨zi=1 ∧mj=1 ¬ ¯ ψk i,j . This means that ‖ψr-1‖M = ‖ψr‖M = T. But every x′ ∈ ‖ψr-1‖M′ verifies M′ , x′ |= ψr, and ‖η ∧ ∨zi=1 ∧mj=1 ¬ ¯ ψk i,j ‖M′ = X′ . Then ‖ψr‖M′ = X′ . And as mentioned before, ‖ψr‖M′ /∈ N ′w′ . At this point we can stop iterating since we know that w ∈ ‖[=]ψr‖M but w′ ̸∈ ‖[=]ψr‖M′ . Which is absurd.

The Zag condition is proved similarly.

The finiteness condition of Prop. 13 cannot be dropped.

Lemma 14. Proposition 13 can fail in infinite models.

Proof. Let us consider the following two models:

I.e., M = 〈W,N, ‖ · ‖M〉, where W = {wi | i ≥ 0} ∪ {h}, Nw0 = {{wi | i > 0} ∪ {h}}, N ′a = ∅ for a ̸= w′0 , and ∀i > 0 : ‖pi‖M = {w1, . . . ,wi, h}. And M′ = 〈W ′ , N ′ , ‖ · ‖M′ 〉, where W ′ = {w′i | i ≥ 0}, N ′w′0 = {{w′i | i > 0}}, N ′a = ∅ for a ̸= w′0 , and ∀i > 0 : ‖pi‖M′ = {w′1 , . . . ,w′i }. 〈M,w0〉 ̸↔= 〈M′ ,w′0 〉 as h is not bisimilar to any element in Nw′0 (hence Zag is not satisfied). However, w0 and w′0 satisfy exactly the same formulas of N=: for any ϕ, let pk be the proposition with biggest k in ϕ, then h cannot be distinguished from wk by ϕ.

3 Extensions to N=

In Section 2 we said that the notion of symmetric N=- bisimulations that we introduced in Def. 7, though natural, was too strong for N=. On the other hand, the notion of N=- bisimulations that we introduced in Def. 11 did seemed to match the expressive power of N= but it was involved.

We can solve this dilemma by strengthening the expressive power of N= to exactly match the behavior of symmetric N=-bisimulations. Paying some consideration to Definition 7, we may notice that the problem boils down to the logic's (in)ability to distinguish the subset relation between neighbourhoods. We can check then that he following binary operator ▽ would do the job:

If we call N=(▽) the logic that we obtain by extending N= with this operator, we have a perfect match for symmetric N=-bisimulations.

Proposition 15. Given two epistemic structures M and M′ then 〈M,w〉 ↔s= 〈M′ ,w′ 〉 implies 〈M,w〉 ≡N=(▽) 〈M′ ,w′ 〉. Moreover, if M and M′ are finite, then the converse also holds.

Proof. The proof is similar, but slighly more complex (and lengthier), than the previous results and we refer to the technical report [Areces and Figueira, 2008] for the details.

The trouble now is that ▽ seems rather artificial, and it is difficult to find a suitable epistemic interpretation for it. We have not sorted out the trouble with N=.

Luckily, we are now very close to a solution: we propose to extend N= with the existential modality E instead of ▽. The existential modality E is defined as

Let us call N=(E) the language N= extended with the E operator. The first thing we note is that ▽ can be expressed in N=(E): ‖ϕ▽ψ‖M = ‖[=]ϕ ∧ [=](ϕ ∨ ψ) ∧ E(ψ ∧ ¬ϕ)‖M.

Moreover, we can naturally adjust symmetric N=- bisimulation to N=(E).

Definition 16 (symmetric total N=-bisimulation). Let M and M′ be two epistemic structures. A total symmetric N=-bisimulation between these models is a symmetric N=- bisimulation Z ⊆ W ×W ′ such that the domain of Z coincides withW and the range of Z coincides withW ′ . ✸

That symmetric total N=-bisimulation preserve validity of formulas in N=(E) is easily checked.

Proposition 17. Let M, M′ be two epistemic structures, Z a total symmetric N=-bisimulation between them, w ∈ W, w′ ∈W ′ and wZw′ . Then, 〈M,w〉 ≡N=(E) 〈M′ , w′ 〉.

Proposition 18. Let M and M′ be two finite differentiable epistemic structures, such that 〈M,w〉 ≡N=(E) 〈M′ , w′ 〉. Then there exists Z, a total symmetric N=-bisimulation betweenMandM′ such that wZw′ .

Proof. Define xZx′ iff 〈M, x〉 ≡N=(E) 〈M′ , x′ 〉. We must prove that this is indeed a bisimulation. By definition, (w,w′ ) ∈ Z hence Z is non-empty and Prop holds. We must now check the other conditions of definition 16.

Zig. We will proceed with the same strategy as in the proof of Proposition 13. Assume that Zig does not hold, and let N ′w′ = {T ′1 , . . . , T ′ t } ∪ {S′1 , . . . , S′ l } where all T ′ i fail Zig 1 and all S′ i fail Zig 2. Let T = {h1, . . . , hn} and W \ T = {¯h1, . . . , ¯hm}.

Set ψ0 := ϕT the characteristic formula of T. As w ∈ ‖[=]ψ0‖M, then w′ ∈ ‖[=]ψ0‖M′ and ‖ψ0‖M′ ∈ N ′w′ . Again we will take as an invariant that at step r, ‖ψr‖M′ ∈ N ′w′ . We show that in every step, ‖ψr‖M′ ⊊ ‖ψr+1‖M′ . In a finite number of steps q ≤ #W ′ we will obtain ψq s.t. w ∈ ‖[=]ψq‖M but w′ ̸∈ ‖[=]ψq‖M′ , which contradicts the hypothesis. At step r:

If ‖ψr-1‖M′ = T ′k . Then there exists h′k ∈ T ′k such that for every hi ∈ T there is a ψk i where hi ∈ ‖ψk i ‖M but h′k ̸∈ ‖ψk i ‖M′ . Let ψr = ψr-1 ∧ (∨nj=1 ψk j ). We state that w ∈ ‖[=]ψr‖M. If w′ ̸∈ ‖[=]ψr‖M′ , absurd. If not, iterate noting that ‖ψr‖M′ ⊊ ‖ψr-1‖M′ (because h′k does not satisfies ψr any longer) and therefore #‖ψr‖M′ < #‖ψr-1‖M′ , and besides ‖ψr-1‖M = ‖ψr‖M = T .

If ‖ψr-1‖M′ = S′k . Then there exists ¯h′ ∈ W ′ \ S′k such that for every ¯hi ∈ W \ T there is a ¯ ψk i where ¯hi ̸∈ ‖ ¯ ψk i ‖M but ¯h′ ∈ ‖ ¯ ψk i ‖M′ . Let ϕk = ∧mi=0 ¯ ψk i , ψr = ψr-1 ∨ ϕk . If ‖ψr‖M′ /∈ N ′w′ , then w ∈ ‖[=]ψr‖M but w′ ̸∈ ‖[=]ψr‖M′ , a contradiction. Otherwise, let η = E(ϕk ∧ ¬ψr-1), then w′ ∈ ‖η‖M′ but w ̸∈ ‖η‖M. Again a contradiction.

Zag is proved similarly.

Finally, we should show that Z is total. Suppose that it is not. Without loss of generality, suppose that there exists v ∈ W that is not bisimilar to any other element of W ′ . Let W ′ = {w′0 , . . . ,w′p }. By definition of bisimulation, this means that v is not equivalent to any world in W ′ . Then, for every w′i there is ψi s.t. v ∈ ‖ψi‖M but w′i ̸∈ ‖ψi‖M′ . Let ψ = ∧pi=0 ψi. Then w ∈ ‖Eψ‖M but w′ ̸∈ ‖Eψ‖M′ , contradicting that w and w′ are pointwise equivalent.

It is easy to see that N⊆ is not more expressive than N=(E), as N⊆ cannot express properties of 'unconnected' states in the model. We can use bisimulations to prove that also N=(E) is not more expressive than N⊆ (we refer again to [Areces and Figueira, 2008] for details).

Proposition 19. N=(E) and N⊆ are incomparable in terms of expressive power.

4 Complexity Analysis

In this section we will discuss the complexity of N⊆ and N=(E). It was already shown in [Vardi, 1989] that the complexity of satisfiabily for N= is NP-complete. We will first show that we can use that result to prove NP-completeness of N⊆. We will then prove that even when we extend N= with the E operator, the complexity remains in NP.

We start with some definitions (details in [Chellas, 1980]).

Definition 20 (Schema M and Supplementation). The formula schemaM is [ ](ϕ∧ψ) → [ ]ϕ∧[ ]ψ. It corresponds to the following conditions over a class of epistemic structures. If a model satisfies M for arbitrary ϕ and ψ then if X ⊆ Y and X ∈ Nw then Y ∈ Nw.

Let M be an epistemic structure. The supplementation of M, denotedM+, is the structure 〈W,N +, ‖ · ‖M〉 in which N + a is the superset closure of Na, for every a in W. That is, for every a ∈ W and X ⊆ W, X ∈ N + a if and only if Y ⊆ X for some Y ∈ Na. ✸

In what follows, we will need to compare satisfiability of formulas in N⊆ and N=. On the semantic side, we will write |=⊆ for the satisfaction relation of N⊆, and |== for satisfaction of N=. On the syntactic side we will always write [ ] for the modal operator, and interpreted according to the indicated semantics. The following result is fairly straightforward and can be proved by induction on the complexity of the formula.

Proposition 21. For every formula ϕ and epistemic structure M, ‖ϕ‖M⊆ = ‖ϕ‖M+ = .

Corollary 22. Let S be the class of supplemented models. For every formula ϕ ∈ N⊆ and epistemic structure M ∈ S: M |=⊆ ϕ if and only if M |== ϕ.

Proof. EveryM∈ S verifiesM+ =Mby idempotence of supplementation. It only remains to apply Prop. 21.

Proposition 23. The satisfaction problem of N⊆ is in NP.

Proof. In [Vardi, 1989] we can find the NP algorithm for the satisfaction problem of N= restricted to the class S (the class of supplemented models, denoted as ε{3} in the literature).

To check whether ϕ is satisfiable in N⊆, we can feed ϕ as input of the NP Turing machine that solves the satisfaction problem for N= over the class of supplemented models. If it answers yes, then there must be a supplemented model M+ such that M+, w |== ϕ. We can then instantiate Proposition 21 with M+ and, as M++ = M+, conclude that M+, w |=⊆ ϕ. Then, ϕ is satisfiable in N⊆. If it answers no, let us suppose ad absurdum that ∃M such that w ∈ ‖ϕ‖M⊆ . By Proposition 21 this implies that w ∈ ‖ϕ‖M+ = . But as the algorithm has answered no, there cannot be a supplemented model M+ that satisfies ϕ under N=. Absurd. Then, ϕ is unsatisfiable under N⊆.

Next we show an NP algorithm for satisfiability of formulas in N=(E). But first some necessary definitions.

Definition 24 (Valuation and Universal Valuation). A valuation for ϕ ∈ N=(E) is any function ν : sub(ϕ) ∪ {⊥} → {0, 1} such that, and: i) ν(ψ) = 1 iff ν(∼ψ) = 0; ii) if ν(Eψ) = 0 then ν(ψ) = 0; iii) ν(⊥) = 0; and iv) ν(ψ1 ∨ ψ2) = 1 iff ν(ψ1) = 1 or ν(ψ2) = 1. Here, sub(ϕ) stands for the set of subformulas of ϕ closed under ∼, where we define ∼(ψ) = ξ if ψ = ¬ξ, and ∼(ψ) = ¬ψ otherwise.

A universal valuation for ϕ is any function μ that fixes the values of all universal subformulas. Letting univ(ϕ) = {Eψ | Eψ ∈ sub(ϕ)}, then μ : univ(ϕ) → {0, 1}. We say that a valuation ν for ϕ is compatible with a universal valuation μ iff they agree in the value of all elements of univ(ϕ). ✸

We first describe the procedure intuitively and then give a precise algorithm. Given a formula ϕ, the algorithm describes the valuations present in the model that satisfies it. The procedure will first fix a universal valuation μ for the truth value for each Eψ subformula. All other valuations must be compatible with μ. We first guess a valuation ν such that ν(ϕ) = 1. If ν([=]ψ1) = 1 and ν([=]ψ2) = 0 for some pair of subformulas, this means that ‖ψ1‖ is a neighbourhood but ‖ψ1‖ is not. Then there must be an element where the truth value of ψ1 and of ψ2 differs. We require then a valuation ν ′ such that ν(ψ1) = 1 and ν(ψ2) = 0 (or viceversa). Recursively, the algorithm searches for new valuations satisfying similar demands. We can restrict it to always look for valuations not yet tried, to ensure termination.

In the code below, calls to witness(ψ1, ψ2,R) find a valuation that distinguishes ψ1 from ψ2. The valuations (that can be seen as elements from the model) are always maintained in the R variable. The first call to witness (line 2 of sat) just asks for for the existence of a valuation that makes ϕ true. We will also need witnesses for all formulas ψ such that μ(Eψ) = 1 as the second part of sat describes.

Algorithm: sat(ϕ)

1: guess a universal valuation μ for ϕ 2: R← witnessϕμ (ϕ, ⊥, ∅) 3: for all Eψ ∈ sub(ϕ) s.t. μ(Eψ) = 1 do 4: 5: R← witnessϕμ (ψ, ⊥, R) 6: end if 7: end for

• 1: guess a valuation ν for ϕ compatible with μ s.t.: ν(ψ1) = 1 and ν(ψ2) = 0, or ν(ψ1) = 0 and ν(ψ2) = 1
• 6: for all [=]η1, [=]η2 ∈ sub(ϕ) s.t. ν([=]η1) = 1 and
• 7: if there is no ν ′ ∈ R such that ν ′ (η1) = 1 and ν ′ (η2) = 0, or ν ′ (η1) = 0 and ν ′ (η2) = 1 then
• if there is no ν ∈ R where ν(ψ) = 1 then 8: return R Algorithm: witnessϕμ (ψ1, ψ2, R) 2: if there is not such a valuation then 3: print UNSAT and exit 4: end if 5: R←R∪ {ν} ν([=]η2) = 0 do 8: R← witnessϕμ (η1, η2, R) 9: end if 10: end for
• 11: return R

Complexity. The algorithm makes as many recursive calls as elements are in R when it ends. Each element in ν ∈ R is the witness for ψ1, ψ2 such that ν(ψ1) = 0 and ν(ψ2) = 1 or viceversa. We should also note that there are not more than two witnesses for a certain pair ψ1, ψ2, thanks to the condition of line 4 in sat and 7 in witness. We will then have at most O(|ϕ|2 ) elements in R, so the number of calls to the witness algorithm is polynomial. Checking that an assignment is a valuation, and that it is compatible with μ is polynomial. Then the body of witness takes only NP time.

Proposition 25. If sat(ϕ) succeeds then ϕ is satisfiable.

Proof. We build a model based on the elements from R returned by the algorithm. Let M be the model where W = R, and ‖p‖M = {ν ∈ R | p ∈ sub(ϕ) ∧ ν(p) = 1}. We define Nν as the smallest set such that, if ν([=]ψ) = 1, then {ν ′ | ν ′ (ψ) = 1} ∈ Nν. Our claim is that τ ∈ ‖ϕ‖M, for some τ ∈ W such that τ(ϕ) = 1. Note that there should exist such τ because of the first call to witness with ϕ as a parameter (line 2 of sat). Furthermore, we will prove that for every ψ ∈ sub(ϕ) and ν ∈ W: ν ∈ ‖ψ‖M iff ν(ψ) = 1. We proceed by induction on the length of the formula. It is easy to check the base case of propositional variables.

The modal case. Suppose now that ν ∈ ‖[=]ψ‖M, with [=]ψ ∈ sub(ϕ). Then ‖ψ‖M ∈ Nν. By IH, ‖ψ‖M = {ν ′ | ν ′ (ψ) = 1}, so {ν ′ | ν ′ (ψ) = 1} ∈ Nν.

By construction of Nν, any element of it is a set of the form {ν ′ | ν ′ (η) = 1}, caused by the existence of a formula [=]η ∈ sub(ϕ) such that ν([=]η) = 1. We then have that ‖ψ‖M = {ν ′ | ν ′ (ψ) = 1} = {ν ′ | ν ′ (η) = 1} ∈ Nν. Suppose ad absurdum that ν([=]ψ) = 0. As ν([=]η) = 1 and ν([=]ψ) = 0, when the algorithm was on the step where ν was added it must have either 1. added a new element ν ′ such that ν ′ (η) = 1 and ν ′ (ψ) = 0 (or viceversa), or 2. checked the existence of such an element in R. Either way there is an element ν ′ ∈ R such that it is in one but not in the other of the two sets: {ν ′ | ν ′ (η) = 1}, {ν ′ | ν ′ (ψ) = 1}. But then they cannot be equal. Absurd. Hence, ν([=]ψ) = 1.

The converse is simpler. Let us suppose ν([=]ψ) = 1, then {ν ′ | ν ′ (ψ) = 1} ∈ Nν by construction. Applying IH, ‖ψ‖M ∈ Nν and thus ν ∈ ‖[=]ψ‖M.

The universal modality. If ν ∈ ‖Eψ‖M with Eψ ∈ sub(ϕ), then there is an element ν ′ such that ν ′ ∈ ‖ψ‖M. Applying IH this happens iff ν ′ (ψ) = 1. By definition, ν and ν ′ are compatible with the μ returned by the algorithm.

Suppose ad absurdum that ν(Eψ) = 0. As ν and μ are compatible, and μ is fixed for all the calls to the witness algorithm, then we have that 0 = ν(Eψ) = μ(Eψ) = ν ′ (Eψ). By definition of valuation we have that if ν ′ (Eψ) = 0 then ν ′ (ψ) = 0, which is absurd. Hence ν(Eψ) = 1.

For the converse implication suppose ν(Eψ) = 1. Then μ(Eψ) = 1 and the procedure will have added an element ν ′ such that ν ′ (ψ) = 1 (lines 3, 4 of sat). By IH, ν ′ ∈ ‖ψ‖M, and hence ν ∈ ‖Eψ‖M = W.

Proposition 26. If ϕ is satisfiable then sat(ϕ) succeeds.

Proof. Let M be such that w ∈ ‖ϕ‖M. For Eψ ∈ sub(ϕ), define μ(Eψ) = 1 iff w ∈ ‖Eψ‖M, and for each v ∈ W and ψ ∈ sub(ϕ), let νv be such that νv(ψ) = 1 iff v ∈ ‖ψ‖M. It is easy to see that νv is a valuation, and that it is compatible with μ. Let S = {νv | v ∈ W}. The idea is that each time the algorithm needs to guess a valuation, it picks one from S.

Suppose however that at a certain point, witness(ψ1, ψ2) cannot find a suitable valuation among S. If the witness function was called from a valuation νv ∈ S, then -by definition of the algorithm- the call must have been made because νv([=]ψ1) = 1 and νv([=]ψ2) = 0 (or viceversa). And then -by construction of νv- it must be the case that v ∈ ‖[=]ψ1‖M and v ̸∈ ‖[=]ψ2‖M (or viceversa). This means that ‖ψ1‖M ∈ Nv and ‖ψ2‖M ̸∈ Nv (or viceversa), in other words ‖ψ1‖M ̸= ‖ψ2‖M. Let v′ ∈ (‖ψ1‖M ∪ ‖ψ2‖M) \ (‖ψ1‖M ∩ ‖ψ2‖M). Then νv′ ∈ S should have worked as a guessing for the algorithm. Absurd.

Corollary 27. The satisfiability problem for N=(E) is NPcomplete.

5 Conclusions

Neighbourhood semantics is widely used in epistemic logic, but sometimes it is not clear exactly which semantics is involved. As we discussed in this paper, two alternative proposals can be found in the literature.

We showed that N=, the semantics originally introduced in [Vardi, 1986] does not seem to have a nice characterization in terms of bisimulation, and we proposed N=(E) as a natural extension. The E operator can be used to model information which is globally true in an epistemic structure, hence the extension seems to be well motivated for the application. Moreover, a simple notion of bisimulation exists for N=(E) and its satisfiability problem remains NP-complete. We also showed that satisfiability for N⊆ is NP-complete mostly as a corollary of results from [Vardi, 1986].