The fan theorem is one of the basic principles of intuitionism that make it more specific (even in mathematical practice, independent of any philosophical issues) than garden-variety constructive mathematics. Its main use is to justify pointwise analysis; without it, one really needs locale theory instead. In classical mathematics, the fan theorem is true.
Let be a collection of finite sequences of bits, that is a subset of the free monoid on the boolean domain. Given an infinite sequence and a natural number , we say that -bars if ; given only , we say that bars if -bars for some .
We are interested in these three properties of :
A bar is a barred subset .
Every decidable bar is uniform.
Although the fan theorem is about bars, it is different from the bar theorem?, which is related but stronger.
Let be the set of binary digits (bits) and the set of natural numbers (numbers). Given a set , let be the set of finite sequences of elements of , let be the set of infinite sequences of elements of , and let be the set of decidable subsets of . Then the fan theorem is about (elements of) , , and .
However, the sets , , and are all isomorphic. Similarly, the sets , , , and are all isomorphic. In much of the literature on bars, one tacitly uses all of these isomorphisms, taking and as chosen representatives of their isomorphism classes. Thus, everything in sight is either a natural number or an infinite sequence of bits.
The fan theorem is hard enough to understand when is an infinite sequence of bits and is a finite sequence of bits; it is even harder to understand when is a natural number that bears no immediate relationship to the digits in the sequence .
The fan theorem may be stated about all bars, not just the decidable ones. Brouwer himself at one point claimed that it held for all bars, but later Kleene showed that this contradicted Brouwer's continuity theorem?. However, the theorem does hold for all bars classically.
In classical mathematics, the fan theorem is simply true.
In constructive mathematics, the fan theorem is equivalent to any and all of the following statements: * As a locale, Cantor space has enough points (is topological). * As a topological space, Cantor space is compact. * As a topological space, the (located Dedekind) unit interval is compact (the Heine–Borel theorem). * As a topological space, the (located Dedekind) real line is locally compact. * Every uniformly continuous function from Cantor space to the metric space of positive real numbers has a positive lower bound. * Every uniformly continuous function from the unit interval to has a positive lower bound. * There exists a class of “kontinuous” partial functions from the set of (located Dedekind) real numbers to itself (see Waaldijk) such that * the restriction of a kontinuous function to any smaller domain is kontinuous; * the identity function on is kontinuous; * the composite of two kontinuous functions is kontinuous; * a function whose domain is the unit interval is kontinuous if and only if it is uniformly continuous (in the usual metric-space sense); and * the function defined on is kontinuous.
It follows from any of these statements: * The bar theorem? holds. * As a locale, Baire space has enough points. * Every pointwise-continuous function on Cantor space is uniformly continuous. * Every pointwise-continuous function on the unit interval is uniformly continuous.
I need to figure out how it relates to the various versions of König's Lemma?, as well as these statements (which are mutually equivalent): * As a locale, the unit interval has enough points. * As a locale, the real line (the locale of real numbers) has enough points.
Some of the results above may use countable choice, but probably no more than (which is choice for relations between and itself).
Point-wise real analysis without the fan theorem is very difficult, as the example from Waaldijk shows. This was Brouwer's motivation for introducing the fan theorem. But if you use locales (or other pointless approaches), then you don't need the fan theorem (or bar theorem).
Fourman and Hyland provide a sheaf model not satisfying the fan theorem.
I need to read the relevant parts here:
More links that I need to keep in mind: