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.

Solutions to selected exercises (Coming soon!)

From Relational to Neighborhood Models
Core Concepts

The main objects of study are neighborhood models and propositional modal languages.

Suppose that \mathsf{At}=\{p,q,r,\ldots\} is a (finite or countable) set of sentence letters, or atomic propositions. The set of well-formed formulas generated from \mathsf{At}, denoted \mathcal{L}(\mathsf{At}), is the smallest set of formulas generated by the following grammar:
p\ |\ \neg\varphi\ |\ (\varphi\wedge \psi)\ |\ \Box\varphi
where p\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: \Box p\vee \Box\neg p, \ \Box\Diamond(p\vee \neg p),\ p\rightarrow \Box(q\wedge r), and \Box(p\rightarrow (q\vee \Diamond r)). Neighborhood semantics for the basic propositional modal language \mathcal{L}(\mathsf{At}) is defined as follows.

A function N:W\rightarrow\wp(\wp(W)), where W is a set and \wp(W) is the powerset of W (i.e., for any set X, \wp(X)=\{Y\ |\ Y\subseteq X\}) is called a neighborhood function.
A neighborhood frame is a tuple \mathcal{F}=\langle W, N\rangle, where W is a non-empty set, elements of which are called states, or possible worlds; and N:W\rightarrow\wp(\wp(W)) is a neighborhood function.
A neighborhood model is a tuple \mathcal{M}=\langle W, N, V\rangle, where \langle W, N\rangle is a neighborhood frame and V:\mathsf{At}\rightarrow\wp(W) is a valuation function assigning sets of states to atomic formulas.

Formulas \varphi\in\mathcal{L}(\mathsf{At}) are interpreted at states w in a neighborhood model.

Suppose that \mathcal{M}=\langle W,N,V\rangle is a neighborhood model and that w\in W. Truth of formulas \varphi\in\mathcal{L}(\mathsf{At}) at w is defined by recursion on the structure of \varphi:
• \mathcal{M},w\vDash p iff w\in V(p)    (where p\in \mathsf{At})
• \mathcal{M},w\vDash\neg\varphi iff \mathcal{M},w\nvDash \varphi
• \mathcal{M},w\vDash(\varphi\wedge\psi) iff \mathcal{M},w\vDash \varphi and \mathcal{M},w\vDash \psi
• \mathcal{M},w\vDash\Box\varphi iff [\![\varphi]\!]_{\mathcal{M}}\in N(w)
where [\![\varphi]\!]_{\mathcal{M}}= \{w\ |\ \mathcal{M},w\vDash\varphi\} is the truth set of \varphi.

An alternative definition of truth for the modal operator can be found in the literature. To keep the definitions separate, I introduce a new modal operator \langle\ ]\varphi with the following definition of truth at a state in a neighborhood model:

\mathcal{M},w\vDash\ \langle\ ]\varphi iff there is a X\in N(w) such that X\subseteq [\![\varphi]\!]_{\mathcal{M}}

In general, these two modal operators are not equivalent. In particular, the two modalities validates different formulas and inference ruls. For instance, \langle\ ](\varphi\wedge\psi)\rightarrow \langle\ ]\varphi is valid (true at any state in any neighborhood model), but \Box(\varphi\wedge\psi)\rightarrow \Box\varphi is not valid (there is a neighborhood model containing a state that makes an instance of this formula false). (Click to see the proof.)

Suppose that \mathcal{M}=\langle W, N, V\rangle is a neighborhood model with a state w\in W such that \mathcal{M},w\vDash \langle\ ](\varphi\wedge\psi). Then, there is some X\in N(w) such that X\subseteq [\![\varphi\wedge\psi]\!]_{\mathcal{M}} = [\![\varphi]\!]_{\mathcal{M}}\cap [\![\psi]\!]_{\mathcal{M}}. Then, since [\![\varphi]\!]_{\mathcal{M}}\cap [\![\psi]\!]_{\mathcal{M}}\subseteq[\![\varphi]\!]_{\mathcal{M}}, we have that X\subseteq [\![\varphi]\!]_{\mathcal{M}}. Hence, \mathcal{M},w\vDash \langle\ ]\varphi. Since \mathcal{M} and w was arbitrary, \langle\ ](\varphi\wedge\psi)\rightarrow \langle\ ]\varphi is true at any state in any neighborhood model. To see that \Box(\varphi\wedge\psi)\rightarrow \Box\varphi is not valid, consider an instance of this formula scheme \Box(p\wedge q)\rightarrow \Box p, and let \mathcal{M}=\langle W, N, V\rangle be a neighborhood model with W=\{w,v, u\}, N(w)=\{\{v\}\}, V(p)=\{v, u\}, and V(q)=\{w, v\}. Then, [\![p\wedge q]\!]_{\mathcal{M}}=\{v\}\in N(w), so \mathcal{M},w\models\Box(p\wedge q). However, [\![p]\!]_{\mathcal{M}}=\{v,u\}\notin N(w), so \mathcal{M},w\nvDash \Box p. Thus, \mathcal{M},w\nvDash\Box(p\wedge q)\rightarrow\Box p. (Close)

However, note that the two definitions of the modal operator are equivalent when the neighborhood function is closed under supersets (i.e., for all states w and all sets X and Y, if X\in N(w) and X\subseteq Y, then Y\in N(w)).

Example. Suppose that \mathcal{M}=\langle W, N, V\rangle is a neighborhood model, where W=\{w, v, u\}, N(w)=\{\{w,u\}, \{w,v\}\}, N(v)=\{\{w,v\}, \emptyset\}, N(u)=\{v\}, V(p)=\{w,v\}, and V(q)=\{w,u\}. This neighborhood model is depicted below. Answer the following questions to test your understanding of the basic definitions.

1. \mathcal{M},w\vDash \Box p
This is true since [\![p]\!]_{\mathcal{M}}=\{w,v\}\in N(w).
2. \mathcal{M},w\vDash \Box q
This is true since [\![q]\!]_{\mathcal{M}}=\{w,u\}\in N(w).
3. \mathcal{M},w\vDash \Box (p\wedge q)
This is false since [\![p\wedge q]\!]_{\mathcal{M}} = [\![p]\!]_{\mathcal{M}}\cap [\![q]\!]_{\mathcal{M}}=\{w\}\notin N(w).
4. \mathcal{M},v\vDash \Box (p\wedge \neg p)
This is true since [\![p\wedge \neg p]\!]_{\mathcal{M}} = [\![p]\!]_{\mathcal{M}}\cap [\![\neg p]\!]_{\mathcal{M}}=\emptyset\in N(v).
5. \mathcal{M},u\vDash \Box p
This is false since [\![p]\!]_{\mathcal{M}} = \{w,v\}\notin N(u). However, note that \mathcal{M},u\vDash \langle\ ]p.
6. \mathcal{M},w\vDash \Box\Box p
This is true since [\![\Box p]\!]_{\mathcal{M}}=\{x\ |\ [\![p]\!]_{\mathcal{M}}\in N(x)\}=\{w,v\}\in N(w).
Courses and Slides