Modal Semantics for Reasoning with Probability and Uncertainty
Nino Guallart

Modal Semantics for Reasoning with Probability and Uncertainty



*
    Nino Guallart
    Received Dec. 18, 2023; accepted Apr. 16, 2024.
===================================================



   
This paper belongs to the field of probabilistic modal logic, focusing on a comparative analysis of two distinct semantics: one rooted in Kripke semantics and the other in neighbourhood semantics. The primary distinction lies in the following: The latter allows us to adequately express belief functions (lower probabilities) over propositions, whereas the former does not. Thus, neighbourhood semantics is more expressive.
The main part of the work is a section in which we study the modal equivalence between probabilistic Kripke models and a subclass of belief neighbourhood models, namely additive ones. We study how to obtain modally equivalent structures.
 

Keywords: Neighbourhood semantics, Kripke semantics, Dempster-Shafer belief function, probability,  modal logic.





§ INTRODUCTION


The convergence of probability theory and modal logic has garnered significant attention across multiple disciplines.  Probabilistic modal logic has been the object of intense research in these fields over the last few decades.  Authors such as Nilsson <cit.>, Bacchus <cit.>, Fagin and Halpern <cit.>, Aumann <cit.>, Samet, Heifetz and Mongin <cit.>
have applied modal logic for the formalisation of subjective probability in different fields: economics, artificial intelligence or philosophy of science.  The basic idea is to develop a probability space within some kind of structure, with Kripke models being the most obvious choice. Modal semantics allows the combination of probability with other modal operators, and hence its applicability to different kinds of modal logics such as epistemic logic or dynamic epistemic logic <cit.>. 

