I take a multimodal logic to be a logic with multiple (potentially infinitely many) primitive modal operators. I am curious if anyone has studied a logic that allows one to quantify over the modal operators themselves. Intuitively, if we think of $\langle R\rangle \varphi$ as $\varphi$ by doing $R$ (where $R$ is a program), then it should make sense to want to say ``$\varphi$ by doing something,'' hence the thought of quantifying over modal operators.


In topos theory there are modal operators known as the Lawvere-Tierney operators. Such an operator is a certain endomorphism $j : \Omega \to \Omega$ on the subobject classifier. The object $J$ of all such operators is definable in the internal language of the topos, and so we can quantify over all $j$'s. My topos-theoretic knowledge is too poor to know whether anyone has done anything interesting with the object of all $j$-operators.

A related idea is the frame (or locale) of nuclei. If we think of a frame as a kind of logic (geometric logic, to be precise) then a nucleus is a modal operator on it. Once again, the nuclei of a frame themselves form a frame.

  • $\begingroup$ It's slightly speculative but I wonder if there's a Galois-theory result characterizing automorphisms of $J$ in relation to (2-category) of subtopoi? Up to equivalence, isn't every such subtopos determined by a Lawvere-Tierney topology? $\endgroup$ – Daniel Gratzer Apr 16 '20 at 19:25
  • $\begingroup$ Yes it is, I am pretty sure you can find this in the MacLane & Moerdijk book, and of course also somewhere in the Elephant. $\endgroup$ – Andrej Bauer Apr 17 '20 at 6:41

Perhaps relevant are term-modal logics.

Term-modal logics are a family of qunatified modal logics in which the subscript of the modal operators are terms of a first-order language mkaing e.g. $\exists x K_x \varphi(x)$ a well-formed formula.

You can find a recent review of the literature in this paper: https://arxiv.org/abs/1906.06047


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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