On a continuity theorem for constructive functions. (English. Russian original) Zbl 1391.03043

Vladimirov, A. A.

J. Math. Sci., New York 199, No. 1, 6-15 (2014); translation from Zap. Nauchn. Semin. POMI 407, 17-34 (2012).

The paper aims at characterising the class of uniformly continuous maps of compact constructive metric spaces without using the notion of continuity, and not presuming the functions can be extended to formal points. Specifically, the major result in the paper is the proof that a total constructive map from a compact metric space into a complete metric space preserving the precompactness of subsets, is uniformly continuous.
Although the paper is very neat and clear, it may pose a number of difficulties to a potential reader. In the first place, it refers to Shanin’s and Markov’s view of constructive mathematics, which differs in many aspects to other approaches. In particular, in the context of the paper, it is worth reminding that Markov accepts a variant of Church’s thesis, while Bishop does not use it, even if accepting it as plausible. Also, in the Russian constructive approach to mathematics, the so-called Markov’s principle, stating that \(\neg \neg \exists x.\, A\) entails \(\exists x.\, A\) is assumed, provided \(A\) being decidable, while the principle is rejected in the other major systems, especially Brouwer’s and Bishop’s. A good starting point to understand the conceptual framework of the article is [B. A. Kushner, Am. Math. Mon. 113, No. 6, 559–566 (2006; Zbl 1110.01009)].
The second major difficulty is that most background results, cited in the first part of the work, have been published in the sixties and the seventies in USSR journals, and they are in Russian. Not all of them are easily accessible, and some of them have not been translated.
The dry style, emphasised by the numbering of paragraphs is very distant from the usual scholar standards: this way of presenting the content, which is typical of some parts of the Russian scientific tradition, may be intimidating, but, in fact, it helps to proceed along the proofs, by condensing each major step in a paragraph.
The result is significant in the context of Markov’s constructive mathematics, but to fully appreciate, it is worth comparing the similar achievements in Bishop’s line of thought. In this respect, there are many references, for example, [D. Bridges et al., Lect. Notes Comput. Sci. 2471, 89–102 (2002; Zbl 1021.03056)] provides a reasonably close starting point.

Reviewer: Marco Benini (Buccinasco)

MSC:

03F60	Constructive and recursive analysis
26E40	Constructive real analysis
54C10	Special maps on topological spaces (open, closed, perfect, etc.)
54E45	Compact (locally compact) metric spaces

Keywords:

constructive metric space; compactness; Hausdorff metric; uniform continuity

Citations:

Zbl 1110.01009; Zbl 1021.03056

References:

[1]	B. A. Kushner, ”A constructive version of König’s theorem; functions computable in the sense of Markov, Grzegorczyk, and Lacombe,” in: The Theory of Algorithms and Mathematical Logic [in Russian], B. A. Kushner and N. M. Nagorny (eds.), CC AS USSR (1974), pp. 87–111.
[2]	A. A. Markov, ”On the language L {\(\omega\)}| ,” Dokl. Akad. Nauk SSSR, 215, No. 1, 57–60 (1974).
[3]	A. A. Vladimirov and M. N. Dombrovskii-Kabanchenko, Stratified Semantic System [in Russian], CCAS Publ., Moscow (2009).
[4]	N. A. Shanin, ”A constructive interpretation of mathematical judgments,” Trudy Mat. Inst. Steklov, 52, 226–311 (1958).
[5]	B. A. Kushner, Lectures on Constructive Mathematical Analysis, Amer. Math. Soc., Providence, Rhode Island (1973).
[6]	N. A. Shanin, ”A sketch of a finitary version of mathematical analysis,” Preprint of PDSIM, 06-2000.
[7]	N. A. Shanin, ”Constructive real numbers and constructive functional spaces,” Trudy Mat. Inst. Steklov, 67, 15–294 (1962).
[8]	G. S. Tseitin, ”Algorithmic operators in constructive metric spaces,” Trudy Mat. Inst. Steklov, 67, 295–361 (1962).