Varieties of constructive mathematics.

*(English)*Zbl 0618.03032
London Mathematical Society Lecture Note Series, 97. Cambridge etc.: Cambridge University Press. X, 149 p.; £10.95; $ 19.95 (1987).

The intention of the authors is to give - in a way as simple as the subject matter admits - a clear idea of the problems and methods of modern constructive mathematics, represented by its three most important varietes. These varieties are Bishop’s constructive mathematics BISH, Markov’s algorithmic mathematics RUSS and intuitionistic mathematics INT.

The treatment is carried out in BISH, occasionally enlarged by principles proper to RUSS and INT, i.e. RUSS and INT are viewed as (diverging) extensions of BISH. This is a good choice, because Bishop’s conception of constructive mathematics has proved to have more appeal to the general mathematician (who usually works within the system CLASS of classical mathematics) than the autonomous systems of Markov (RUSS) and Brouwer (INT).

After a brief introductory Ch. 1 on the foundations of constructive mathematics, the practice of constructive mathematics is illustrated in Ch. 2, containing elements of the theory of metric spaces with constructive versions of Baire’s theorem and a discussion of the role of the constructive key-notion of located subset. The importance of this notion is further illustrated in the part on linear mappings of normed linear spaces, which contains a constructive version of the Hahn-Banach theorem and an interesting section on compactly generated Banach spaces. A similar bird’s eye view of the principles and methods of RUSS is given in Ch. 3. There we find discussions of the mean-value theorem, Specker’s nonconvergent bounded increasing sequence of rationals, the Heine-Borel theorem and Ceitin’s theorem on the pointwise continuity of representable functions. Chapter 4 on constructive algebra culminates in a proof of a constructive version of the Hilbert basis theorem.

The discussion of intuitionism in Ch. 5 is rather brief and concentrates on the principle of continuous choice and the fan theorem and its consequences. In Ch. 6 the varieties BISH, RUSS and INT of constructive mathematics are compared with respect to their capability of proving certain key theorems on real functions. This chapter clarifies their mutual relationship.

The final (telegraphic) Ch. 7 discusses the use of Kripke models and topos models in deducing underivability results in intuitionistic logic.

Each chapter contains a number of exercises and a set of explanatory and historical notes and references to the research literature.

The above survey of its content gives an imperfect impression of the book. One should read it to experience its attractive qualities of style and presentation. It contains a remarkable amount of information in its 150 pages and seems to be very well suited as a basis for an introductory course on modern constructive mathematics.

The treatment is carried out in BISH, occasionally enlarged by principles proper to RUSS and INT, i.e. RUSS and INT are viewed as (diverging) extensions of BISH. This is a good choice, because Bishop’s conception of constructive mathematics has proved to have more appeal to the general mathematician (who usually works within the system CLASS of classical mathematics) than the autonomous systems of Markov (RUSS) and Brouwer (INT).

After a brief introductory Ch. 1 on the foundations of constructive mathematics, the practice of constructive mathematics is illustrated in Ch. 2, containing elements of the theory of metric spaces with constructive versions of Baire’s theorem and a discussion of the role of the constructive key-notion of located subset. The importance of this notion is further illustrated in the part on linear mappings of normed linear spaces, which contains a constructive version of the Hahn-Banach theorem and an interesting section on compactly generated Banach spaces. A similar bird’s eye view of the principles and methods of RUSS is given in Ch. 3. There we find discussions of the mean-value theorem, Specker’s nonconvergent bounded increasing sequence of rationals, the Heine-Borel theorem and Ceitin’s theorem on the pointwise continuity of representable functions. Chapter 4 on constructive algebra culminates in a proof of a constructive version of the Hilbert basis theorem.

The discussion of intuitionism in Ch. 5 is rather brief and concentrates on the principle of continuous choice and the fan theorem and its consequences. In Ch. 6 the varieties BISH, RUSS and INT of constructive mathematics are compared with respect to their capability of proving certain key theorems on real functions. This chapter clarifies their mutual relationship.

The final (telegraphic) Ch. 7 discusses the use of Kripke models and topos models in deducing underivability results in intuitionistic logic.

Each chapter contains a number of exercises and a set of explanatory and historical notes and references to the research literature.

The above survey of its content gives an imperfect impression of the book. One should read it to experience its attractive qualities of style and presentation. It contains a remarkable amount of information in its 150 pages and seems to be very well suited as a basis for an introductory course on modern constructive mathematics.

Reviewer: B.v.Rootselaar

##### MSC:

03F65 | Other constructive mathematics |

03-01 | Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations |

03-02 | Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations |

46S30 | Constructive functional analysis |

13E05 | Commutative Noetherian rings and modules |

03F55 | Intuitionistic mathematics |

26E99 | Miscellaneous topics in real functions |