 Once free choice sequences are admitted into mathematics, so, perhaps to one’s initial surprise, are certain strong choice principles. Let \(P\) be a subset of \(\bN^{\bN} \times \bN\) (where \(\bN\) denotes the set of natural numbers and, for sets \(A\) and \(B, B^A\) denotes the set of mappings from \(A\) into \(B)\), and suppose that for each \(\ba \in \bN^{\bN}\) there exists \(n \in \bN\) such that \((\ba,n) \in P\). From a constructive point of view, this means that we have a procedure, applicable to sequences, that computes \(n\) for any given \(\ba\). According to Brouwer, the construction of an element of \(\bN^{\bN}\) is forever incomplete: a generic sequence \(\ba\) is purely extensional, in the sense that at any given moment we can know nothing about \(\ba\) other than a finite set of its terms. It follows that our procedure must be able to calculate, from some finite initial sequence \((a_0 ,\ldots ,a_N)\) of terms of \(\ba\), a natural number \(n\) such that \(P(\ba,n)\). If \(\bb \in \bN^{\bN}\) is any sequence such that \(b_{k} = a_{k}\) for \(0 \le k \le N\), then our procedure must return the same \(n\) for \(\bb\) as it does for \(\ba\). This means that \(n\) is a continuous function of \(\ba\) with respect to the topology on \(\bN^{\bN}\) given by the metric 