The idea of generalising probability is not new and early works on lower probabilities can be dated to Keynes <cit.> and Koopman <cit.>. In this work, however, we will focus on belief functions, probably the most known generalisation of probability, developed from the works of Dempster <cit.>  and Shafer <cit.>. 
There is also an extensive work on logic for belief functions: Sossai <cit.>
Ruspini (<cit.> and Smets <cit.> have developed works in the field. A remarkable point is the similarity between modal epistemic logics and Dempster-Shafer's belief functions, which has been studied since the late 80's <cit.> <cit.>[See <cit.> for a comprehensive description of different works in the area.]. We are mainly interested in the interpretation of belief functions as generalisation of probability, leaving aside the interpretation of Dempster-Shafer theory as a theory of evidence. Some approaches to the topic, such as <cit.>, <cit.> focus on the uncertainty of fuzzy events. 

Goals and structure of this work.  The purpose of this work is to develop a neighborhood semantics for belief functions that is modally equivalent to Kripke structures with probability, making the latter a subclass of neighbourhood structures. The structure of the paper is as follows: Section <ref> offers a summary of the main theoretical concepts in probability that will be used. This work develops a modal logic for probability and belief functions and two semantics for it:  in section <ref> we introduce the syntax of the language, and then we focus on two possible semantics for it: We first develop a standard Kripke semantics <ref>, and then a semantics based in neighbourhood semantics <ref>.  We make a study of several issues related to the structure of the system of neighbourhoods in section <ref>, which will be used in section <ref>, where it is studied the correspondence between probabilistic Kripke models and a subclass of belief neighbourhood models, additive ones. It is based on the proofs of the relationship between augmented neighbourhood models and Kripke models. Thus  we will compare them, observing their differences in expressiveness.  Section <ref> concludes the paper.


 


§ BASIC CONCEPTS


Subjective probability is an agent's estimate or belief about the likelihood of an event. In this work, we will use propositional formulas to represent events using atomic and compound propositions, while modal operators ranging over propositions will serve to represent the agent's degrees of belief.  Probability is defined over σ-algebras, but here we will work over Boolean algebras. 





    (Probability measure on a Boolean algebra.) Given a Boolean algebra 𝒜, the  probability measure pr𝒜→ [0,1]  is a function that satisfies the following axioms:
    


  * pr(A)⩾ 0 for any A∈𝒜.

  * pr(⊤) = 1.

  * Finite additivity: pr(⋃_i=1^n A_i)= ∑_A_i=1^n pr (A_i), for a family of pairwise disjoint events  {A_i}_i=1^n, n∈ℕ.



For σ-algebras in general, the third axiom is stated for countable sets: pr(⋃_i=1^∞ A_i)= ∑_A_i=1^∞ pr (A_i).


Belief functions are a generalisation of subjective probabilities <cit.>. The following definition is taken from <cit.>, which is an adaptation to Boolean algebras of the  definition in  <cit.>:

(Belief function on a Boolean algebra.) A belief function on a Boolean algebra A is a function bel A → [0, 1] satisfying: 


  * bel(⊤)=1 and bel()=0.

  * bel(A)⩾ 0 for any A∈𝒜.

  * Superadditivity: bel(⋃_i=1^n A_n)=∑_i=1^n ∑_J⊆{1,…,n}:|J|=i (-1)^i+1 bel(⋂_j∈ J A_j)




The last condition is also called monotonicity. It can be seen as a weakened form of additivity. Belief functions are a subset of a broader family, lower probabilities. For the purposes of this work, it is sufficient to know that lower probabilities encompass belief functions, that the lower probability of ⊤ is 1, and the lower probability of  is 0, whereas monotonicity is not met, but a more general condition instead <cit.>. Lower probabilities and belief functions can be seen as the lower bound of a set of probabilities, that is, stating bel(A)=α entails that all probabilities for A greater than or equal to α are compatible with that belief function. From now on, when the term “lower probabilities" in mentioned in this work, it actually refers to belief functions as described above.


The following remark, that is a consequence of the previous definitions. will be one of the central ideas of this paper. 


(Probability functions and belief functions.)
A probability function is an additive belief function (an additive lower probability). <cit.>


As we will see, whereas Kripke semantics is able to interpret probabilities directly, in neighbourhood semantics they are a special case of belief functions. Neighbourhood semantics thus offers a broader expressiveness than Kripke semantics.





§ SYNTAX OF ℒ_PR


We now develop a modal propositional language to express probabilistic beliefs. It is a variation of works such as <cit.>, <cit.>, <cit.>, and other similar works, although with a  different notation. 
  will denote a non-empty finite set of atomic propositions.


 (Syntax.) We define recursively the formulas of the language ℒ_PR as follows, where p∈:


    ϕ ::= p | ϕ | (ϕϕ ) | B_⩾αϕ | B_⩾αϕ



The usual equivalences hold: ϕψ stands for (ϕψ), and ⊤ and  are for ϕϕ and ϕϕ. 
 α∈ [0,1] is a rational value. B_⩾αϕ is read in the same way that L_α in <cit.>: “ the agent assigns to ϕ a probability equal to or greater than α (at least α)". Similarly B_⩽αϕ is shorthand for B_⩾ 1-αϕ, which is read as “the agent assigns to ϕ a probability at most α". B_=αϕ, “the agent assigns to ϕ a probability of (exactly) α", is just B_⩾αϕ B_⩽αϕ. B_<αϕ is B_⩾αϕ  and B_>αϕ is B_⩾ 1-αϕ.

Analogously, B_= αϕ refers to a belief function, which can be understood as a lower probability, and could be read as  “the agent assigns a lower probability   of α to ϕ", or more informally as “the agent considers that the probability of ϕ is at least α" (that is, α is the lower probability of ϕ). B_⩾αϕ has a rather complicated translation, as “the agent assigns a lower probability to ϕ, which is at least α".  B_⩽αϕ, B_> αϕ and  B_< αϕ are defined as their probability counterparts.





§ SEMANTICS OF ℒ_PR




 §.§ Kripke semantics


Works on Kripkean semantics for probabilistic modal logic such as <cit.> define a probability distribution over the worlds that are accessible from a certain world w, and it is the type of semantics that we will develop here. Fagin and Halpern <cit.> provide another approach, a probability distribution defined for measurable sets of accessible worlds in a Kripke model. 



 
(Probabilistic Kripke model.) A probabilistic Kripke model  ℳ^P_K is  a tuple ⟨ W, μ,R,v ⟩, where W is a non-empty and finite set of worlds or states, v→℘(W) a valuation function that assigns to each letter the set of worlds in W that satisfy it, μ:W× W→ [0,1]  a probability function following these rules for a given w:




    
  * μ (w,w')⩾ 0 

    
  * ∑_w_i∈ Wμ(w,w_i) = 1


R W× W is defined in this way: (w,w')∈ R (usually stated as wRw') iff μ(w,w')>0, and (w,w')∉ R iff μ(w,w')=0. 


The definition of R and the requirement that ∑_w_i∈ Wμ(w,w')=1  entail that for every w there is at least one w' such that wRw'. Neither R nor μ are symmetric: In general, μ(w,w')≠μ(w',w) and wRw' does not equate to w'Rw.

 
(R and μ:)
The accessibility relationship R is not strictly necessary, since it is implicit in the probability measure μ. We have included it for simplifying some explanations.


 (Probability and belief measures in Kripke frames.)
Given a X⊆ W, we define its probability and belief measures from world w∈ W as follows:


    pr(w,X)=bel(w,X)=∑_w_i∈ Xμ(w,w_i)



A pointed model is a pair ⟨ M,w⟩ with M a model and w an world of its domain W. We will write M,w_K ϕ if the formula ϕ is true at the world w∈ W in Kripke model M. We assign truth values to formulas at a certain world as follows:


 (Interpretation of ℒ_PR in probabilistic Kripke models.)
Given a probability Kripke model ℳ^P_K, the satisfaction relation _K between pointed models and formulas is defined as follows:



  * ℳ^P_K,w_K p iff w∈ v(p).

  * ℳ^P_K,w_K ϕ iff ℳ^P_K,wϕ.

  * ℳ^P_K,w_K (ϕψ) iff ℳ^P_K,wϕ or ℳ^P_K,wψ.

  * ℳ^P_K,w_K B_⩾αϕ  iff pr(w,ϕ_M)⩾α

  * ℳ^P_K,w_K B_⩾αϕ iff bel(w,ϕ_M)⩾α



 ϕ_ℳ^P_K denotes the set { w∈ W | M,w_K ϕ}. 
 We simply use  ϕ_M or ϕ if there is there no possibility of confusion.
 The interpretation of the probabilistic modal operator we have just defined is close to previous works in subjective probabilities (<cit.> for example), and formally it is close to probabilistic labelled transition systems <cit.>.



(Logical consequence and logical equivalence in probabilistic Kripke models.)
A formula ψ is a logical consequence of ϕ  in probabilistic Kripke models if for all pointed models such that ℳ^P_K,wϕ, it is also that  ℳ^P_K,wψ. ϕ and ψ are logically equivalent in probabilistic Kripke models provided that,  for all pointed models, ℳ^P_K,wϕ if and only if ℳ^P_K,wψ.


 (Events and propositions.) 
We can identify each event with the set of all logically equivalent propositions, instead of with propositions. Thus, if ϕ and ψ are logically equivalent, for any Kripke model and any world in it, ℳ^P_K,w B_⩾αϕ if and only if ℳ^P_K,w B_⩾αψ. 


 (Equivalence between probabilities and belief functions in ℒ_PR.)  Given that the conditions for the satisfaction of B_⩾αϕ and B_⩾αϕ are the same, they are logically equivalent. This is not surprising, since probabilities are a kind of belief functions <ref>. However, we cannot adequately interpret a formula whose interpretation is a belief function which is not a probability. Since we are going to study the relationship between Kripke and neighbourhood semantics for ℒ_PR, we have included the operator B_⩾α in order to ensure that both semantics interpret all the formulas of the same language. 




(Example 1: A simple probabilistic Kripke model.)

Let us define W={w_1,w_2,w_3,w_4}. μ W× W is defined in the following matrix, where M(μ)_i,j=μ (w_i,w_j) (for example, μ (w_1,w_2)=M(μ)_1,2=0.4):






    M(μ)_ij= [   0 0.4 0.6   0; 0.4   0 0.6   0;   0   0 0.1 0.9;   0   0   0   1;     ]



It can be verified that the sum of each row is 1.  We add a valuation function such that v(p)={w_1,w_3} and v(q)={w_1,w_2}. In the picture belowe, we have omitted the relationships when μ is 0.





[draw,circle] (a) at (0,0)   w_1;
[draw,circle] (b) at (2,0) w_2;
[draw,circle] (c) at (0,-2) w_3;
[draw,circle] (d) at (2,-2) w_4;

[anchor=west, align=left] at (-1,0) p,q;
[anchor=west, align=left]  at (-1,-2) p;
[anchor=west, align=left] at (2.5,0) q;

[->] (a) to[out=30, in=150, looseness=1] node[above] 0.4 (b);
[->] (a) – node[left] 0.6  ++(c);

[->] (b) to[in=330, out=210, looseness=1] node[below] 0.4 (a);
[->] (b) – node[right] 0.6  ++(c);

[->] (c) – node[below] 0.9  ++(d);

[->] (c) to[out=240, in=210, looseness=8] node[left] 0.1 (c);
[->] (d) to[out=330, in=300, looseness=8] node[right] 1 (d);



Picture 1. Example of probabilistic Kripke model.




We have that R(w_1)={w_2,w_3}. In this model, M,w_1_K B_⩾ 0.6 p and  M,w_1_K B_1 B_⩾ 0.1 p. 







 §.§ Neighbourhood semantics



(Example 2: Expressing bounded probabilistic beliefs.) 

Probability modal logic is commonly used for expressing beliefs with a certain degree, but its formulation in natural language may be misleading. For example, if r means that it will rain tomorrow, B_⩾ 0.5 r is understood as  “Ann believes that the probability of raining tomorrow is at least 50%  (i.e. 0.5)", where the modal operator is used to express the graded beliefs of the agent we are considering, namely Ann. However,  the interpretation of the modal formula according to the previous definition is not exactly what has been expressed in natural language.  B_⩾ 0.5 r actually means that Ann believes with a certain degree of confidence that it will rain tomorrow, and that degree is at least 0.6: There is a definite probability value, which is at least 0.5.

“Ann believes that the probability of raining tomorrow is at least 50%" is usually interpreted in natural language as a lower probability: Ann is considering that the probability of raining cannot be lower than 50%, but she does not have a definite value, and therefore all values above 50% are compatible with her belief. If we see the model in Example 1, w_1 satisfies B_⩾ 0.5 r. If we try to express a lower probability by stating B_⩾ 0.5 r B_> 0.5 r, w_1 does not satisfy that formula, which actually expresses that the agent believes that the probability of raining is exactly 50%. Thus, we need another semantics for interpreting lower probabilities.


A possible alternative to Kripke semantics is neighbourhood semantics. It is better suited for non-normal logic, and probabilistic modal logic is a monotonic, non-normal modal logic. Neighbourhood semantics for probability modal logic are much rarer than Kripke semantics: Arló-Costa <cit.> proposed a model for a non-normal high probability operator,  and Herzig <cit.>  offered a qualitative interpretation of the modal operator. 


We briefly recall a few preliminary definitions of neighbourhood semantics:



(Neighbourhood frame and neighbourhood model.)
Neighbourhood frame and model
A neighbourhood frame is the ordered pair ⟨ W,N⟩
formed by a non-empty and finite set W and a neighbourhood function over it
N: W→℘(℘(W)) that assigns a set of subsets of W to each w∈ W. Given a neighbourhood frame ⟨ W,N⟩
and a set of atomic propositional formulas  with a valuation
function v: →℘(W), a neighbourhood model
is a triple M=⟨ W,N,v⟩.


In neighbourhood semantics, M,w satisfies □ϕ if ϕ_M∈ N(w), that is, if the set formed by all worlds that satisfy ϕ is one of the sets in the neighbourhood of w. 


(Some properties of neighbourhoods.)
These are some properties that neighbourhoods may have:


  * A neighbourhood is monotonic if X∈ N(w) and X⊆ Y entails Y∈ N(w).

  * A neighbourhood is closed under finite intersections provided that for a family of sets {X_i}_i∈ J such that for each i∈ J (J finite), X_i∈ N(w), then ⋂{X_i}_i∈ J∈ N(w).

  * A neighbourhood is closed under finite unions provided that for a family of sets {X_i}_i∈ J such that for each i∈ J (J finite), X_i∈ N(w), then ⋃{X_i}_i∈ J∈ N(w).

  * A neighbourhood is closed under complement provided that for each X∈ N(w), X^C∈ N(w).

  * A neighbourhood N(w) contains its core ∩ N(w) if the core of the neighborhood, the intersection of all sets in N(w), is a set in N(w).

  * A monotonic neighbourhood that contains its core is said to be augmented.




A high-probability modal operator is monotonic (P(ϕψ)→ Pϕ Pψ / Pϕ Pψ→ P(ϕψ)  is a valid axiom scheme), where “high probability" refers to a probability higher than a given threshold. However, this axiom can be generalised for any probability,
We will consider a belief function operator, intended to be a lower probability operator. To define the neighbourhood semantics of our modal probabilistic operator, we will add a probabilistic metrics. We will combine the previous idea of the high probability operator with a set of nested neighbourhoods, akin to Lewis' sphere model in <cit.>, one for each probability. 
We will also add a belief function.


 (Belief neighbourhood   model.) A tuple ℳ^B_N=⟨ W,b, {N_⩾α}_α∈ [0,1], {N_> α}_α∈ [0,1), v⟩ is  a belief neighbourhood   model if W is a non-empty, finite set of worlds, N a neighbourhood function W→℘(℘(W)), b a belief function W×℘(W)→ [0,1], and v→ W a valuation function.



 (Belief function in N(w).)
The function b:W×℘(W)→ [0,1] assigns a value to each X∈ N_⩾ 0(w),  satisfying:


  * b(w,W)=1, b(w,∅)=0.

  * bel(w,⋁_i=1^n ϕ_n)⩾∑_i=1^n ∑_J⊆{1,…,n}:|J|=i (-1)^i+1 bel(w,⋀_j∈ Jϕ_j)



 (Monotonicity of in N_⩾α(w).) 
All N_⩾α(w) are monotonic: If X∈ N_⩾α(w) and X⊆ Y, then Y⊆ N_⩾α(w).


 (N_α(w) and b(w,X).)
For all w∈ W, if b(w,X)⩾α, then X∈ N_⩾α(w), and if b(w,X)> α, then X∈ N_> α(w).



(Nesting of neighbourhoods.)  From the previous definitions, the system of nested neighbourhoods is established in this way: 


    
  * If α⩾β, then N_⩾α(w)⊆ N_⩾β(w).
    
  * N_> α(w)⊆ N_⩾α(w).
    
  * If α>β, then N_⩾α(w)⊆ N_>β(w).




(A remark about the relationship between N_⩾α(w) and b(w,X).)
Analogously to <ref>, the system of nested neighbourhoods N_⩾α is not strictly necessary. We could develop it just by using the belief measure b. If we did so, however,  we should redefine   neighbourhood semantics' concepts in terms of a neighbourhood measure, and all the concepts we are going to introduce here should be formulated in those terms.



Since b(w,∅)=0 for all w∈ W, then ∅∈ N_⩾ 0(w). Therefore, all subsets of W∈ N_⩾α(w).  In practice, we are only interested in the sets that correspond to the truth set of some ϕ. Thus, for any w∈ and any formula ϕ, ϕ_M∈ N_⩾ 0(w). If β =b(w,ϕ_M), then ϕ_M∈ N_⩾α(w) for all α⩽β. In order to do that, we must define the semantics of the model.


 (Semantics in belief neighbourhood models.)

Given a belief neighbourhood model ℳ^B_N, the satisfaction relation _N between pointed models and formulas is defined as follows:




  * ℳ^ B_N,w p iff w∈ v(p).

  * ℳ^ B_N,wϕ iff ℳ^ B_N,wϕ.

  * ℳ^ B_N,w (ϕψ) iff ℳ^ B_N,wϕ or ℳ^ B_N,wψ.


  * ℳ^ B_N,wB_⩾αϕ  iff ϕ∈ N(w) and b(w,ϕ)⩾α.

  * ℳ^ B_N,wB_> αϕ  iff ϕ∈ N(w) and b(w,ϕ)> α.




The following definition derives from the previous one:






  * ℳ^ B_N,w B_⩾αϕ iff ϕ∈ N(w) and b(w,ϕ)⩾α and b(w,ϕ)_M+b(w,ϕ)_M=1.




A special case of the latter is ℳ^ B_N,w B_= αϕ, which is b(w,ϕ)_M=α.  b(w,ϕ)_M=1-α according to the last definition.

 ϕ_ℳ^B_N denotes the set { w∈ W | M,w_N ϕ}. Again, we will denote it by  ϕ_M or ϕ is there no possibility of confusion about the semantics we are using.




(Logical consequence and logical equivalence in belief neighbourhood models.)
A formula ψ is a logical consequence of ϕ if for all belief neighbourhood pointed models ℳ^B_N,w that satisfy ϕ, it is also that  ℳ^B_N,w_Kψ.
ϕ and ψ are logically equivalent provided that, for all pointed belief neighbourhood models, ℳ^B_N,w_Kϕ if and only if ℳ^B_N,w_Kψ.



 (Probabilities and belief functions in neighbourhood models.)  In neighbourhood semantics, B_⩾αϕ is a logical consequence of B_⩾αϕ. The converse is not true, so therefore they are not logically equivalent.





Some properties of the set of nested neighbourhoods in the belief neighbourhood model are the following:


    
  * N_⩾ 0(w) and N_1(w) are the only neighbourhoods that contain their respective cores (∅ for N_⩾ 0(w)). Since all neighbourhoods are monotonic, N_⩾ 0(w) and N_1(w) are augmented.
    
  * N_⩾ 0(w) and N_1(w) are the only neighbourhoods that are closed under intersection, complement and union.
    
  * N_⩾ 0(w) is also the only one in which  W and ∅ belong to the neighbourhood.



(Example 2: A belief neighbourhood model.)


W={w_1,w_2,w_3,w_4}. In the following table, we show the truth sets in N_⩾ 0(w_1) and their belief value. For readability, we write b(X) instead of b(w_1,X). We define just the neighbourhood of w_1:






b(w_1,W) = 1                      

b(W\{w_1}) = 0.9      b(w_1,W\{w_2}) = 0.7       b(W\{w_3}) = 0.6      b(W\{w_4}) = 0.6  

b({w_1,w_2}) = 0.2      b({w_1,w_3}) = 0.3      b({w_4}) = 0.4           

b({w_2,w_3}) = 0.4       b(,{w_2,w_4}) = 0.5     b(w_3,{w_4}) = 0.6           

b({w_1}) = 0.1      b({w_2}) = 0.1      b({w_3}) = 0.2    b({w_4}) = 0.3      

b({}) = 0                       








Table 1. Example of neighbourhood frame (only b(w_1,X)).



We can verify that b is superadditive: For example, b(w_1,{w_1,w_2,w_3,w_4})=1⩾ b(w_1,{w_1,w_2})+b(w_1,{w_3,w_4})=0.2+0.6. 

If we add a valuation, we obtain a model. Let us make {w_3,w_4}= p_M. b(w_1, p_M)=0.7, and we have that M,w_1B_0.7p.







§ THE NON-MONOTONIC CORE OF N_> 0(W)

This section provides a characterisation of the sets in the nested neighbourhoods in terms of disjoint unions of certain sets that we will call elementary sets. In particular, we will see the relationship between the core of N_1(w) and these sets, which are the sets in N_⩾ 0(w) that are closed under the inclusion relation in that neighbourhood. This will be especially useful in the next section for the proofs of the equivalence between a certain subclass of additive belief neighbourhood models and probabilistic Kripke frames. The following two definitions are taken from <cit.>:


(Non-monotonic core.)
The non-monotonic core of a neighbourhood N(w), denoted N(w)^𝒩𝒞, is a subset of N(w) defined as follows:
 
    N(w)^𝒩𝒞 ={ X∈ N(X) | For all  X'⊆ W , if X'⊂ X, X'∉ N(w)}



N(w)^𝒩𝒞 contains the subset of minimal elements in N(w) under the subset relationship.  Regarding our system of nested neighbourhoods, we have the following: From the definition of non-monotonic core, it is immediate that  N_⩾ 0(w)^𝒩𝒞 contains just the empty set, whose belief measure is 0, and  N_1(w)^𝒩𝒞 contains just ∩ N_1 (w).  



(Core complete.)
A monotonic neighbourhood N(w) is core-complete if for all X∈ N(w), there is some X'∈ N(w)^𝒩𝒞 such that X'⊆ X.


A neighbourhood is core-complete if every set in it has a subset in the non-monotonic core of the neighbourhood. If a certain N(w) is monotonic and contains a finite number of sets, it is core-complete <cit.>. 

 In this work, we are dealing with a finite W, so the previous comment applies in particular to all nested neighbourhoods:

 
All nested neighbourhoods N_⩾α)(w) (α∈ [0,1]) and N_> α)(w) (α∈ [0,1)) are core-complete.

 
 We are going to use the previous concepts to study the core of N_1(w) in terms of the sets in the non-monotonic core of N_> 0(w).  



N_⩾ 0(w)^𝒩𝒞 contains just one set, the empty set. N_> 0(w)^𝒩𝒞 is the subset of N_> 0(w) formed by the sets in N_⩾ 0(w) whose belief function is greater than 0 and do not have subsets. We will call the sets in N_> 0(w)^𝒩𝒞 elementary sets.


The elementary sets in N_> 0(w)^𝒩𝒞 are pairwise disjoint.


The sets in a non-monotonic core are closed under the subset relation.


The following lemma is immediate, given that N_>0(w) is core-complete: 


Any X∈ N_> 0(w), have as a subset  the disjoint union of some elementary sets in N_> 0^𝒩𝒞(w).



We introduce the following definition:
 

(Interior of a set in N_⩾ 0(w).)
We define the interior of a set X∈ N_⩾ 0(w) as the union of all the sets in the maximal set of elementary sets of X, that is, the set that contains all elementary sets that are subsets of X:

    
    𝚒𝚗𝚝_N (X) = ⋃_E_i⊆ X, E_i ∈ N_>0(w)^𝒩𝒞 E_i



We have chosen the name by analogy with the concept of interior in topology, although the concept is not the same, since the elementary sets mentioned here are not open spaces.
This maximal subset will allow us to define b(w,X) in terms of the belief functions of the elementary sets in the maximal subset, given that the belief function is superadditive, and the elementary sets
are pairwise disjoint. 


(Belief function of a set X∈ N_>0(w).)
Given some X∈ N_>0(w), b(w,X)⩾𝚒𝚗𝚝_N (X)



If the maximal subset is empty, b(w,X)=0. 


∩ N_1 (w) is equal to the disjoint union of all elementary sets in N_> 0(w)^𝒩𝒞.


By lemma <ref>, ∩ N_1(w) has a  a maximal subset of elementary sets, whose union is _N(∩ N_1(w)). 
We must prove that all w_i∈∩ N_1(w) belongs to some elementary set. If this were not the case, then x_i∈ A for some set A such that b(w,A)=0. In this case b(w,∩ N_1(w)\ A)=1, and being disjoint A and ∩ N_1(w)\ A, then b(w,A)+b(w,∩ N_1(w)\ A)=1. 

but this would mean that ∩ N_1(w)⊆ (∩ N_1(w)\ A)  and (∩ N_1(w)\ A)⊆∩ N_1(w), that is, ∩ N_1(w)=∩ N_1(w)\ A. Therefore, A is empty and all worlds in ∩ N_1(w) belong to some elementary set.  Now we must prove that all elementary sets are subsets of ∩ N_1(w). Let us suppose that there is an elementary set E_i⊈∩ N_1(w). We have that  b(w,∩ N_1(w)∪ E_i)⩾ b(w,∩ N_1(w))+b(w,E_i)>1, because the sets are disjoint. Therefore, all elementary sets are subsets of ∩ N_1(w).

All elementary sets are pairwise disjoint, so ∩ N_1(w) is the pairwise union of all elementary sets:  ∩ N_1(w)=_N(∩ N_1(w))=_N(W).



(Belief function of the maximal subset of elementary sets of   N_1(w).)
The sum of the belief functions of all elementary sets is  equal to or less than 1.


From the previous propositions and lemmas, belief function being superadditive and b(w,∩ N_1(w))=1.


Lastly, we are going to characterise the class of belief neighbourhood frames in which beliefs are additive.


(Additive belief neighbourhood frame.)
A belief neighbourhood frame  is additive if the following holds:

    For all  w∈ W, b(w,⋃{A_i}_i∈ J)= ∑_i∈ J b(w,A_i)  (All A_i pairwise disjoint)



In this case, the belief function reduces to a probability function. To prove that a neighbourhood is additive, we do not need to verify it for all possible sets in  N_⩾ 0(w). We just need to verify the following proposition.


(Core complete neigbhourhood of N_>0(w) and additive neighbourhoods.)
If and only if the frame is additive, then for all w∈ W and, for all X∈ N_> 0(w), ∑_E_i∈ N_> 0(w)^𝒩𝒞 b(w,E_i)=1. 


If the frame is additive, by definition of additivity,  proposition <ref> and the elementary sets being pairwise disjoint, the sum of all the elementary sets in the neighbourhood of all w∈ W is 1. If the frame is not additive, for some w∈ W the sum of the belief functions of the elementary sets in its neighbourhood is less than 1.



We need to provide a condition for a set to be measurable. 


(Well-defined set.)
A set X in N_⩾α(w) is well-defined if X∩∩ N_1(w)=_N(X).


In other words, a set is well-defined if it does not insersect any elementary set which is not its subset.  A consequence of this definition, the last proposition and proposition <ref> is the following:


If the frame is additive, if a set X in N_⩾α(w) is well-defined, then.  b(w,X)=b(w,_N(X)).

 
If the frame is not additive or the set is not well-defined, we only can state b(w,X)⩾ b(w,_N(X)). When we define a model, sets corresponding to the truth sets of formulas should be well-defined. Otherwise, they may not be measurable. 
 
 


§ RELATIONSHIP BETWEEN PROBABILITY AND BELIEF MODELS





The relationship between probabilistic Kripke semantics and belief neighbourhood semantics is akin to the relationship between Kripke semantics and neighbourhood semantics: a Kripke model has a kind of equivalence called modal equivalence with an augmented neighbourhood model. 

We will ground our proof for probabilistic models in the aforementioned  equivalence between Kripke semantics and a subclass of the neighbourhood semantics. First, we recall the latter proof, and then we will develop our own proof for probability and belief. The original proof for the relationship between Kripke and augmented neighbourhood models can be found in <cit.>. Here we will follow Pacuit <cit.>, which is also the source of these definitions:


(R-necessity.)
Given a Kripke frame ⟨ W,R⟩, X⊆ W is  R-necessary at w if R(w)⊆ W. The set { X⊆ W | R(w)⊆ X  } will be denoted by 𝒩^R_w. 



(Pointwise equivalence.)
Given a non-empty set W, a Kripke frame ⟨ W,R⟩ and a neighbourhood frame ⟨ W,N⟩ are pointwise equivalent if, for all w∈ W and X⊆ W, X∈ N(w) iff X∈𝒩^R_w.



(Modal equivalence.) Given a modal language ℒ and two classes of models for it M and M', we say that M,w is ℒ-modally equivalent to M,w' iff the set {ϕ∈ℒ | M,wϕ} is the same than {ϕ∈ℒ | M',w'ϕ}.

Given models M and M', if for every pointed model M,w, there is some w' such that M,w and M,w' are pointwise equivalent, then  M and M' are modally equivalent. More generally, a class of models M is modally equivalent to a class of models M' iff for each pointed model M,w there is another pointed model M',w' such that they are modally equivalent.


Modal equivalence is a concept which encloses other well-known ones, such as bisimulation. However, bisimulation is defined within structures of the same kind (for example, bisimulation in Kripke or neighbourhood models). A usual way of proving that M and M' are modally equivalent  is showing a way of transforming  M into M' and vice versa. The following propositions are also taken from <cit.>:



(Kripke models and augmented neighbourhood models.) Let ⟨ W,R⟩ be a Kripke frame. Then, there is a modally equivalent augmented neighborhood frame. 


For each w∈ W, let N(w)=𝒩^R_w as described above, and ⟨ W,R⟩ is the desired neighbourhood frame, which is augmented. 



(Kripke models and augmented neighbourhood models.) 
Let ⟨ W,N⟩ be an augmented neighborhood frame. Then, there is a modally equivalent relational frame. 


From an augmented ⟨ W,N⟩, we define a binary relation R_N W× W in the following way: For every w,w'∈ W, let wR_Nv iff v∈∩ N(w). The frame ⟨ W,R_N⟩ is the desired Kripke frame.


As a result, we have the following:


(Kripke models and augmented neighbourhood models.) 
The class of Kripke models is modally equivalent to the class of augmented neighbourhood models.


If we add a valuation function v:→ W to the previous structures, we obtain the corresponding Kripke and neighbourhood models. We observe that the satisfaction of formulas is maintained in all w∈ W, by induction:

    
  * The satisfaction of atomic formulas is the same, since v is the same.
    
  * The satisfaction of the conjunction and negation of formulas is preserved, since in both semantics their interpretation is the same.
    
  * Satisfaction of the modal formulas: 
    
        
  * If M,w_K □ϕ, all worlds w_i such that wRw_i satisfy ϕ. In the augmented neighbourhood model, all w_i are in ∩ N(w)∈ N(w) and ∩ N(w)⊆ϕ_M'∈ N(w), and thus M',w_N ϕ by the definition of satifaction of □ϕ in neighbourhood semantics.
        
  * If M',w_N □ψ, by defining a relation R_N W× W as stated before, we obtain a set of worlds w_i such that wR_nw_i, and all of them satisfy ϕ. Thus, M,w_K□ϕ in the Kripke model.
     





Fagin and Halpern <cit.> show that for every probability structure, there is an equivalent structure in which belief functions have been defined, and the converse is not true in general, just under specific circumstances.
Having seen the relationship between Kripke frames and augmented neighbourhood frames, now we will study this relationship for probabilistic Kripke frames and a subclass of belief neighbourhood frames, namely additive ones. We will base our proof in the previous ones and the results of the previous section.



 Let ℳ^P_K =⟨ W,μ,R⟩ be a probabilistic Kripke frame. There is an additive belief neighbourhood frame which is modally equivalent to ℳ^P_K.
    


 If we have  ℳ^P_K, we first obtain  ∩ N_1(w) for each w∈ W in an analogous way to the procedure described in proposition <ref> for Kripke and neighbourhood models. It will be the core of an augmented neighbourhood <ref>. 
 
    Now let us consider all singletons  {w_i}⊆ R(w)=∩ N_1 (w). They will be the elementary sets in  N_> 0(w)^𝒩𝒞. We want to define an additive neighbourhood frame, and then we know by proposition  <ref> that the following condition has to be met: ∑_{w_i}∈ N_>0(w)^𝒩𝒞 b(w,{w_i})=1. Thus, for all singletons {w_i}, we define a function  b_k(w,{w_i})=μ(w,w_i).  We also specify that b(w,∅)=0, and thus ∅∈ N_⩾ 0(w). 

    We have to define the value of b for the rest of the sets in N_⩾ 0
    (w). Neighbourhoods are monotonic <ref>, so for every A⊆ W, we are going to consider its interior   _N(A) <ref>. We define b(w,A)=b(w,_N(A)) (see lemma <ref>). If _N(A)=0, then b(w,A)=0.


 
Let ℳ^B_N=⟨ W,b,{N_⩾α,α∈ [0,1]}⟩ be   an additive belief neighbourhood frame. There is a probabilistic Kripke frame which is modally equivalent to ℳ^B_N.


    
    For all w∈ W, we define a binary relationship R_N:W× W in this way: wR_N w' iff w'∈∩ N_1(w). We will denote by R_N(w) the set of all w' in this relation. 

    We know from proposition <ref> that ∩ N_1(w) is equal to the disjoint union of the elementary sets in N_> 0(w)^𝒩𝒞. The frame is additive, so the sum of the beliefs of the elementary sets is equal to 1. Thus, we define a function μ_N:W× W→ [0,1] such that μ_N(w,w_i)=0 if  w'∉∩ N_1(w) and μ(w,w_i)>0 otherwise. The value of μ_N(w,w_i)>0 in this second case will be determined in the following step.
    
    Now we must consider each elementary set E_i. It will correspond to one or more w_i in R_N(w).  Since each set is disjoint, the exact value of μ(w,w_i)  is arbitrary, as long as the sum of μ_N(w,w_i) for all w_i within a given elementary set E_i is equal to b(w,E_i). We make this for all elementary sets.
    
    Since the frame is additive and ∩ N_1 (w)=⋃_i=1^n E_i for {E_i} disjoint sets, then b(w,∩ N_1 (w))=1=∑_i=1^n b(w,E_i).
    Thus, ∑_w_i∈ Wμ_N(w,w_i)=1.


As a consequence, we have the following result:


(Equivalence between probabilistic and belief models.) The class of probabilistic Kripke models is modally equivalent to the class of of additive  belief models.


Analogous to proposition <ref>. If we add a valuation v:→ W to the previous frames, we obtain the corresponding models. We just need to consider modal operators:



  * From Kripke to neighbourhood models: If ℳ^P_K,w B_⩾αϕ, then there is a subset of R(w) such that the sum of their probabilities μ(w,w_i) is a certain value α'⩾α, and the analogue value for ϕ is a certain value  β such that α'+β=1. By applying the process described in proposition <ref>, the elementary sets of the modally equivalent neighbourhood model are formed by a series of singletons, one for each world in R(w). The union of all the elementary sets corresponding to worlds in R(w) that satisfy ϕ is _N(ϕ_M).  b(w,ϕ_M)=b(w,_N(ϕ_M) is the sum of the beliefs of the elementary sets corresponding to worlds satisfying ϕ. Thus b(w,ϕ_M)=α'⩾α. The same reasoning applies to ϕ, giving a value of b(w,ϕ_M)=β. Therefore ℳ^B_NB_⩾α'⩾αϕ and ℳ^B_NB_⩾βϕ. We know that this logically entails ℳ^B_N B_⩾αϕ.


  * From additive neighbourhood to Kripke models: Let us have ℳ^B_N,w_N B_⩾αϕ. We first obtain R(w) from ∩ N_1(w) as described in proposition <ref>: We define R_N W× W such that wRw_i if w_i ∈∩ N_1(w). A subset of the worlds in ∩ N_1(w) satisfies ϕ, and this subset is also a subset of ϕ_M. More precisely, this subset, ∩ N_1(w)∩ϕ_M=_N (ϕ_M), and  by lemma <ref>, b(w_1,_N(ϕ_M))=b(w_1,ϕ_N). Thus, this value is at least α, and therefore, the worlds in R(w) that satisfy ϕ must sum up a probability of at least α. Therefore, ℳ^P_K,w_K B_⩾αϕ.




Not all belief neighbourhood frames have a modally equivalent probabilistic neighbourhood frame: If the neighbourhood frame is not additive, we cannot obtain a modally equivalent Kripke frame. Instead, there will be an infinite family of of probabilistic Kripke frames that are compatible with that belief neighbourhood model. This means that we can obtain an infinite family of Kripke models, and the formulas that are satisfied on them logically entail the formulas of the neighbourhood model, but the converse is not true in general.



(Example 4: From a probabilistic Kripke model to a belief neighbourhood model and back.)
From probabilistic Kripke model to belief neighbourhood model:  The ℳ^P_K in Example 1  (<ref>) can have a modally equivalent belief neighbourhood model. Let us study just one world, the process in the other ones is identical. Let us take w_1, we recall that in ℳ^P_K, μ(w_1,w_1)=0, μ(w_1,w_2)=0.4, μ(w_1,w_3)=0.6, μ(w_1,w_4)=0. We will assign a certain b to every subset of R(w_1)={w_2,w_3}. b(∅)=0, and thus b(w_1,{w_3})=μ(w_1,w_3)=0.6, and b(w_1,{w_2})=μ(w_1,w_2)=0.4. b({w_1}=0. The belief function for the rest of the subsets of W is defined from the belief function of their interior, that it is some of the previous sets. For example, b(w_1,W)=b(w_1,{w_2,w_3})=1, and b(w_1,{w_1,w_3})=b(w_1,{w_3})=0.6.

If we apply the valuation function that we have defined in Example 1, {w_1,w_3}= p_M, and thus b(w_1,p)=0.6. Similarly, {w_2,w_4}= p _M, and thus b(w_1, p)=0.4. That is, b(w_1,p)+b(w_1, p)=1.

From additive belief neighbourhood model to probabilistic Kripke model: Now let us see the belief neighbourhood model we have obtained. Let us take w_1 again, for example, and let us observe that ∩ N_1 (w_1)={w_2,w_3}. Both {w_2} and {w_3} are elementary sets in N_⩾ 0(w_1), and we know that b,(w_1,{w_2})+b,(w_1,{w_3})= 1, and thus the frame is additive.  

Let us define R_N W× W and μ_N W× W→ [0,1], and μ_N(w_1,w_2)=0.4 and μ_N(w_1,w_3)=0.6. Since each elementary set E_i is formed by a single world, we do not have to distribute the value of b(w_1,E_i) among several worlds. For several worlds, we should operate in this way: Let us assume that E_1={w_2,w_5}, then μ_N(w_1,w_2)+μ_N(w_1,w_5)=b(w_1,E_1), for example μ_N(w_1,w_2)=0.3 and μ_N(w_1,w_5)=0.1. Since w_1 and w_4 are not in ∩ N_1(w_1), then μ_N(w_1,w_1)=0 and μ_N(w_1,w_4)=0. We have that R_N(w_1)={w_2,w_3}, which is the set of worlds in ∩ N_1(w_1). We verify that μ_N(w_1,w_2)+μ_N(w_1,w_3)=1, which is the expected value.



(Example 5: Belief neighbourhood model with no modally equivalent probabilistic Kripke model.)
We can take the belief neighbourhood model that we have created in the previous example and just make two small changes. Let us make b(w_1,{w_2})=0.4 and b(w_1,{w_3})=0.3, but b(w_1,{w_2,w_3})=1. We have that b(w_1,{w_2,w_3}) > b(w_1,{w_2})+b(w_1,{w_3}) and thus additivity is not held <ref>. Thus, there is not a Kripke frame that is modally equivalent to this neighbourhood frame, but infinite Kripke frames, these with μ_N(w_1,w_2)⩾ b(w_1,{w_2})=0.3, μ_N(w_1,w_2)⩾ b(w_1,{w_3}=0.4,  and  μ_N(w_1,w_2)+μ_N(w_1,w_3)=1. 

Let us suppose a certain Kripke frame such that μ(w_1,w_2)=0.4 and μ(w_1,w_3)=0.6, being R(w_1)={w_2,w_3}. We have that ℳ^P_K,w_1_K B_0.4p, for example. B_0.4p logically entails B_0.3p, which is satisfied in w_1 in the neighbourhood model. However, B_0.3p does not logically entail B_0.4p. 






§ CONCLUDING REMARKS AND FUTURE WORK


Concluding remarks.  It has been shown that every probability can be understood as an additive belief function <ref>. In a probability Kripke model, it is possible to express subjective probabilities, which also are additive belief functions <ref>, but it is not possible to express arbitrary belief functions. In a neighborhood belief model, a probability is a special case of belief functions, additive ones. Thus, neighborhood models allow for a more expressive interpretation by distinguishing between probability and belief functions. In the final section, we have seen how to interpret this in terms of relationships between models: Every probabilistic Kripke model can be converted into a modally equivalent neighborhood model, but the reverse is only possible for additive belief neighbourhood models <ref>. They form a proper subclass of of belief neighborhood models.


Future works.
In this work we have deliberately omitted the consideration of conditional probability and conditional belief, which arise as an immediate logical extension. In future works, an possible line of research is their study and their connection to basic logical operations, such as probabilistic deduction and the application of Bayes' theorem. Specifically, our aim is to integrate these operations within the framework of belief neighborhood models, considering these operations on probabilistic Kripke models as equivalent to their counterparts in a specific subclass of neighbourhood models.





Acknowledgements. Thanks to the two anonymous peer reviewers who greatly helped with their suggestions to improve the final version of this article. 





