Fan Theorem

Definition

Let $2^{\ast }$ be the set of finite binary sequences and $2^{\mathbb{N}}$ the Cantor space of infinite binary sequences. A subset $B\subseteq 2^{\ast }$ is a bar if for every $\alpha \in 2^{\mathbb{N}}$, there exists a finite initial segment $\alpha [n]\in B$. A bar $B$ is uniform if there exists $N\in \mathbb{N}$ such that every $\sigma \in 2^{\ast }$ of length $N$ possesses an initial segment in $B$. The Fan Theorem states that every bar is uniform.

Context

Classically, this is equivalent to the compactness of Cantor space. In intuinistic mathematics, it is assumed as an axiom or derived from bar induction. It contradicts the Church-Turing thesis formulation in Russian constructive mathematics (Kleene’s tree).

References

• Brouwer, L. E. J. (1927). Über Definitionsbereiche von Funktionen.
• Troelstra, A. S., & van Dalen, D. (1988). Constructivism in Mathematics.
• Bishop, E. (1967). Foundations of Constructive Analysis.
• dummett2000-intuitionism