Truth, proof and infinity. A theory of constructions and constructive reasoning (Q1273591)

The fact that the intuition behind sets is imperfect (and easily leads to paradoxes) has motivated many mathematicians to replace set-theoretic foundation of mathematics by a new (more intuitive) foundation. The corresponding criticism of the set intuition and the resulting formalisms are described in the first chapters of the book. Probably the most intuitively convincing attempts came from considering the notions of a ``process'' and ``construction'' (algorithm) as a new basis for mathematics. These notions led to, correspondingly, intuitionistic and constructive directions in mathematics. The author shows that the intuitions behind the purely intuitionistic direction (such as a notion of ``choice sequence'') are also not very clear, so he prefers constructive mathematics, with its notion of construction. The original informal and semi-formal ideas of intuitionistic and constructive mathematics have led to several different formalisms. The original formalisms were mainly aimed at formalizing the original ideas; however, since then, these formalisms have evolved in different directions: some of them have been reformulated so as to make the corresponding constructive mathematics as close to the working mathematics as possible; some other formalisms were reformulated so as to make the fundamental logical analysis (e.g., comparison with the corresponding classical theories) easier. The resulting reformulated formalisms are very convenient for their new purposes, but, due to the reformulation, the underlying axioms and principles are far from being intuitively clear. It is therefore desirable to come up with a new formalism in which all the assumption would be in perfectly clear accordance with the original ideas of constructive mathematics. To achieve this goal, we cannot simply go back to the original formalisms, because in the process of reformulation some features of these original formalisms have been corrected. The author proposes to provide a new intuitively clear foundation for constructive mathematics. The resulting formalism turns out to be very close to the constructive mathematics as proposed by the Russian school of constructive mathematics originated by A. A. Markov and N. A. Shanin [see, e.g., \textit{B. A. Kushner}, Lectures on constructive mathematical analysis (Russian) (1973; Zbl 0285.02029); English translation (1984; Zbl 0547.03040), and references therein]; page-long constructions from the book are very similar to the constructions presented in the original papers and monographs by N. A. Shanin and other pioneers of that direction (unfortunately, the author seems to be unfamiliar with this direction and does not cite any of it). There is an important difference between the author's formalism and the Russian constructive mathematics. Namely, while in both formalisms a first-order function (e.g., from integers to integers) is defined as an algorithm, second-order objects like functionals (mappings from functions to integers) are defined differently: in the original Markov-Shanin formalism, a functional is defined as an algorithm which acts on codes of the corresponding functions, while in the author's formalism, a functional uses the input function as a black box (oracle), but has to access to its code (in the Markov-Shanin direction, such a definition has been developed by \textit{V. P. Chernov} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 32, 140-147 (1973; Zbl 0347.02023); English translation in J. Sov. Math. 6, 465-470 (1976; Zbl 0375.02023)] and by \textit{Yu. L. Ershov} [Z. Math. Logik Grundlagen Math. 19, 289-388 (1973; Zbl 0281.02041); ibid. 21, 473-584 (1975; Zbl 0344.02031); ibid. 23, 289-371 (1977; Zbl 0374.02028); Decision problems and constructivizable models (Russian) (1980; Zbl 0495.03009)]; see also formalizations of Bishop's constructive mathematics). The author shows, in detail, how his formalism leads to Heyting arithmetic, to constructive analysis, and how classical arithmetic can be interpreted within this new formalism. The fact that such an interpretation is possible is not new (it dates back to Gödel), but the author's proof is much more intuitive and natural than the previously known ones (albeit much longer).