Neighborhood Semantics for Modal Logic

Neighborhood models generalize relational models (also known as Kripke models) for modal logic. The original motivation for introducing these more general models was to provide a semantics for weak systems of modal logic (i.e., the non-normal modal logics). Over the past 30 years, inspired, in part, by application of modal logic in philosophy, game theory and AI, interest in neighborhood models has grown well beyond the original motivation. This book will quickly familiarize the reader with the general theory of neighborhood semantics for modal logic. The main takeaway message is that neighborhood models form an interesting and rich class of mathematical structures that can be fruitfully studied using modal logic. The book explains how neighborhood models fit within the large family of semantic frameworks for modal logic, and identifies the pitfalls and potential uses of neighborhood models.

From Relational to Neighborhood Models


Brief Overview

Suppose that At\mathsf{At} is a (finite or countable) set of sentence letters, or atomic propositions. The set of well-formed formulas generated from At\mathsf{At}, denoted L(At)\mathcal{L}(\mathsf{At}), is the smallest set of formulas generated by the following grammar:

p  ¬φ  (φψ)  φp\ |\ \neg\varphi\ |\ (\varphi\wedge \psi)\ |\ \Box\varphi

where pAtp\in\mathsf{At}.

Additional propositional connectives (e.g., , , \vee,\ \rightarrow,\ \leftrightarrow) are defined as usual. The dual modal operator φ\Diamond\varphi is defined as ¬¬φ\neg\Box\neg\varphi. Examples of modal formulas include: p¬p\Box p\vee \Box\neg p, (p¬p)\Box\Diamond(p\vee \neg p), p(qr),p\rightarrow \Box(q\wedge r), and (p(qr))\Box(p\rightarrow (q\vee \Diamond r)).

Definition 1. A neighborhood frame is a tuple W,N\langle W, N\rangle, where WW is a non-empty set, elements of which are called states, or possible worlds; and N:W((W))N:W\rightarrow\wp(\wp(W)) is a function assigning to each state a set of sets of states (where for any set XX, (X)\wp(X) is the powerset of XX, i.e., (X)={Y  YX}\wp(X)=\{Y\ |\ Y\subseteq X\}).

Definition 2. A neighborhood model is a tuple W,N,V\langle W, N, V\rangle, where W,N\langle W, N\rangle is a neighborhood frame and V:At(W)V:\mathsf{At}\rightarrow\wp(W) is a valuation function assigning to each atomic formula a subset of WW.

Definition 3. Suppose that M=W,N,V\mathcal{M}=\langle W,N,V\rangle is a neighborhood model and that wWw\in W. Truth of formulas φL(At)\varphi\in\mathcal{L}(\mathsf{At}) at ww is defined by recursion on the structure of φ\varphi:

  • M,wp\mathcal{M},w\models p iff wV(p)w\in V(p)    where pAtp\in \mathsf{At}
  • M,w¬φ\mathcal{M},w\models\neg\varphi iff M,w⊭φ\mathcal{M},w\not\models \varphi
  • M,w(φψ)\mathcal{M},w\models(\varphi\wedge\psi) iff M,wφ\mathcal{M},w\models \varphi and M,wψ\mathcal{M},w\models \psi
  • M,wφ\mathcal{M},w\models\Box\varphi iff [ ⁣[φ] ⁣]MN(w)[\![\varphi]\!]_{\mathcal{M}}\in N(w)

where [ ⁣[φ] ⁣]M={w  M,wφ}[\![\varphi]\!]_{\mathcal{M}}= \{w\ |\ \mathcal{M},w\models\varphi\} is the truth set of φ\varphi.

