Premium
Brouwer's fan theorem and unique existence in constructive analysis
Author(s) -
Berger Josef,
Ishihara Hajime
Publication year - 2005
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200410038
Subject(s) - mathematics , lemma (botany) , infimum and supremum , constructive , omniscience , equivalence (formal languages) , discrete mathematics , pure mathematics , property (philosophy) , calculus (dental) , computer science , epistemology , medicine , ecology , philosophy , poaceae , dentistry , process (computing) , biology , operating system
Many existence propositions in constructive analysis are implied by the lesser limited principle of omniscience LLPO; sometimes one can even show equivalence. It was discovered recently that some existence propositions are equivalent to Bouwer's fan theorem FAN if one additionally assumes that there exists at most one object with the desired property. We are providing a list of conditions being equivalent to FAN, such as a unique version of weak König's lemma. This illuminates the relation between FAN and LLPO. Furthermore, we give a short and elementary proof of the fact that FAN is equivalent to each positive valued function with compact domain having positive infimum. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)