fan theorem

The fan theorem


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.


Consider the finite and infinite sequences of binary digits. Given an infinite sequence α\alpha and a natural number nn, let α¯n\bar \alpha n be the finite sequence consisting of the first nn elements of α\alpha.

Let BB be a collection of finite sequences of bits, that is a subset of the free monoid on the boolean domain. Given an infinite sequence α\alpha and a natural number nn, we say that α\alpha nn-bars BB if α¯nB\bar \alpha n \in B; given only α\alpha, we say that α\alpha bars BB if α\alpha nn-bars BB for some nn.

We are interested in these three properties of BB:

  • BB is decidable: For every finite sequence uu, either uBu \in B or uBu \notin B. (This is trivial in classical logic but may hold constructively for a particular subset BB.)
  • BB is barred: For every infinite sequence α\alpha, α\alpha bars BB.
  • BB is uniform: For some natural number MM, for every infinite sequence α\alpha, if α\alpha bars BB at all, then α\alpha nn-bars BB for some nMn \leq M.

A bar is a barred subset BB.

Fan Theorem

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 𝔹\mathbb{B} be the set {0,1}\{0,1\} of binary digits (bits) and \mathbb{N} the set {0,1,2,}\{0,1,2,\ldots\} of natural numbers (numbers). Given a set AA, let A *A^* be the set of finite sequences of elements of AA, let A A^{\mathbb{N}} be the set of infinite sequences of elements of AA, and let 𝒫 ΔA\mathcal{P}_{\Delta}A be the set of decidable subsets of AA. Then the fan theorem is about (elements of) 𝔹 *\mathbb{B}^*, 𝔹 \mathbb{B}^{\mathbb{N}}, and 𝒫 Δ𝔹 *\mathcal{P}_{\Delta}\mathbb{B}^*.

However, the sets \mathbb{N}, 𝔹 *\mathbb{B}^*, and *\mathbb{N}^* are all isomorphic. Similarly, the sets 𝔹 \mathbb{B}^{\mathbb{N}}, 𝒫 Δ\mathcal{P}_{\Delta}\mathbb{N}, 𝒫 Δ𝔹 *\mathcal{P}_{\Delta}\mathbb{B}^*, and 𝒫 Δ *\mathcal{P}_{\Delta}\mathbb{N}^* are all isomorphic. In much of the literature on bars, one tacitly uses all of these isomorphisms, taking \mathbb{N} and 𝔹 \mathbb{B}^{\mathbb{N}} 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 α\alpha is an infinite sequence of bits and α¯n\bar \alpha n is a finite sequence of bits; it is even harder to understand when α¯n\bar \alpha n is a natural number that bears no immediate relationship to the digits in the sequence α\alpha.


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.

Use in analysis

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:

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):

Some of the results above may use countable choice, but probably no more than AC 0,0AC_{0,0} (which is choice for relations between \mathbb{N} and itself).

Uselessness in analysis

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).


I should write down the classical proof (which uses excluded middle and some form of dependent choice), as well as Brouwer's argument.

Sheaf models

Fourman and Hyland provide a sheaf model not satisfying the fan theorem.


I need to read the relevant parts here:

  • Mike Fourman, R. Grayson, Formal Spaces. In: The L.E.J. Brouwer Centenary Symposium, A.S. Troelstra and D. van Dalen, eds. North Holland (1982), pp. 107–122.

More links that I need to keep in mind:

Revised on November 11, 2014 09:45:18 by Thomas Holder (