Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics (Q2869900)

The omniscience principle for a set \(X\) says that, given any decidable property on the set, either there exists a member of \(X\) satisfying the property or no member of \(X\) satisfies the property. This classically true disjunction is not acceptable constructively for already the case \(X=\mathbb{N}\), known as the limited principle of omniscience (LPO), and would imply a constructive solution to the halting problem. NEWLINENEWLINE\smallskip The intuitive reason why LPO should not be acceptable is that \(\mathbb{N}\) is infinite. In this, and a number of previous papers, the author presents infinite sets that even constructively satisfy the omniscience principle. The first such example is \(\mathbb{N}_\infty\), the subset of non-increasing binary sequences of the Cantor space \(2^{\mathbb{N}}\). More complex omniscient infinite sets exist as shown by a construction using infinite ordinals. NEWLINENEWLINE\smallskip The method to prove a set omniscient goes via the notion of selection function. The paper contains a survey of results on selection functions, as well as detailed explanations on how the relevant constructions of G. Kreisel [\textit{H. P. Barendregt}, The lambda calculus. Its syntax and semantics. Rev. ed. York-Oxford: North-Holland. 581 (1984; Zbl 0551.03007), Exercise 1], \textit{T. J. Grilliot} [J. Symb. Log. 36, 245--248 (1971; Zbl 0224.02034)] and \textit{H. Ishihara} [J. Symb. Log. 56, No. 4, 1349--1354 (1991; Zbl 0745.03048)] can be interpreted as statements about selection functions. Selection functions can, perhaps, also be seen as constructive versions of Hilbert's \(\epsilon\)-operator.