Constructivism in mathematics. An introduction. Volume I (Q1188500)

In the preface the authors present this first volume as an all-round introduction to constructivism in the wide sense, covering in particular Brouwer's intuitionism, Bishop's constructive mathematics and Markov's constructive recursive mathematics. Its main concern is with these different forms of constructive mathematics and with the metamathematics of constructivism. After an introduction on constructivity and its history there follows a chapter on logic, treating natural deduction, classical and intuitionistic logic, Hilbert-type systems and Kripke semantics. The third chapter deals with primitive recursive and intuitionistic first order arithmetic, algorithms, inductive definitions, metamathematics of Heyting's arithmetic, higher order logic and arithmetic and the formalization of elementary recursion theory. Essential for a deeper understanding of the different forms of constructive mathematics are the principles discussed in chapter four, such as axioms of choice, continuity principles, Church's thesis, Markov's principle, fan theorem, bar induction, Kripke's schema. The remaining chapters 5 and 6 introduce constructive Cauchy and Dedekind reals, develop their arithmetic and part of elementary real analysis. All chapters contain a set of notes with supplementary information such as historical notes and suggestions for further reading as well as a substantial set of exercises. The book is very rich in content: it discusses about twenty formal systems and a multiple of special axioms. Generally the treatment is efficient and clear, although sometimes a little hasty. It introduces well into recent results and current research. It is a good guide to more specialized treatises on constructive (meta-) mathematics (among which Vol. II). However a book of about 300 pages, with an equal amount hidden in the exercises is not exactly an introduction for a reader with only some knowledge of classical first order predicate logic, as stated in the preface. Obviously it is also tacitly assumed that he has some knowledge of mathematics (e.g. ordinals). In this connection it is significant that advice is supplied for the content of an introductory course to be extracted from the book, comprising about a hundred pages (which seems to be the normal size for such a course). In my opinion the merit and permanent value of the book lies in the first place in the fact that it gives an efficient, clear and well-considered exposition of its field of interest. The book is very well produced and there is little to complain with respect to the exposition. Of course there are always some unfortunate spots, which in this case are generally of a trivial nature and can be easily resolved by an interested reader. I mention a few examples: The names of the elimination rules on p. 38 are contrary to those on p. 40 (which are natural). The notion of a tree is defined on p. 186, but is used earlier many times, e.g. in the proof on p. 90. On p. 113 interchange the indices 0 and 2. In the proof of the corollary on p. 221 a well-founded tree occurs, whose notion is defined on p. 224, while it could have been included in the definition on p. 186. On p. 264 insert an apartness sign in the open space. In the first line of p. 312 read quasi cover for quasi-order. A little suspect is the remark on p. 322 that a proof is found in the exercises to ch. 7 (vol. II). Usually in the exercises one is asked to supply a proof.