5
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ Could you clarify what is $p$, please? $\endgroup$
    – Todd Trimble
    Commented Apr 9 at 20:53
  • 2
    $\begingroup$ I feel like the fact mentioned in the cited paragraph that there is no operator with these two properties answer the question. So, are you asking for a proof of that fact? or are you not convinced that this fact answer your question? $\endgroup$ Commented Apr 9 at 21:19
  • 2
    $\begingroup$ @ToddTrimble Given the context, my understanding is that p is a variable of type $\Omega$ and this is an internal statement. That is this is the assumption that $(\square,id): \Omega \to \Omega^2$ factor through the order relation. $\endgroup$ Commented Apr 9 at 21:34
  • 2
    $\begingroup$ A formal answer to your question has already been given by Simon Henry. But let me make the following more informal remark: even just classically, the whole point of modal operators is that they give rise to a semantic of “possible worlds” (Kripke semantics) where the truth value differs from one world to another: so the whole point of $\Box$ is that the truth value of $\Box p$ doesn't just depend on the truth value of $p$. As such, it is unreasonable to try to make $\Box$ into a function from the object $\Omega$ of truth value to itself. $\endgroup$
    – Gro-Tsen
    Commented Apr 10 at 15:42
  • 2
    $\begingroup$ (My previous comment should be taken cum grano salis, however, because a Lawvere-Tierney topology (=local operator) $j\colon\Omega\to\Omega$ certainly behaves as a sort of modal operator (whose meaning is something like “locally”), and by definition it makes sense at the truth-value level.) $\endgroup$
    – Gro-Tsen
    Commented Apr 10 at 15:46

1 Answer 1

11
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ Thank you so much for your answer! It is more clear now! However, why do we need to assume that for all $x \in \Omega, \Box x \leq x$? $\endgroup$
    – Miviska
    Commented Apr 10 at 21:24
  • 2
    $\begingroup$ I'm not really an expert on all the form of Modal logic that exists so I can't really comment on that beyond "that's the kind of property a Neccessity operator is generally required to satisfies" if your modality operator don't satisfies that, maybe you should give it another name. I can't give you a blanket statement that no kind of modality operator is definable : as Mentioned by Gro-tsen Lawvere Tierney Topologies are something we may want to think as a modal operator and are perfectly fine and interesting internally in toposes. The sort of thing people in HoTT call modalities are also[...] $\endgroup$ Commented Apr 10 at 22:31
  • 2
    $\begingroup$ [...] fine, but the kind of operator like the necessity and possibility that people doing modal logic are interested in aren't - at least not with this kind of naive interpretation. $\endgroup$ Commented Apr 10 at 22:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.