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
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 14 at 14:28 | vote | accept | Miviska | ||
| Apr 10 at 15:46 | comment | added | Gro-Tsen | (My previous comment should be taken cum grano salis, however, because a Lawvere-Tierney topology (=local operator) $j\colon\Omega\to\Omega$ certainly behaves as a sort of modal operator (whose meaning is something like “locally”), and by definition it makes sense at the truth-value level.) | |
| Apr 10 at 15:42 | comment | added | Gro-Tsen | A formal answer to your question has already been given by Simon Henry. But let me make the following more informal remark: even just classically, the whole point of modal operators is that they give rise to a semantic of “possible worlds” (Kripke semantics) where the truth value differs from one world to another: so the whole point of $\Box$ is that the truth value of $\Box p$ doesn't just depend on the truth value of $p$. As such, it is unreasonable to try to make $\Box$ into a function from the object $\Omega$ of truth value to itself. | |
| Apr 10 at 14:31 | answer | added | Simon Henry | timeline score: 11 | |
| Apr 9 at 22:00 | comment | added | Todd Trimble | @SimonHenry Thanks. That sounds right to me. | |
| Apr 9 at 21:34 | comment | added | Simon Henry | @ToddTrimble Given the context, my understanding is that p is a variable of type $\Omega$ and this is an internal statement. That is this is the assumption that $(\square,id): \Omega \to \Omega^2$ factor through the order relation. | |
| Apr 9 at 21:19 | comment | added | Simon Henry | I feel like the fact mentioned in the cited paragraph that there is no operator with these two properties answer the question. So, are you asking for a proof of that fact? or are you not convinced that this fact answer your question? | |
| Apr 9 at 20:53 | comment | added | Todd Trimble | Could you clarify what is $p$, please? | |
| S Apr 9 at 20:45 | review | First questions | |||
| Apr 9 at 21:24 | |||||
| S Apr 9 at 20:45 | history | asked | Miviska | CC BY-SA 4.0 |