×

Strong continuity implies uniform sequential continuity. (English) Zbl 1088.03048

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.

MSC:

03F60 Constructive and recursive analysis
03F65 Other constructive mathematics
54C08 Weak and generalized continuity
54E17 Nearness spaces
54E35 Metric spaces, metrizability
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Beeson, M. J.: ‘The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations’. J. Symb. Logic 40, 321–346 (1975) · Zbl 0316.02038 · doi:10.2307/2272158
[2] Beeson, M. J.: Foundations of Constructive Mathematics. Springer–Verlag, Heidelberg, 1985 · Zbl 0565.03028
[3] Bishop, E.: Foundations of Constructive Analysis. McGraw–Hill, New York, 1967 · Zbl 0183.01503
[4] Bishop, E., Bridges, D.: Constructive Analysis. Grundlehren der Math. Wissenschaften 279, Springer–Verlag, Heidelberg, 1985 · Zbl 0656.03042
[5] Bridges, D., van Dalen, D., Ishihara, H.: ‘Ishihara’s proof technique in constructive analysis’. Indag. Math. 13, 433–440 (2002) · Zbl 1092.47063 · doi:10.1016/S0019-3577(02)80024-6
[6] Bridges, D., Richman, F.: Varieties of Constructive Mathematics. London Math. Soc. Lecture Notes 97, Cambridge: Cambridge University Press, 1987 · Zbl 0618.03032
[7] Bridges, D., Mines, R.: ‘Sequentially continuous linear mappings in constructive analysis’. J. Symb. Logic 63, 579–583 (1998) · Zbl 0927.03082 · doi:10.2307/2586851
[8] Bridges, D., Ishihara, H., Schuster, P.: ‘Sequential compactness in constructive analysis’. Österreich. Akad. Wiss. Math.-Natur. Kl. Sitzungsber. II 208, 159–63 (1999) · Zbl 1001.03056
[9] Bridges, D., Ishihara, H., Schuster, P.: ‘Compactness and continuity, constructively revisited’. In: Computer Science Logic (J. Bradfield, ed; Proceedings of 16th International Workshop CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, September 22–25), Lecture Notes in Computer Science 2471, 89–102, Springer–Verlag, Berlin and Heidelberg, 2002 · Zbl 1021.03056
[10] Bridges, D., Vîţă, L.: ‘Apartness spaces as a framework for constructive topology’. Ann. Pure Appl. Logic. 119 (1–3), 61–83 (2003) · Zbl 1044.03048
[11] Cameron, P., Hocking, J.G., Naimpally, S.A.: ‘Nearness, a better approach to continuity and limits, Part II’. Mathematics Report #18–73, Lakehead University, Ontario, Canada, 1973
[12] Dummett, M.: Intuitionism: An Introduction (2nd Edn). Oxford University Press, 2000 · Zbl 0949.03059
[13] Ishihara, H.: ‘Continuity and nondiscontinuity in constructive mathematics’. J. Symb. Logic 56, 1349–1354 (1991) · Zbl 0745.03048 · doi:10.2307/2275479
[14] Ishihara, H.: ‘Continuity properties in constructive mathematics’. J. Symb. Logic 57, 557–565 (1992) · Zbl 0771.03018 · doi:10.2307/2275292
[15] Ishihara, H.: ‘Markov’s principle, Church’s thesis and Lindelöf’s theorem’. Indag. Mathem., N.S. 4, 321–325 (1993) · Zbl 0795.03087 · doi:10.1016/0019-3577(93)90005-J
[16] Ishihara, H.: ‘A constructive version of Banach’s inverse mapping theorem’. New Zealand J. Math 23, 71–75 (1994) · Zbl 0835.46068
[17] Ishihara, H.: ‘Sequential continuity in constructive mathematics’. In: Combinatorics, Computability and Logic (Proceedings of DMTCS’01, Constanţa, Romania, 2–6 July 2001; Calude, C.S., Dinneen, M.J., Sburlan, S. (eds.)), 5–12, DMTCS Series 17, Springer–Verlag, London, 2001 · Zbl 0987.03053
[18] Ishihara, H., Schuster, P.: ‘A constructive uniform continuity theorem’. Quarterly J. Math. 53, 185–193 (2002) · Zbl 1004.54011 · doi:10.1093/qjmath/53.2.185
[19] Ishihara, H., Yoshida, S.: ‘A constructive look at the completeness of J. Symb. Logic 67, 1511–1519 (2002) · Zbl 1053.03036 · doi:10.2178/jsl/1190150296
[20] Kushner, B. A.: Lectures on Constructive Mathematical Analysis. Amer. Math. Soc., Providence RI, 1985 · Zbl 0547.03040
[21] Schuster, P. M.: ‘Elementary choiceless constructive analysis’. In: Computer Science Logic (Proceedings of Conference in Fischbachau, August 2000; P. Clote, H. Schwichtenberg, eds), Lecture Notes in Computer Science 1862, 512–526, Springer–Verlag, Berlin, 2000 · Zbl 0973.03079
[22] Schuster, P., Vîţă, L., Bridges, D.: ‘Apartness as a relation between subsets’. In: Combinatorics, Computability and Logic (Proceedings of DMTCS’01, Constanţa, Romania, 2–6 July 2001; Calude, C.S., Dinneen, M.J., Sburlan, S. (eds.)), 203–214, DMTCS Series 17, Springer–Verlag, London, 2001
[23] Schuster, P. M.: ‘Unique existence, approximate solutions, and countable choice’. Theor. Comp. Sci. 305, 433–455 (2003) · Zbl 1050.03042 · doi:10.1016/S0304-3975(02)00707-7
[24] Troelstra, A. S., van Dalen, D.: Constructivism in Mathematics: An Introduction (two volumes). North Holland, Amsterdam, 1988 · Zbl 0653.03040
[25] Weihrauch, K.: ‘A foundation for computable analysis’. In: Combinatorics, Complexity, & Logic(Proceedings of Conference in Auckland, 9–13 December 1996; Bridges, D.S., Calude, C.S., Gibbons, J., Reeves, S., Witten, I.H. (eds)), Springer–Verlag, Singapore, 1996
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.