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.

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:

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})

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.

\mathcal{M},w\vDash \Box p

This is true since [\![p]\!]_{\mathcal{M}}=\{w,v\}\in N(w).

\mathcal{M},w\vDash \Box q

This is true since [\![q]\!]_{\mathcal{M}}=\{w,u\}\in N(w).

\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).

\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).

\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.

\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).