A separation result for varieties of Brouwer's fan theorem
Josef Berger · 2009
We recall the axioms FAN, c- FAN, and Π01-FAN, which are ver-sions of Brouwer’s fan theorem. It is easy to see that Π01-FAN implies c- FAN and that c- FAN implies FAN. We show that, in general, FAN does not imply c- FAN. We start with the description of a formal system FS. The language of FS contains variables for natural numbers n,m ∈ N, for finite sequences of natural numbers u, v, w ∈ {0, 1} ∗ (we write u = (u(0),..., u(n − 1)) to denote the components), and for infinite binary sequences α, β ∈ {0, 1}N. Furthermore, we assume the existence of bijections θ: N × N → N and η: N → {0, 1}∗. With the help of θ, we can define functions from N × N into {0, 1}, whereas η allows us to identify N with {0, 1}∗. The system is based on intuitionistic predicate logic. Furthermore, it contains the defining axioms of the following functions: • u 7 → |u|, the length of u ∈ {0, 1}∗;