Vous consultezAbout Brouwer's fan theorem / THIERRY COQUAND / September 23, 2003

Introduction

The purpose of this short note is first to give a precise formulation of Brouwer's fan theorem, which highlights its philosophical interest. We use this formulation to give a somewhat surprising solution to a problem that arises in constructive mathematics when trying to describe topological spaces, such as Cantor space or the real line. Such a formulation is not new, but it seems to the author that it appears only implicitly in the available literature [1] [1] It was directly suggtested by the intuitionistic analysis...
suite. The fan theorem arises from Brouwer's attempt to analyse constructively the continuum. As shown in this note, this purely mathematical problem is connected to philosophical dichotomies such as continuum/discrete, actual/potential but also non-determinism/determinism.

1) Brouwer's fan theorem

2 The binary tree is the set of all finite binary sequences, that is finite sequences of 0 or 1. For instance, 001 or 1011 are such sequences. We denote by () the empty sequence and use a, r, ... as variables for such sequences. One can think of the set of all such sequences as a tree. Such objects, finite, are not problematic constructively. What is more problematic is the notion of an infinite branch in such a tree. One preliminary way to think of such a sequence is a function N —> {0,1}, where function is understood constructively, as in Bishop's book [2]. We shall see however that there is a problem with such an interpretation. We use a, (3, ... as variables for such infinite sequences. It will be useful for the discussion to use some terminology from topology. The "set" of all infinite sequences is called the Cantor space, and each finite sequence cr represents canonically a basic open Ua of the space, which can be thought of as the set of all infinite sequences which extend a. Our aim is to describe the structure of this space in a purely phenomenological way, using obly finite objects.

3 If a is an infinite sequence and n e N we denote by a(n) the finite sequence a(0) ... a(n - 1). Thus5(0) is the empty sequence (), and if n is the lenght of a, the basic open Ua is the "set" of all sequences a such that a(n)=a. We write &  a to express that the finite sequence & extends the sequence a. Clearly o' C a holds iff Uai C Ua.

4 Consider now a set V of finite sequences that satisfies the condition that if a e V then &0 e V and al e V and more generally a' e V whenever cr' C a We want to say that V is a bar iff the union of all Ua, a e V is a covering of Cantor space, that is all infinite sequences belong to at least one of the sets Ua. Brouwer's fan theorem is concerned with analysing constructively this notion of covering. We can write

and interpret the concept of bar as follows : whenever we make a sequence of successive choices

eventually we shall get a number n such that a(ji) and then all values aim) for m >n are in V.

5 For instance, let VQ be the set of finite sequences extending 1 or 00 or 010 or Oil. It is clear that V0 is a bar : if «(0)=1 we can take n= 1, otherwise a(0)= 0 and if a(l)=0 we can take n=2 and otherwise n= 3. We get a picture of the form.

6 We can now state the fan theorem[2] [2] This implication clearly holds non constructively : since...
suite.

2) Kleene's counter-example

7 If we combine (*) and (**) we get the implication

The contraposite statement

also known as Konig's lemma, is provable classically. Let indeed AT be the set of sequence o such that there are arbitrary long sequences extending a not in V. The hypothesis tells us that () £ K. Also, classically, if a £ K then crO £ K or cl £ K.In this way, we can build a sequence a(0)a(l)a(2)...

8 such thata(n) e K for all n and in particulara(n) £ Vfor all n. Thus classically, the version (***), as well as (**), are provable. Notice however that this reasoning does not tell us any way to compute any appropriate N from the hypothesis that V is a bar.

9 The surprise is that this implication (***) does not hold constructively, if we interpret the universal quantification in

as quantifying only over computable functions a. More precisely, Kleene [3] defined explicitely a decidable subset V such that we can fid arbitrary long finite sequences not in V but such that, for any computable function a there is n such that a(ji) £ V.

10 This can be interpreted in the following way : in constructive mathematics, such as developed by Bishop, there is no hope to be able to prove the fan theorem, is we accept the identification (*). Indeed, Bishop's mathematics can be interpreted in a recursive way, identifying the notion of function with the notion of computable functions.

11 This is surprising, since Brouwer held the implication (**) to be valid, implying in some way that it should be possible to compute N from the hypothesis that V is a bar.

12 It is tempting to interpret further this unprovability result as follows.

13 The equivalence (*) is problematic constructively because when we say that V is a bar, we want to express that for whatever sequence of successive choices a(0)a(l)a(2)...

14 eventually we shall get a number n such that a(n), but we do not want to restrict this sequence of choices to one given by a law. This sequence may be obtained for instance by tossing a coin.

15 The problem now is the following : is there a way to capture constructively this idea of quantifying over all possible sequence, not necessarily given by a law ?

3) Analysis of "eventually"

16 Let us define inductively the predicate Va. There are two inductive clauses

1. if <T£ Vthen v|crand (2) if v|o0 and v|crl then va

17 We say that V is an inductive bar iff V(). We consider this to be the precise intuitionistic definition of what it means that if we make successive choices a(0)a(l)a(2)...

18 then eventually we have a(n) e V.

19 Notice that the clauses (1) and (2) only talk about finite sequences.

