# Multimodal logic with quantification over modal operators

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.

• 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? – Daniel Gratzer Apr 16 '20 at 19:25
• Yes it is, I am pretty sure you can find this in the MacLane & Moerdijk book, and of course also somewhere in the Elephant. – 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