# Brouwer's Fan Theorem

I am not a mathematician, but I really would like to understand/know the following:

What is so special about Brouwer's "Fan Theorem"? Is there an easy to undestand proof somewhere? Why was Brouwer apparently so obsessed with the "Fan Theorem"?

-
Somehow I cannot comment the answers on my question - I guess because I was not registered before. So, thanks for the answers. What I do not understand however is the exact meaning of your statement "Brouwer's proof of the fan theorem was (IIRC) via introspection about the possible methods of constructive proofs." This sounds like a metamathematical kind of proof-method (?) of which I thought there are no in intuitionistic mathematics. Also, my question why Brouwer was apparently "obsessed" with the theorem was not really answered. He seemed to be dissatisfied with his own proofs of the theore –  corto Jun 15 '11 at 8:58
your accounts have been merged. You should be able to comment normally now that you're using a registered account. –  Qiaochu Yuan Jun 15 '11 at 9:45

Brouwer's fan theorem is important because:

1. Constructivists including Brouwer have found it constructively acceptable, and
2. Informally, it is an expression of the compactness of the Cantor space $2^{\mathbb{N}}$, and when used as an axiom it can be used to establish results in mathematical analysis that require that sort of compactness.

The contrapositive of the fan theorem is known as Weak König's Lemma, and you can find a classical proof of that in many places (including Wikipedia).

However, Weak König's Lemma is not constructively valid, so a different justification is required for constructive mathematics. Brouwer's proof of the fan theorem was (IIRC) via introspection about the possible methods of constructive proofs. Brouwer later developed the notion of "bar induction" which can be used to prove the fan theorem.

In the past decade or so, the fan theorem and restrictions of it have occurred very often in constructive reverse mathematics, in a way that I find very analogous to the role of Weak König's Lemma in classical reverse mathematics.

Extension

Brouwer did accept some sorts of "metamathematical" proof methods, actually. He wasn't looking at formalized systems that could be analyzed metamathematically in the modern sense, but he was willing to reason about what he thought were all possible constructive proof methods. Unsurprisingly proofs of this sort were often unsatisfying, because constructive proof was not formalized and so was difficult to reason about. This is an integral part of his subjectivist philosophy of mathematics, though. As Douglas Bridges wrote [1],

Unfortunately — and perhaps inevitably, in the face of opposition from mathematicians of such stature as Hilbert — Brouwer's intuitionist school of mathematics and philosophy became more and more involved in what, at least to classical mathematicians, appeared to be quasi-mystical speculation about the nature of constructive thought, to the detriment of the practice of constructive mathematics itself.

This "speculation" is the "metamathematical" analysis we are talking about.

I don't know that Brouwer was obsessed with the fan theorem more than other things. But, to take his side for a moment, he was trying to develop an entirely new philosophy of mathematics, relying on subjective understanding of the content of proofs rather than on any reference to objective truth. It's natural that a project like that would require him to go back and revisit previous results, or to attempt to provide more solid justifications for principles that he felt should be acceptable but didn't feel he had properly justified yet.

-
Thanks for the answer. What I do not understand however is the exact meaning of your statement "Brouwer's proof of the fan theorem was (IIRC) via introspection about the possible methods of constructive proofs." This sounds like a metamathematical kind of proof-method (?) of which I thought there are no in intuitionistic mathematics. Also, my question why Brouwer was apparently "obsessed" with the theorem was not really answered. He seemed to be dissatisfied with his own proofs of the theorem, but it is not clear to me why. –  corto Jun 15 '11 at 10:37
@corto: I wrote a little more. –  Carl Mummert Jun 15 '11 at 11:30
What I can gather from Brouwer's writings is that he considered the fan theorem a cornerstone of the intuitionist's resurrection of mathematics. At the same time he seemed really dissatisfied with his proofs of this particular theorem. The impression I got from your answer (and from others) is that mathematicians nowadays don't consider the fan theorem "to be a big thing". This makes me wonder why Brouwer, who was a great mathematician, made such a fuss about it. –  corto Jun 15 '11 at 12:51
Also, I do not really understand, I guess because I lack the mathematical sophistication, whether Brouwer's problem is a technical, mathematical one or rather due to a kind of vague philosophical reluctance on his side. –  corto Jun 15 '11 at 13:00
The main difficulty for Brouwer and other constructivists is giving a motivation for accepting the fan theorem which is satisfying to constructivists. In other words their difficulty in in arguing why they should accept the fan "theorem" as an axiom. In classical mathematics there is an easy proof, which is why the fan theorem is less interesting in that context. –  Carl Mummert Jun 15 '11 at 13:26

A little bit of googling yielded this http://www.cairn.info/revue-internationale-de-philosophie-2004-4-page-483.htm

I hope it's not too difficult to read for a non-mathematician.

-
I read the paper and I do not find it very illuminating. Also, the author uses terms as "computable function" which were not part of Brouwer's terminology and which confuses me in regard to in what sense the author sticks to Brouwer's reasoning and in what sense he doesn't. –  corto Jun 15 '11 at 12:44
I think that the term "computable function" was not a part of Brouwer's terminology because from intuitionistic point of view all functions are computable. –  Levon Haykazyan Jun 16 '11 at 8:32