3
$\begingroup$

I would like to create a big list of Grothendieck topoi (or Grothendieck $\infty$-topoi) which do / do not satisfy the law of excluded middle. That is, let’s list some examples of topoi whose internal logic does / does not validate that inference rule

$$ \overline{P \vee \neg P}$$

IIRC, there is a subtle distinction between double-negation elimination and LEM, but that if we’re talking about the entire topos validating the inference rule, they are equivalent, so we are equivalently asking whether these topoi do / do not validate the inference rule

$$\overline{\neg \neg P \Rightarrow P}$$

So for example, $Set$ (or $Spaces$) does validate this rule, but beyond that I am very fuzzy:

  • Which presheaf topoi validate LEM?

  • The sheaf topoi on which topological spaces validate LEM?

  • $G$-sets for which (topological) groups validate LEM?

  • …

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ 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. $\endgroup$
    – Arshak Aivazian
    Commented Jun 18 at 21:18
  • 2
    $\begingroup$ 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). $\endgroup$
    – R. van Dobben de Bruyn
    Commented Jun 18 at 21:21
  • $\begingroup$ 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) $\endgroup$
    – Arshak Aivazian
    Commented Jun 18 at 21:24
  • $\begingroup$ I am confused, I thought that by HoTT 3.2.2. no ∞-topos satisfy LEM. $\endgroup$
    – Nikola Tomić
    Commented Jun 19 at 9:36
  • 4
    $\begingroup$ @NikolaTomić 3.2.2 disproves $\mathsf{LEM}_\infty$, but the proper version in section 3.4, which concerns only propositions, is consistent. $\endgroup$
    – Naïm Favier
    Commented Jun 19 at 9:39

0

Reset to default