Paper Info
Title
A Direct Proof of the Equivalence between Brouwer's Fan Theorem and König's Lemma with a Uniqueness Hypothesis
Abstract
From results of Ishihara it is known that the weak (that is, binary) form of Konig's lemma (WKL) implies Brouwer's fan theorem (Fan). Moreover, Berger and Ishihara [MLQ 2005] have shown that a weakened form WKL! of WKL, where as an additional hypothesis it is required that in an effective sense infinite paths are unique, is equivalent to Fan. The proof that WKL! implies Fan is done explicitely. The other direction (Fan implies WKL!) is far less directly proved; the emphasis is rather to provide a fair number of equivalents to Fan, and to do the proofs economically by giving a circle of implications. Here we give a direct construction. Moreover, we go one step further and formalize the equivalence proof (in the Minlog proof assistant). Since the statements of both Fan and WKL! have computational content, we can automatically extract terms from the two proofs. It turns out that these terms express in a rather perspicuous way the informal constructions.
Year
Venue
Keywords
2005
JOURNAL OF UNIVERSAL COMPUTER SCIENCE
Brouwer's fan theorem,Konig's lemma
Field
DocType
Volume
Analytic proof,Discrete mathematics,Uniqueness,Data mining,Computer science,Brouwer fixed-point theorem,König's lemma,Mathematical proof,Lemma (mathematics),Proof assistant,Direct proof
Journal
11
Issue
ISSN
Citations 
12
0948-695X
9
PageRank 
References 
Authors
0.79
5
1
Name
Order
Citations
PageRank
Helmut Schwichtenberg137344.83