4
$\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$ Commented Jun 18, 2024 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$ Commented Jun 18, 2024 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$ Commented Jun 18, 2024 at 21:24
  • $\begingroup$ I am confused, I thought that by HoTT 3.2.2. no ∞-topos satisfy LEM. $\endgroup$ Commented Jun 19, 2024 at 9:36
  • 5
    $\begingroup$ @NikolaTomić 3.2.2 disproves $\mathsf{LEM}_\infty$, but the proper version in section 3.4, which concerns only propositions, is consistent. $\endgroup$ Commented Jun 19, 2024 at 9:39

0

Reset to default

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.