1 - THE FOUNDATIONS OF CONSTRUCTIVE MATHEMATICS

Summary

In which the reader is introduced to the three varieties of constructive mathematics that will be studied in detail in subsequent chapters; the framework of Bishop's constructive mathematics is erected; and the elementary theory of the real numbers is developed.

Existence and omniscience

We engage in constructive mathematics from a desire to clarify the meaning of mathematical terminology and practice – in particular, the meaning of existence in a mathematical context. The classical mathematician, with the freedom of methodology advocated by Hilbert, perceives an object x to exist if he can prove the impossibility of its nonexistence; the constructive mathematician must be presented with an algorithm that constructs the object x before he will recognize that x exists.

What do we mean by an algorithm? We may think of an algorithm as a specification of a step-by-step computation, such as a program in some computer language, which can be performed, at least in principle, by a human being or a computer in a finite period of time; moreover, the passage from one step to another should be deterministic. Note that we say ‘performed, at least in principle’, for it is possible for an algorithm to require an amount of time greater than the age of the universe for its complete execution. We are not concerned here with questions of complexity or efficiency.