3
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$

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.