Timeline for Why is it not possible to define the necessity operator internally $\Box: \Omega \to \Omega$ in a topos?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 12 at 12:45 | comment | added | მამუკა ჯიბლაძე | Even without assuming $\Box\mathrm{true}=\mathrm{true}$ - I believe Bénabou was first to observe that the only $\Box:\Omega\to\Omega$ satisfying $\Box x\leqslant x$ are of the form $x\land\Box\mathrm{true}$. Indeed for any $\Box$ whatsoever, from $x\Rightarrow(x=\mathrm{true})$ it follows $x\land\Box x=x\land\Box\mathrm{true}$, so that if $\Box x\leqslant x$ then $\Box x=x\land\Box\mathrm{true}$. | |
| Apr 14 at 14:28 | vote | accept | Miviska | ||
| Apr 10 at 22:32 | comment | added | Simon Henry | [...] fine, but the kind of operator like the necessity and possibility that people doing modal logic are interested in aren't - at least not with this kind of naive interpretation. | |
| Apr 10 at 22:31 | comment | added | Simon Henry | I'm not really an expert on all the form of Modal logic that exists so I can't really comment on that beyond "that's the kind of property a Neccessity operator is generally required to satisfies" if your modality operator don't satisfies that, maybe you should give it another name. I can't give you a blanket statement that no kind of modality operator is definable : as Mentioned by Gro-tsen Lawvere Tierney Topologies are something we may want to think as a modal operator and are perfectly fine and interesting internally in toposes. The sort of thing people in HoTT call modalities are also[...] | |
| Apr 10 at 21:24 | comment | added | Miviska | Thank you so much for your answer! It is more clear now! However, why do we need to assume that for all $x \in \Omega, \Box x \leq x$? | |
| Apr 10 at 19:37 | history | edited | LSpice | CC BY-SA 4.0 |
`\mathrm`
|
| Apr 10 at 15:35 | history | edited | Simon Henry | CC BY-SA 4.0 |
edited body
|
| Apr 10 at 14:31 | history | answered | Simon Henry | CC BY-SA 4.0 |