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