Characterising Brouwer's continuity by bar recursion on moduli of continuity (Q2219099)

The paper studies the notions of continuity that arise from inductively generated neighborhood functions and from functions \(\mathbb{N}^{\mathbb{N}}\to \mathbb{N}\) having a bar recursive modulus of continuity, in a strictly constructive context (constructive reverse mathematics). The inductively generated neighborhood function (called \emph{Brouwer operations} in the paper) are given by two constructors of an inductive set \(\mathbb{K}\), \(\mathrm{L} : \mathbb{N}\to\mathbb{K}\) and \(\mathrm{Sup} : (\mathbb{N}\to\mathbb{K})\to\mathbb{K}\), and an associated (primitive / structurally decreasing) recursor \(\mathcal{R}\) satisfying the equations \begin{align*} \mathcal{R} u f & (\mathrm{L} x) = u x\\ \mathcal{R} u f & (\mathrm{Sup} \phi) = f \phi (\lambda x. \mathcal{R} u f (\phi x)). \end{align*} A function \(\xi\) is a bar recursor for a function \(Y : (\mathbb{N}\to\mathbb{N})\to\mathbb{N}\) (the stopping condition for Spector's bar recursion) if \begin{align*} \xi G H s & = G s &\text{when } Y(\hat{s})<|s|\\ \xi G H s & = H s (\lambda x. \xi G H (s*\langle x\rangle)) &\text{when } Y(\hat{s})\geq |s|. \end{align*} The recursion in this case is not primitive/structurally decreasing as in the case of Brouwer operations. While usual/general neighborhood functions can be simply be seen as continuous moduli for the functions they induce, in the strictly constructive setting, the relation between \emph{inductively generated} neighborhood functions and the continuity of functions they induce is more subtle and the subject of this paper. In either classical mathematics (in presence of classical logic and dependent choice) or in intuitionistic mathematics (in presence of bar induction and strong continuity for numbers), all neighborhood functions are inductively defined. Similarly, the relation between bar induction and bar recursion has not been extensively studied in the strictly constructive setting. A first result of the paper is that a function \(Y : (\mathbb{N}\to\mathbb{N})\to\mathbb{N}\) is induced by a Brouwer operation if and only if it has a bar recursive modulus of continuity (Theorem~4.15). A second contribution of the paper is the introduction of the following equivalence-of-continuity principles. \begin{itemize} \item[\(\text{BC}\)] Every continuous function \(Y : (\mathbb{N}\to\mathbb{N})\to\mathbb{N}\) is induced by a Brouwer operation / has a bar recursive modulus. \item[\(\text{BC}_{\text{c}}\)] Every continuous function \(Y : (\mathbb{N}\to\mathbb{N})\to\mathbb{N}\) with a continuous modulus is induced by a Brouwer operation / has a bar recursive modulus. \end{itemize} It is shown in Proposition~5.1 that \(\text{BC}_{\text{c}}\) is equivalent to decidable bar induction, in the presence of the axiom of countable choice and the axiom of choice for functions \(\mathbb{N}\to\mathbb{N}\) and quantifier-free formulas. \(\text{BC}\) is equivalent to continuous bar induction, in the presence of the axiom of countable choice and the axiom of choice for functions \(\mathbb{N}\to\mathbb{N}\) and \(\Pi^0_1\) formulas. A third contribution of the paper is the transposition of the previous results in the settings of Cantor space and uniform continuity.