20 For instance, the following is a derivation showing that V0 is an inductive ba

r

21 The solution of our problem is now to take the (classically valid) equivalence

as a definition of what it means for V to be a bar. This may seem a surprising solution. Its justification is then to check that our proposed rigourous definition V0|() of an intuitive, somewhat vague, notion satisfies the expected properties of the intuitive notion. This is perfectly similar to the Cauchy-Weierstrass s8 analysis of the notion of continuity in finite terms instead of using infinitesimals.

4) A proof of the fan theorem

22 As a simple example of our analysis, let us give a proof of Brouwer's fan theorem. The main point is to assume V to be an inductive bar. We thus have a proof of VJ(). This proof can be thought of as a finitely branching tree. Let N be the height of this tree. It is then clear that we have

which is the desired conclusion of the fan theorem.

23 This example is paradigmatic : by replacing systematically the intuitive notion of bar by the notion of inductive bar, we can now prove Brouwer's fan theorem. More generally, we can think of V() as the correct format expression of a universal quantification over all sequences, not necessarily given by a law.

Conclusion

24 Brouwer's analysis of the notion of bar has clearly some analogy with the Cauchy-Weierstrass sS analysis of the notion of continuity. In both cases, an intuitive, somewhat vague notion is captured by a formally precise definition for which one can prove in a rigourous way the expected properties. The main interest however, I believe, is to show the way towards a purely phenomenological description of topological spaces such as Cantor space or the interval [0,1].

Appendix : brouwer's bar theorem

25 This section contains a technically more involved result. Brouwer formulated a more general theorem, which concerns the notion of arbitrary choice sequence of natural numbers (not necessarily restricted to 0 or 1). The collection of all these sequences is known in mathematics as the Baire space. Here also, each finite sequence crcan be thought of as the set of all infinite sequences which extend o. We consider a set V of finite sequences such that o' e ^ whenever a £ Vand cr'C c. The predicate Va is now logically more complex :

1. if a e Vfhen V|crand
2. if V| an for all integer n then v|o

26 The complexity of this definition is reflected in the universal quantification over all natural numbers. Brouwer's bar theorem states then that V is a bar, i.e.

27 if and only if v().

28 It is clear that the fan theorem is a consequence of the bar theorem.

29 A point, which is not often stressed enough in presentations of these two results, is that both theorems, the fan theorem and the bar theorem, are compatible with classical logic [3] [3] This is to be contrasted with some continuity principles...
suite.

30 The analysis of these principles that we present has the advantage to suggest at least the plausibility of technical results :

• the conservativity of the formulation (***) of the fan theorem over arithmetic [6] and hence by analogy, the conservativity of some formulation of Konig's lemma over arithmetic [5]). This is expected to hold since one can explain the fan theorem using only finitary inductive definitions, that can be explained in arithmetic. Similarly, the bar theorem is conservative over the logic of one generalised induetive definition [1], since we can give an explanation of this principle in this logic.
• the implication
  

31 though not provable, is admissible, that is, whenever we can prove the hypothesis, we can prove the conclusion. For this, it is enough to use that if a statement is provable intuitionistically, it should hold over any Beth model, and to look at the meaning of the hypothesis in a suitable Beth model defined from Cantor space. A similar analysis is possible for the bar theorem and Baire space.

Bibliographie

References

[1] ACZEL, P. An introduction to inductive definitions, in Handbook of mathematical logic. Edited by Jon Barwise, North-Holland Publishing Co., pp. 739-782,1977.

[2] BISHOP, E. Foundations of constructive analysis. McGraw-Hill Book Co., New York-Toronto, Ont.-London, 1967.

[3] KLEENE, S. C. and VESLEY, R. E. The foundations of intuitionistic mathematics, especially in relation to recursive functions. North-Holland Publishing Co., Amsterdam, 1965.

[4] MARTIN-LOF, P. Notes on constructive mathematics. Almqvist & Wiksell, Stockholm, 1970.

[5] SIMPSON, S.G. Subsystems of second order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1999.

[6] TROELSTRA, A. S. Note on the fan theorem. J. Symbolic Logic 39 (1974), 584-596.

Notes

[ 1] It was directly suggtested by the intuitionistic analysis of Cantor space presented in [4].

[ 2] This implication clearly holds non constructively : since Cantor space is compact, if the union of all U^ a e V is a covering, then already finitely many of them Ual, ... Uok will be a covering of Cantor space, and we can take for N the maximum of the lengths of (/al, ... Uak. The proof of Konig's lemma that we present below is a concrete version of this remark.

[ 3] This is to be contrasted with some continuity principles stated by Brouwer about infinite sequences that are incompatible with classical logic.

PLAN DE L'ARTICLE

• Introduction
• 1) Brouwer's fan theorem
• 2) Kleene's counter-example
• 3) Analysis of "eventually"
• 4) A proof of the fan theorem
• Conclusion
• Appendix : brouwer's bar theorem

« About Brouwer's fan theorem / THIERRY COQUAND / September 23, 2003 », Revue internationale de philosophie 4/2004 (n° 230), p. 483-489.
URL : www.cairn.info/revue-internationale-de-philosophie-2004-4-page-483.htm.