Suppose that $\mathsf{At}$ 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:

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

Definition 1. A neighborhood frame is a tuple $\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 function assigning to each state a set of sets of states (where for any set $X$, $\wp(X)$ is the powerset of $X$, i.e., $\wp(X)=\{Y\ |\ Y\subseteq X\}$).

Definition 2. A neighborhood model is a tuple $\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 to each atomic formula a subset of $W$.

Definition 3. 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\models p$ iff $w\in V(p)$    where $p\in \mathsf{At}$
• $\mathcal{M},w\models\neg\varphi$ iff $\mathcal{M},w\not\models \varphi$
• $\mathcal{M},w\models(\varphi\wedge\psi)$ iff $\mathcal{M},w\models \varphi$ and $\mathcal{M},w\models \psi$
• $\mathcal{M},w\models\Box\varphi$ iff $[\![\varphi]\!]_{\mathcal{M}}\in N(w)$

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

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

• $\mathcal{M}_1, w\models\Box(p\wedge q)$ since $[\![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 $[\![\Box(p\wedge q)]\!]_{\mathcal{M}_1} = \{w, u\}$

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

• $\mathcal{M}_1,v\not\models \Box (p\vee\neg p)$ since $[\![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 $[\![\Box (p\vee\neg p)]\!]_{\mathcal{M}_1} = \{u\}$

• $\mathcal{M}_1,u\not\models \Box (p\wedge\neg p)$ since $[\![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 $[\![\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 $\mathcal{M}$ with a state $w$,

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

The modal operators $\Box$ and $\langle\ ]$ validate different formulas. A formula $\varphi$ is valid on a neighborhood frame $\mathcal{F}=\langle W, N\rangle$ if for all models $\mathcal{M}=\langle W, N, V\rangle$ based on the frame $\mathcal{F}$, for all $w\in W$, we have $\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 $\mathcal{F}=\langle W, N\rangle$ is a neighborhood frame, $\mathcal{M}=\langle W, N, V\rangle$ is a neighborhood model based on $\mathcal{F}$, and $w\in W$. We will show that $\mathcal{M}, w\models \langle\ ](\varphi\wedge\psi)\rightarrow\langle\ ]\varphi$. Suppose that $\mathcal{M},w\models \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\models \langle\ ]\varphi$. To see that $\Box(\varphi\wedge\psi)\rightarrow \Box\varphi$ is not valid, consider the above model $\mathcal{M}_1$ and the instance of this formula scheme $\Box(p\wedge q)\rightarrow \Box p$. We have that $\mathcal{M}_1, w\models\Box(p\wedge q)$ and $\mathcal{M}_1, w\models\neg \Box p$, and so $\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 $\langle W, N\rangle$ is monotonic when for all $w\in W$, for all $X, Y\subseteq W$, if $X\in N(w)$ and $X\subseteq Y$, then $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 $\langle W, R\rangle$ where $W$ is a non-empty set and $R\subseteq W\times W$ is a relation on $W$. We write $R(w) = \{v\mid w\mathrel{R} v\}$ for the set of states accessible from $w$. A relational model is a tuple $\langle W, R, V\rangle$ where $V:\mathsf{At}\rightarrow\wp(W)$ is a valuation function (cf. Definition 2 above).

Truth for modal formulas at a state $w$ in a relational model $\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:

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

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

The neighborhood frame $\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 $w\in W$, $W\in N_R(w)$
• closed under intersection: For all $w\in W$ and $X, Y\subseteq W$, if $X\in N_R(w)$ and $Y\in N_R(w)$, then $X\cap Y\in N_R(w)$.
• monotonic: For all $w\in W$ and $X, Y\subseteq W$, if $X\in N_R(w)$ and $X\subseteq Y$, then $Y\in N_R(w)$.
• contains the core: For all $w\in 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 $\mathcal{F}=\langle W, N\rangle$ contains the unit, is closed under conjunction, is monotonic and contains the core. Then the relational model $\langle W, R_N\rangle$ with $w\mathrel{R_N} v$ iff $v\in\bigcap N(w)$ validates the same formulas as $\mathcal{F}$.