Strong continuity implies uniform sequential continuity (Q2573727)

This paper is a contribution to a productive and long-term project, initiated by Bridges and Vîţǎ, which aims to develop constructive topology based on the classical theory of nearness spaces. Constructively, apartness seems to be a more basic notion than nearness. In the present paper the notion of `strong continuity' is investigated. Classically, in a metric apartness topology, strong continuity coincides with uniform continuity. However, it is shown that this equivalence requires Ishihara's principle BD-N. This principle holds in Brouwer's intuitionistic mathematics, recursive mathematics and classical mathematics, but is not provable in Bishop-style mathematics. To be precise, BD-N is not true in a model constructed by Beeson. A remarkable technique due to Ishihara allows one to avoid BD-N when one considers only a sequential version of a certain theorem. The present case is no exception. A function \(f\) is called uniformly sequential continuous if \(\rho(f(x_n,x_n'))\to 0\) whenever \(x_n\) and \(x_n'\) are sequences such that \(\rho(x_n,x_n')\to 0\). The rate of convergence does not depend on the sequences \(x_n\) and \(x_n'\), but only on the rate of convergence of the sequence \(\rho(x_n,x_n')\). The main result of the paper is that strong continuity implies uniform sequential continuity. Using BD-N one can then derive that strong continuity implies uniform continuity. According to the authors their proof is smoother than the known classical proofs. The result is certainly interesting and technically non-trivial. However, one may question its importance in constructive practice. Any explicitly definable function on a complete separable metric space is pointwise continuous. This was contended by Brouwer and proved, by traditional methods, as a meta-theorem for many constructive formal systems. This result quickly proves every concrete instance of Theorem 11, the main result of the paper. One may thus wonder whether the results of this paper should be considered as `pseudo-generality', as Bishop may have claimed, or whether they are part of a smooth general framework for constructive general topology.