Timeline for Examples of Grothendieck ($\infty$-)topoi which do / do not satisfy the law of excluded middle
Current License: CC BY-SA 4.0
Post Revisions
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 19, 2024 at 9:39 | comment | added | Naïm Camille Favier | @NikolaTomić 3.2.2 disproves $\mathsf{LEM}_\infty$, but the proper version in section 3.4, which concerns only propositions, is consistent. | |
| Jun 19, 2024 at 9:36 | comment | added | Nikola Tomić | I am confused, I thought that by HoTT 3.2.2. no ∞-topos satisfy LEM. | |
| Jun 18, 2024 at 21:24 | comment | added | Arshak Aivazian | Also, geometric gros topoi are not Boolean (if there were an excluded middle, then mappings of spaces could be defined piecewise: on a subspace cut out by some condition and its complement) | |
| Jun 18, 2024 at 21:21 | comment | added | R. van Dobben de Bruyn | These are exactly the Boolean topoi, see for instance MacLane–Moerdijk, Chapter VI, §1, Proposition 1 and equation (15) in Chapter VI, §6. Since this is a property of the lattice of opens, it only depends on the 0-localic reflection (I suspect the same should be true for $\infty$-topoi, but I don't know the 'logic' interpretation of higher topoi that well). | |
| Jun 18, 2024 at 21:18 | comment | added | Arshak Aivazian | These are called Boolean topoi. The topoi of presheaves are typically not Boolean. Exception: presheaves on groupoids. The topos of sheaves on a topological space is Boolean if and only if its T_0-fication is a discrete space. | |
| Jun 18, 2024 at 20:48 | history | made wiki | Post Made Community Wiki by Tim Campion | ||
| Jun 18, 2024 at 20:48 | history | asked | Tim Campion | CC BY-SA 4.0 |