To illustrate the above definitions, suppose that M1=W,N,V\mathcal{M}_1=\langle W, N, V\rangle is a neighborhood model with W={w,v,u}W=\{w,v, u\}, N(w)={{v}}N(w)=\{\{v\}\}, N(v)=N(v) =\varnothing, N(u)={,{v},W} N(u) = \{\varnothing, \{v\}, W\}, V(p)={v,u}V(p)=\{v, u\}, and V(q)={w,v}.V(q)=\{w, v\}. Then, we have that:

  • M1,w(pq)\mathcal{M}_1, w\models\Box(p\wedge q) since [ ⁣[pq] ⁣]M1=[ ⁣[p] ⁣]M[ ⁣[q] ⁣]M1={v,u}{w,v}={v}N(w)[\![p\wedge q]\!]_{\mathcal{M}_1} = [\![p]\!]_\mathcal{M}\cap [\![q]\!]_{\mathcal{M}_1} = \{v, u\}\cap \{w, v\} = \{v\}\in N(w). One can check that [ ⁣[(pq)] ⁣]M1={w,u}[\![\Box(p\wedge q)]\!]_{\mathcal{M}_1} = \{w, u\}

  • M1,w⊭p\mathcal{M}_1,w\not\models \Box p since [ ⁣[p] ⁣]M1={v,u}N(w)[\![p]\!]_{\mathcal{M}_1}=\{v,u\}\notin N(w). One can check that [ ⁣[p] ⁣]M1=[\![\Box p]\!]_{\mathcal{M}_1} = \varnothing

  • M1,v⊭(p¬p)\mathcal{M}_1,v\not\models \Box (p\vee\neg p) since [ ⁣[p¬p] ⁣]M1=[ ⁣[p] ⁣]M[ ⁣[¬p] ⁣]M1={v,u}{w}={w,v,u}N(v)[\![p\vee\neg p]\!]_{\mathcal{M}_1} = [\![p]\!]_\mathcal{M} \cup [\![\neg p]\!]_{\mathcal{M}_1}=\{v,u\}\cup \{w\} = \{w, v, u\}\notin N(v). One can check that [ ⁣[(p¬p)] ⁣]M1={u}[\![\Box (p\vee\neg p)]\!]_{\mathcal{M}_1} = \{u\}

  • M1,u⊭(p¬p)\mathcal{M}_1,u\not\models \Box (p\wedge\neg p) since [ ⁣[p¬p] ⁣]M1=[ ⁣[p] ⁣]M[ ⁣[¬p] ⁣]M1={v,u}{w}=N(u)[\![p\wedge\neg p]\!]_{\mathcal{M}_1} = [\![p]\!]_\mathcal{M} \cap [\![\neg p]\!]_{\mathcal{M}_1}=\{v,u\}\cap \{w\} = \varnothing\in N(u). One can check that [ ⁣[(p¬p)] ⁣]M1={u}[\![\Box (p\wedge\neg p)]\!]_{\mathcal{M}_1} = \{u\}

There are other modal operators that can be defined in a neighborhood model. One modal operator that has been discussed in the literature is the following: For any neighborhood model M\mathcal{M} with a state ww,

M,w  ]φ\mathcal{M},w\models\ \langle\ ]\varphi iff there is a XN(w)X\in N(w) such that X[ ⁣[φ] ⁣]MX\subseteq [\![\varphi]\!]_{\mathcal{M}}.

The modal operators \Box and  ]\langle\ ] validate different formulas. A formula φ\varphi is valid on a neighborhood frame F=W,N\mathcal{F}=\langle W, N\rangle if for all models M=W,N,V\mathcal{M}=\langle W, N, V\rangle based on the frame F\mathcal{F}, for all wWw\in W, we have M,wφ\mathcal{M}, w\models \varphi

Fact 1. The formula  ](φψ) ]φ\langle\ ](\varphi\wedge\psi)\rightarrow\langle\ ]\varphi is valid on the class of all neighborhood frames, but (φψ)φ\Box(\varphi\wedge\psi)\rightarrow\Box\varphi is not valid on the class of all neighborhood frames.

Proof. Suppose that F=W,N\mathcal{F}=\langle W, N\rangle is a neighborhood frame, M=W,N,V\mathcal{M}=\langle W, N, V\rangle is a neighborhood model based on F\mathcal{F}, and wWw\in W. We will show that M,w ](φψ) ]φ\mathcal{M}, w\models \langle\ ](\varphi\wedge\psi)\rightarrow\langle\ ]\varphi. Suppose that M,w ](φψ)\mathcal{M},w\models \langle\ ](\varphi\wedge\psi). Then, there is some XN(w)X\in N(w) such that X[ ⁣[φψ] ⁣]M=[ ⁣[φ] ⁣]M[ ⁣[ψ] ⁣]M.X\subseteq [\![\varphi\wedge\psi]\!]_{\mathcal{M}} = [\![\varphi]\!]_{\mathcal{M}}\cap [\![\psi]\!]_{\mathcal{M}}. Then, since [ ⁣[φ] ⁣]M[ ⁣[ψ] ⁣]M[ ⁣[φ] ⁣]M,[\![\varphi]\!]_{\mathcal{M}}\cap [\![\psi]\!]_{\mathcal{M}}\subseteq[\![\varphi]\!]_{\mathcal{M}}, we have that X[ ⁣[φ] ⁣]M.X\subseteq [\![\varphi]\!]_{\mathcal{M}}. Hence, M,w ]φ\mathcal{M},w\models \langle\ ]\varphi. To see that (φψ)φ\Box(\varphi\wedge\psi)\rightarrow \Box\varphi is not valid, consider the above model M1\mathcal{M}_1 and the instance of this formula scheme (pq)p\Box(p\wedge q)\rightarrow \Box p. We have that M1,w(pq)\mathcal{M}_1, w\models\Box(p\wedge q) and M1,w¬p\mathcal{M}_1, w\models\neg \Box p, and so M1,w⊭(pq)p\mathcal{M}_1,w\not\models \Box(p\wedge q)\rightarrow \Box p.

