# 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.
• 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? Apr 16 '20 at 19:25
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.