8
$\begingroup$

Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable product of spaces, it can be viewed as a countable choice axiom in its own right. However, general elementary topoi satisfy very few choice principles and the effective topos famously does not satisfy the fan theorem.

The fan theorem is a well known foundational result in constructive analysis, and continuous functions on the set of reals are allowed to have very pathological behaviours if it is not assumed, which is a symptom of the fact that the locale of real numbers cannot be proven to be spatial.

For which sheaf topoi is the fan theorem true?

(I am also interested in results on other related theorems like the bar theorem and especially the principle of open induction on the Dedekind reals, which are slightly stronger. I mostly care about sheaves on compact Hausdorff spaces and about smooth sets)

$\endgroup$
2
  • $\begingroup$ It's not enough to have dependent choice. DC holds in the effective topos, but the Fan theorem does not, but the "Kleene tree" argument. $\endgroup$
    – aws
    Nov 24, 2022 at 17:58
  • $\begingroup$ @aws Thank you. I'll just shorten that paragraph. $\endgroup$
    – saolof
    Nov 24, 2022 at 18:25

1 Answer 1

7
$\begingroup$

The classic 1979 paper Fourman & Hyland, Sheaf models for analysis, has a number of results along these lines. They show in particular in Theorem 3.2 that every spatial topos, i.e. topos of sheaves on a topological space, satisfies the Fan Theorem.

$\endgroup$
3
  • $\begingroup$ Somewhat related question (at least to the extent that this reply is also relevant to that question). $\endgroup$
    – Gro-Tsen
    Nov 24, 2022 at 18:52
  • 1
    $\begingroup$ This was really helpful. Having a wealth of models definitely makes me value the fan theorem a lot more. Also, for locally countably compact spaces, the provided reference states in theorem 3.4 that Bar induction holds. He states a bunch of other criteria for bar induction as well. $\endgroup$
    – saolof
    Nov 24, 2022 at 21:46
  • $\begingroup$ (And that Sh(Q) fails bar induction where Q is the rationals with the usual topology. So while the fan theorem holds for all spatial topoi, Bar induction does not) $\endgroup$
    – saolof
    Nov 24, 2022 at 21:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.