Modal Operator

Let $H$ be a Heyting algebra.

Definition. A modal operator on $H$ is a monotone map $\square \colon H \to H$ satisfying additional axioms that depend on the intended modality. The two fundamental modal operators are:

1. A necessity operator ($\Box$): a closure operator on $H$, i.e., a map $\Box \colon H \to H$ satisfying

   • $a \leq \Box a$ (extensive),
   • $a \leq b \Rightarrow \Box a \leq \Box b$ (monotone),
   • $\Box\Box a = \Box a$ (idempotent).

2. A possibility operator ($\Diamond$): an interior operator on $H$, i.e., the order-dual of a closure operator, satisfying $\Diamond a \leq a$, monotonicity, and $\Diamond\Diamond a = \Diamond a$.

In classical modal logic (where $H$ is Boolean), $\Box$ and $\Diamond$ are interdefinable: $\Box a = \neg\Diamond\neg a$ and $\Diamond a = \neg\Box\neg a$.

Proposition. If $\Box$ is a closure operator on $H$, then $H^{\Box} = \{a \in H : \Box a = a\}$ is a sub-meet-semilattice of $H$ containing $\top$.

Proof sketch. $\Box\top = \top$ by extensiveness and $\top$ being greatest. For $a, b \in H^{\Box}$, monotonicity gives $\Box(a \wedge b) \leq \Box a \wedge \Box b = a \wedge b$, and extensiveness gives the reverse inequality. $\square$

Proposition. In Kripke semantics, the operator $\Box_R(S) = \{w \in W : \forall v\,(wRv \Rightarrow v \in S)\}$ on $\mathcal{P}(W)$ preserves finite meets: $\Box_R(S \cap T) = \Box_R(S) \cap \Box_R(T)$ and $\Box_R(W) = W$.

Proof sketch. Direct from the universal quantification in the definition. $\square$

Examples.

• On a Boolean algebra, any normal modal operator satisfies $\Box(a \wedge b) = \Box a \wedge \Box b$ and $\Box\top = \top$ (the K axioms). Additional axioms (T, 4, 5) correspond to reflexivity, transitivity, and euclideanness of the underlying accessibility relation.
• On $\mathcal{O}(X)$ for a topological space $X$, the identity is a closure operator (trivial modality). A Lawvere-Tierney topology $j \colon \Omega \to \Omega$ in a topos gives a nontrivial modal operator on the subobject classifier.
• In intuitionistic modal logic, the duality $\Diamond a = \neg\Box\neg a$ fails precisely when $H$ is non-Boolean: in a non-Boolean Heyting algebra, $\neg$ is not an involution, so $\neg\Box\neg a \neq \Diamond a$ in general. The duality holds iff $H$ is Boolean.