The fan theorem

# The fan theorem

## Introduction

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 for point-free topology instead. In classical mathematics, the fan theorem is true.

## Statement

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

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

We are interested in these three properties of $B$:

• $B$ is decidable: For every finite sequence $u$, either $u \in B$ or $u \notin B$. (This is trivial in classical logic but will hold constructively only for some subsets $B$.)
• $B$ is barred: For every infinite sequence $\alpha$, $\alpha$ bars $B$.
• $B$ is uniform: For some natural number $M$, for every infinite sequence $\alpha$, if $\alpha$ bars $B$ at all, then $\alpha$ $n$-bars $B$ for some $n \leq M$.

A bar is a barred subset $B$.

###### Fan Theorem

Every decidable bar is uniform. (In other words, if a collection of bitlists is decidable and barred, then it is also uniform.)

Although the fan theorem is about bars, it is different from the bar theorem?, which is related but stronger.

### Obfuscation

Let $\mathbb{B}$ be the set $\{0,1\}$ of binary digits (bits) and $\mathbb{N}$ the set $\{0,1,2,\ldots\}$ of natural numbers (numbers). Given a set $A$, let $A^*$ be the set of finite sequences of elements of $A$, let $A^{\mathbb{N}}$ be the set of infinite sequences of elements of $A$, and let $\mathcal{P}_{\Delta}A$ be the set of decidable subsets of $A$. 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 $\bar \alpha n$ is a finite sequence of bits; it is even harder to understand when $\bar \alpha n$ is a natural number that bears no immediate relationship to the digits in the sequence $\alpha$.

### Variations

The fan theorem may be stated about all bars, not just the decidable ones: all bars are uniform (which is true in classical mathematics). Brouwer himself at one point claimed this, but later Kleene showed that this contradicted Brouwer's continuity theorem?.

Since decidability is classically trivial, we may call this the classical fan theorem.

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

• 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 $\dot{\mathbb{R}}^+$ of positive real numbers has a positive lower bound.
• Every uniformly continuous function from the unit interval to $\dot{\mathbb{R}}^+$ has a positive lower bound.
• (This item might need dependent choice in order to be equivalent to the others.) There exists a class of “kontinuous” partial functions from the set $\mathbb{R}$ 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 $\mathbb{R}$ 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 $(x \mapsto 1/x)$ defined on $\dot{\mathbb{R}}^+$ 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.
• Every uniformity (or indeed any metric) compatible with the usual topology of Cantor space is totally bounded.
• The property of being “complete and totally bounded”, i.e. Bishop-compact, is invariant under topological homemorphism between uniform (or metric) spaces.

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,0}$ (which is choice for relations between $\mathbb{N}$ and itself).

### Analysis without the fan theorem

Point-wise real analysis without the fan theorem is very difficult, as shown by the example above from Waaldijk regarding “kontinuous” functions: without the fan theorem there isn’t really even a good notion of continuity! This was Brouwer's motivation for introducing the fan theorem.

However, the fan theorem (and bar theorem) can be avoided by instead using locales or another point-free approach to analysis.

### Sheaf models

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

## Proofs

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

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:

Also: