Necessity

Let $H$ be a Heyting algebra equipped with a closure operator $j \colon H \to H$ (i.e., $j$ is extensive, monotone, and idempotent).

Definition. The necessity operator on $H$ is the map $\Box = j$. An element $a \in H$ is necessary if $j(a) = a$ (i.e., $a$ is $j$-closed). For any proposition $a \in H$, the element $j(a)$ is the necessitation of $a$ — the least necessary element above $a$.

In a Kripke model $(W, R, V)$, the semantic clause is:

Proposition. The set of necessary elements $H^j = \{a \in H : j(a) = a\}$ is closed under $\wedge$ and contains $\top$.

Proof sketch. $j(\top) = \top$ by extensiveness and $\top$ being greatest. For $a, b \in H^j$: $j(a \wedge b) \leq j(a) \wedge j(b) = a \wedge b$ by monotonicity and the closure of $a, b$; the reverse follows from extensiveness. $\square$

Proposition. In classical modal logic (where $H$ is Boolean), $\Box a = \neg\Diamond\neg a$, where $\Diamond$ is the possibility operator. That is, $a$ is necessary iff $\neg a$ is not possible.

Proposition. If $j$ is additionally a nucleus (i.e., $j(a \wedge b) = j(a) \wedge j(b)$), then $H^j$ is a Heyting algebra with implication $a \Rightarrow_j b = j(a \to b)$.

Proof sketch. For $a, b, c \in H^j$: $c \leq j(a \to b)$ iff $c \leq a \to b$ (since $c$ is $j$-closed and $j$ is a nucleus) iff $a \wedge c \leq b$. $\square$

Examples.

• In a Kripke frame $(W, R)$ where $R$ is reflexive, $\Box\varphi \to \varphi$ is valid (the T axiom): truth at all accessible worlds includes the current world.
• In S5, where $R$ is an equivalence relation, $\Box\varphi$ holds at $w$ iff $\varphi$ holds throughout $w$’s equivalence class.
• On $\mathcal{O}(X)$ for a topological space, the identity is a trivial nucleus; every open set is “necessary.” A nontrivial Lawvere-Tierney topology $j$ on a topos gives a nontrivial modal system on the subobject classifier.