zbMATH — the first resource for mathematics

Foundations of constructive mathematics. Metamathematical studies. (English) Zbl 0565.03028
Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge, Bd. 6. Berlin etc.: Springer-Verlag. XXIII, 466 p. DM 168.00 (1985).
On the last page of this well organized book its subject matter is summarized as being about constructive metamathematics, i.e. the study of (formal) mathematical theories with intuitionistic logic, from about 1970 onward, which was stimulated by E. A. Bishop’s ”Foundations of constructive analysis” (1967; Zbl 0183.015)], a conscious and apparently very successful piece of constructive propaganda, as Bishop put it. The Brouwer movement (i.e. intuitionistic mathematics) was not killed and dead as Bishop said in 1967, but it certainly was in a reduced state and mainly concerned with isolated local problems. The metamathematics of intuitionistic analysis however was already on its way through the work of Kreisel. In any case Bishop succeeded in giving an accessible constructive treatment of a substantial part of mathematics which could not be overlooked and certainly stimulated logicians to the study of the foundations of constructive mathematics.
The author considers his book to be of interest to mathematicians, computer scientists, proof-theoretic experts and mathematically trained philosophers. As minimal prerequisites are listed, familiarity with Bishop’s constructive mathematics, intuitionistic (logic and) mathematics and a good course on mathematical logic.
The book is divided into four parts, each of which has its own introduction, describing clearly its contents in general terms. The first part ”practice and philosophy of constructive mathematics” introduces into the concepts and methods of constructive mathematics with quite a number of examples from various fields. In addition the informal foundations are discussed and the different constructivist positions, with special attention to recursive mathematics.
The second and third part, ”formal systems of the seventies” and ”metamathematical studies”, together comprising some 300 pages form the hard core of the work. These parts give in a very coherent and comprehensive way expositions of the main modern formal systems for constructive mathematics, their interrelations and metamathematical methods and results. This is a remarkable piece of work into which must have gone a considerable amount of energy, not in the least because of the care the author has taken to present Martin-Löf’s constructive type theories as clearly as possible.
The fourth part is devoted to a discussion of philosophical considerations concerning the concept of constructive proof as a continuation of studies by Kreisel and Goodman.
The book ends with a concise historical appendix, tracing the roots of constructive mathematics and its turbulent development, including the origins of non-constructive mathematics which in retrospect has certainly been of importance to metamathematics. Throughout the book we find a series of discussions on the significance of the material presented by a number of theatrical characters of different philosophical and foundational signature, some of which already took part in the discussions in A. Heyting’s ”Intuitionism. An introduction” (1956; Zbl 0070.008). Parts of the many exercises are used to add an external content to the book and in this way contribute to its relatively moderate size. The book itself contains a wealth of information presented systematically with precision and an admirable clarity of style, which no reader will fail to experience and enjoy.
Reviewer: B.van Rootselaar

03F50 Metamathematics of constructive systems
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03F55 Intuitionistic mathematics
03F60 Constructive and recursive analysis
03F65 Other constructive mathematics