<p>Perhaps relevant are <strong>term-modal logics</strong>.</p>

<p>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. <span class="math-container">$\exists x K_x \varphi(x)$</span> a well-formed formula.</p>

<p>You can find a recent review of the literature in this paper: <a href="https://arxiv.org/abs/1906.06047" rel="noreferrer">https://arxiv.org/abs/1906.06047</a></p>

CC BY-SA 4.0
2020-04-15T09:54:26.270Z
2020-04-15T09:54:26.270Z
Rasmus
<p>In topos theory there are modal operators known as the <a href="https://ncatlab.org/nlab/show/Lawvere-Tierney+topology" rel="noreferrer">Lawvere-Tierney operators</a>. 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.</p>

<p>A related idea is the frame (or locale) of <a href="https://ncatlab.org/nlab/show/nucleus" rel="noreferrer">nuclei</a>. If we think of a frame as a kind of logic (<a href="https://ncatlab.org/nlab/show/geometric+logic" rel="noreferrer">geometric logic</a>, to be precise) then a nucleus is a modal operator on it. Once again, the nuclei of a frame themselves form a frame.</p>

CC BY-SA 4.0
2020-04-16T19:25:55.790Z
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
CC BY-SA 4.0
2020-04-17T06:41:45.217Z
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
CC BY-SA 4.0
2018-09-09T08:19:47.977Z
2018-09-09T08:24:48.263Z
2018-09-09T08:24:48.263Z
Andrej Bauer
<p>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.</p>

<lo.logic><modal-logic>
Multimodal logic with quantification over modal operators
Y.Z.
# Multimodal logic with quantification over modal operators

(Asked by: username_0 on 2018-09-09)

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.

**Tags:** lo.logic, modal-logic


---

## 2 answers

### Answer by username_2 on 2018-09-09. Score: 7 | Accepted answer

In topos theory there are modal operators known as the [Lawvere-Tierney operators](https://ncatlab.org/nlab/show/Lawvere-Tierney+topology). 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](https://ncatlab.org/nlab/show/nucleus). If we think of a frame as a kind of logic ([geometric logic](https://ncatlab.org/nlab/show/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.

> **Comments:**
> **username_3**: 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?  
> **username_2**: Yes it is, I am pretty sure you can find this in the MacLane & Moerdijk book, and of course also somewhere in the Elephant.  

---

### Answer by username_1 on 2020-04-15. Score: 5

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>


---

