The fan theorem and unique existence of maxima. (English) Zbl 1107.03064

This paper is a contribution to constructive reverse mathematics. As in reverse mathematics with classical logic one asks the question ‘which axiom does this theorem imply’. In the present context the base system is left informal and taken to be Bishop’s constructive mathematics. The theorem under consideration is ‘a uniformly continuous function on the unit interval has a maximum’. This statement will turn out to be related to Brouwer’s ‘Fan Theorem’, which is considered as an axiom in the present context. Constructively, one has to distinguish between having a supremum and having a maximum. The former means that there exists a real number \(M\) which is bigger than all \(x\) in \([0,1]\) and such that for each \(\epsilon>0\) there exists \(x\) such that \(f(x)>M-\epsilon\). The latter means that the supremum is attained: \(f(y)=M\) for some \(y\). Every uniformly continuous function on a compact set has a supremum, but one cannot prove constructively that this supremum is attained. As a general rule classical unique existence hints at constructive existence. Thus one considers functions with at most one maximum. The main result of the paper is the following list of equivalent statements:
1. Each uniformly continuous, real-valued map with at most one maximum on a compact metric space has a maximum.
2. Brouwer’s fan theorem for detachable bars.
3. Each uniformly continuous, real-valued map with at most one maximum on a compact metric space has a strong maximum.
Here a function \(f\) is said to have a strong maximum when there exists \(t\) such that for each \(\epsilon>0\) there exists \(\delta>0\) such that if \(x\in X\) and \(f(x)>f(t)-\delta\), then \(\rho(x,t)<\epsilon\).


03F60 Constructive and recursive analysis
03B30 Foundations of classical theories (including reverse mathematics)
03F55 Intuitionistic mathematics
03F35 Second- and higher-order arithmetic and fragments
26E40 Constructive real analysis
Full Text: DOI


[1] The L.E.J. Brouwer Centenary Symposium pp 41– (1982)
[2] DOI: 10.1216/RMJ-1981-11-4-491 · Zbl 0478.41021 · doi:10.1216/RMJ-1981-11-4-491
[3] Constructive analysis 279 (1985) · Zbl 0656.03042
[4] Notes on constructive set theory (2001)
[5] Computable analysis (2000) · Zbl 0956.68056
[6] Nicht konstruktiv beweisbare Sätze der Analysis 14 pp 145– (1949)
[7] Constructing local optima on a compact interval (2003)
[8] Sūurikaisekikenkyūsho Kīkyūroko 1381 pp 108– (2004)
[9] Complexity theory of real functions (1991)
[10] Elements of intuitionism 39 (2000) · Zbl 0949.03059
[11] Varieties of constructive mathematics 97 (1987)
[12] Continuity and Lipschitz constants for continuous projections (2003)
[13] DOI: 10.1016/0168-0072(93)90213-W · Zbl 0795.03086 · doi:10.1016/0168-0072(93)90213-W
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.