The above two modalities are equivalent when the neighborhood funcations are closed under supersets. A neighborhood frame W,N\langle W, N\rangle is monotonic when for all wWw\in W, for all X,YWX, Y\subseteq W, if XN(w)X\in N(w) and XYX\subseteq Y, then YN(w)Y\in N(w). The simple, but instructive!, proof of the following fact is left to the reader.

Fact 2. The formula φ ]φ\Box\varphi\leftrightarrow\langle\ ] \varphi is valid on the class of monotonic neighborhood models.

We conclude this brief overview by clairfying the relationship between neighborhood models and relational models.

Definition 3. A relational frame is a pair W,R\langle W, R\rangle where WW is a non-empty set and RW×WR\subseteq W\times W is a relation on WW. We write R(w)={vwRv}R(w) = \{v\mid w\mathrel{R} v\} for the set of states accessible from ww. A relational model is a tuple W,R,V\langle W, R, V\rangle where V:At(W)V:\mathsf{At}\rightarrow\wp(W) is a valuation function (cf. Definition 2 above).

Truth for modal formulas at a state ww in a relational model M=W,R,V\mathbb{M}=\langle W, R, V\rangle is defined as in Defition 3 except that the last clause for the modal formulas is replaced with:

  • M,wφ\mathbb{M}, w\models \Box\varphi iff R(w)[ ⁣[φ] ⁣]MR(w)\subseteq [\![\varphi]\!]_\mathbb{M}, where [ ⁣[φ] ⁣]M={wM,wφ}[\![\varphi]\!]_\mathbb{M} = \{w\mid \mathbb{M}, w\models\varphi\}

The first observation is that for every relational frame W,R\langle W, R\rangle, there is a neighborhood frame W,NR\langle W, N_R\rangle validating the same formulas. Suppose that W,R\langle W, R\rangle is a relational frame. Let NR:W((W))N_R:W\rightarrow \wp(\wp(W)) be defined as follows: for all wWw\in W, NR(w)={XR(w)X}N_R(w)=\{X\mid R(w)\subseteq X\}. Then, it is straightforward to check that W,R\langle W, R\rangle and W,NR\langle W, N_R\rangle validate the same formulas.

The neighborhood frame W,NR\langle W, N_R\rangle derived from a relational model satisfies a number properties not satisfied by arbitrary neighborhood frames:

  • contains the unit: For all wWw\in W, WNR(w)W\in N_R(w)
  • closed under intersection: For all wWw\in W and X,YWX, Y\subseteq W, if XNR(w)X\in N_R(w) and YNR(w)Y\in N_R(w), then XYNR(w)X\cap Y\in N_R(w).
  • monotonic: For all wWw\in W and X,YWX, Y\subseteq W, if XNR(w)X\in N_R(w) and XYX\subseteq Y, then YNR(w)Y\in N_R(w).
  • contains the core: For all wWw\in W, NR(w)NR(w)\bigcap N_R(w)\in N_R(w)

Any neigbhrood frame satisfying the above conditions is equivalent to a relational model:

Fact 3. Suppose that F=W,N\mathcal{F}=\langle W, N\rangle contains the unit, is closed under conjunction, is monotonic and contains the core. Then the relational model W,RN\langle W, R_N\rangle with wRNvw\mathrel{R_N} v iff vN(w)v\in\bigcap N(w) validates the same formulas as F\mathcal{F}.