Constructivism in mathematics. An introduction. Volume II (Q1188522)

This second volume continues in the same spirit as volume 1 (see Zbl 0653.03040). The first two chapters (7 and 8) are mathematical in nature and deal with the topology of metric spaces and algebra. The constructive notions of metrically and topologically located sets are introduced and proved to coincide under assumption of FAN. More consequences of FAN and other principles are presented. The chapter on algebra is in particular concerned with the elements of ideal theory, linear algebra, polynomial rings and the fundamental theorem of algebra. The remaining chapters are mainly metamathematical, with applications to mathematical systems. Because of the size of this part it seems best to give an impression of its contents by listing the chapters: 9. Finite type arithmetic (HA) and theories of operators (APP), 10. Proof theory of intuitionistic logic (systems of natural deduction, sequent calculi), 11. The theory of types (Martin-Löf systems) and constructive set theory (CZF, IZF), 12. Choice sequences (theory LS for lawless sequences, theory CS for GC-sequences, i.e. generated by continuous operations), 13. Semantical completeness (Beth models, validity, (complete) Heyting algebras, forcing), 14. Sheaves, sites and higher-order logic, 15. Applications of sheaf models (axiom of countable choice, local continuity, models for CS and LS), 16. Epilogue (language and informal rigour, intuitionistic logic, formalisms, equality, creative subject, Dummett's anti-realist argument). The favourable impression from the first volume is fully confirmed by this one. It introduces into quite a number of notions, modern methods and results, with supporting reference to the literature. It proceeds with the same speed and efficiency, while the number of (harmless) errors is remarkably small. The book contains an extensive bibliography, an adequate index and lists of formal systems, axioms and rules and frequently used notations.