I am looking for ways to internalize the modal operator of necessity $\Box$, ending up with a morphism $\Box: \Omega \to \Omega$ satisfying the necessitation rule (if $\phi$, then $\Box \phi$) and the distributive under implication $(\Box(\phi \to \psi)\to (\Box \phi \to \Box \psi))$. The reason why is I would like to study categories in which their internal logic, instead of classical ($\Omega$ is a Boolean algebra) or intuitionistic ($\Omega$ is a Heyting algebra), are modal logics, satisfying specifics modal axioms. However, seems like it is a little bit trick to define categorical versions of modal operators.
In the paper Topos Theoretic Approaches to Modality by Reyes and Zolfaghary, they say
''There is a fundamental difference between modal operators in a topos such as $\Box$ (necessity) and other logical operators such as $\neg$ (negation): while $\neg$, is functorial in the sense that it commutes with pull-backs (and hence it defines a map $\neg: \Omega \to \Omega$), this is not so for $\Box$. Indeed, the only operator $\Box: \Omega \to \Omega$ such that $\Box p \subseteq p$ and $\Box T = T$ is the identity''
Then, they define modal operators in the image of a subobject classifier by a geometric morphism.
There are also other constructs, like in the paper Elementary Axioms for Local Maps of Toposes by Awodey and Birkedal, where they notice that the internal logic for local maps could be viewed as the modal logic $S_{4}$.
I would be glad if someone could explain in more detail why it is not possible to define modalities $(\Box,\Diamond)$ internally in a topos, using its subobject classifier.
Many thanks.
Best Answer
As said in the comment, I'm not sure what to add to the paragraph, the point is that in a topos there is no functions $\Omega \to \Omega$ that has the property expected of a neccessity operator except the identity.
$\newcommand\true{\mathrm{true}}\newcommand\false{\mathrm{false}}$If I can give an intuitive explanation the idea is that if you only have two truth values "$\true$" and "$\false$", then you don't really have a choice, you need to define $\square\true = \true$ and $\square\false = \false$.
Now in a topos, you get in a sense more truth value, collected in the object $\Omega$, but to some extent the internal logic doesn't fully agree that you have more than two truth value: for example the following statement is always internally true
$$ \forall x \in \Omega, (x \neq \true) \Rightarrow x = \false $$
(which of course cannot be rewritten as "$x = \false$ or $x = \true$" as we don't have the law of excluded middle).
And it happens that this sort of thing is actually enough to prevent having an "internal" necessity operator.
An internal proof that there is no such operator looks like:
Let $\square : \Omega \to \Omega$ be a function such that $\square\true = \true$ and $\forall x \in \Omega, \square x \leqslant x$. Let $x \in \Omega$. Assume $x$ is true, them $\square x = \square\true = \true$, i.e. if $x$ then $\square x$. So we have proved that $x \Rightarrow \square x$. As we are also assuming $\square x \leqslant x$, this shows that $\square x = x$.