Minima of initial segments of infinite sequences of reals

Suppose that 〈 x k 〉 k ∈ℕ is a countable sequence of real numbers. Working in the usual subsystems for reverse mathematics, RCA 0 suffices to prove the existence of a sequence of reals 〈 u k 〉 k ∈ℕ such that for each k , u k is the minimum of { x 0 , x 1 , …, x k }. However, if we wish to prove the existence of a sequence of integer indices of minima of initial segments of 〈 x k 〉 k ∈ℕ , the stronger subsystem WKL 0 is required. Following the presentation of these reverse mathematics results, we will derive computability theoretic corollaries and use them to illustrate a distinction between computable analysis and constructive analysis. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)