Intro

We start with a typical Kripke frame $\mathcal{F}=(\mathcal{W},R)$ where $W$ is the set of possible worlds (think possible truth assignments to your set of propositional variables) and $R$ is a binary relation on those worlds.

A Kripke model is just some triple $(\mathcal{W},R,⊩)$ where $⊩$ is the forcing relation which determines the relationship between various worlds $w\in \mathcal{W}$ and modal formulas. It’s characterized by the following rules:

• $w⊩\mathrm{\neg }A$ if and only if $w⊮A$
• $w⊩A\to B$ if and only if $w⊩\mathrm{\neg }A$ or $w⊢B$
• $w⊩◻A$ if and only if for all $u$ satisfying $wRu$ we have that $u⊩A.$

(this also subsequently implies that $A$ is possible in world $w$ if and only if it is true in at least one world $u$ adjacent to $w,$ because it’s the dual of necessity)

Different modal logics are generated by changing the assumptions on $R$. For instance, forcing $R$ to be reflexive guarantees that $\mathbf{\text{T}}:◻A\to A$ will be satisfied. However, all Kripke models satisfy axiom $\mathbf{\text{K}}:◻(A\to B)\to (◻A\to ◻B),$ which makes Kripke models very good for representing normal modal logics and very bad at representing non-normal modal logics.

Necessitation as an operator has become popular in representing agents’ “beliefs”. E.g., you can take an agent, represent their policy in some modal logic, and $◻\varphi$ determines their belief in $\varphi$ while $⊢\varphi$ determines whether or not $\varphi$ is true in that world. And this is nice for a lot of things, and Kripke models are great for modeling provability logic, for instance.

But if we want necessity to be some sort of probabilistic operator—, for instance—then this becomes unsatisfactory. Probabilities don’t distribute over conditionals like that. So we want to relax this somehow.

Enter neighborhood semantics. We define a neighborhood frame to be a pair $(\mathcal{W},\mathcal{N}),$ where again $\mathcal{W}$ is the set of possible worlds and $\mathcal{N}:\mathcal{W}\to 2^{2^{\mathcal{W}}}$ is a “neighborhood function” which maps each world $w\in \mathcal{W}$ to a set of their neighborhoods.

Necessity here is defined differently: $w⊩◻\varphi$ if and only if the truth set of $\varphi$ is a neighborhood of $w.$ That is, there has to be a neighborhood of $w$ that contains exactly all worlds in which $\varphi$ is true, and then $w⊩◻\varphi .$

It’s easy to see that this is a generalization of a Kripke frame. You can convert every Kripke frame into a neighborhood frame by making the neighborhoods of each world exactly the truth sets of all $\varphi$ that are necessitated by that world.

However, you can’t go in reverse, because having different neighborhoods attached to the same world means that criterions for necessity can be different for each $\varphi .$ For instance, $◻\varphi$ might be satisfied by a neighborhood $U$ which is disjoint from a neighborhood $V$ which satisfied $◻\psi .$ This is not representable in Kripke models—there’s only one neighborhood for each world.

You can pretty easily construct a world with neighborhood semantics that doesn’t satisfy $\mathbf{K}.$ Or mainly, the neighborhood associated with $◻(A\to B)$ doesn’t have to be the same one associated with $◻A,$ and then as a result this correspondence no longer holds in generality.

Applications to Mathematical Reality

Ok, so why were Kripke semantics useful in the first place? They provided a very clean structure by which they could model logics in a way that allowed one to verify properties like completeness/consistency/decidability well (all Kripke models are just graphs, in essence). Partially this is because they have some formal grounding in set theory. But also because formalizing logical structures as directed graphs is just really powerful and a really useful abstraction to reason about various systems.

In the same vein, reducing other systems to neighborhood semantics allows you to reason about their relevant properties simply and somewhat easily. Intuitively, we have a lot of structures that deal with collections of sets cough topologies cough and it’d be nice to bring some of them to the study of modal logic.

Then there’s the question of what modal logics can simulate. Games feature prominently. Provability logic is quite famous. But more generally, modal logics are ways of modeling systems and structures that allow you to abstract away a bunch of irrelevant features.

(They’re also all fragments of FOL (first-order-logic), and as a result don’t necessarily have the same trials and tribulations that come with additional complexity)