In his 1907 doctoral thesis [Brouwer 23] Brouwer advanced the view that the basis of mathematics and of logic is found in the capacity of human beings to carry out mental constructions. On the method of proof by contradiction he says, ``The words of your mathematical demonstration merely accompany a mathematical construction that is effected without words. At the point where you enounce the contradiction, I simply perceive that the construction no longer goes, that the required structure cannot be imbedded in the given basic structure. And when I make this observation, I do not think of a principium contradictionis.''
In the 1960's the mathematician E. Bishop carried out a sweeping development of mathematics along the lines conceived by Brouwer. Bishop's works, and those of his followers [Bishop 67,Bishop & Bridges 85,Bishop & Cheng 72,Bridges 79,Chan 74], have started a modern school of constructive mathematics that we believe is in harmony with the influence of computing in mathematics, an influence seen in many quarters [Nepeivoda 82,Goad 80,Goto 79,Takasu 78]. In Bishop's words [Bishop 67], ``The positive integers and their arithmetic are presupposed by the very nature of our intelligence.... Every mathematical statement ultimately expresses the fact that if we perform certain computations within the set of positive integers, we shall get certain results.... Thus even the most abstract mathematical statement has a computational basis.''
Very different views of mathematics were put forward by G. Frege [Frege 1879] and by Russell [Russell 08,Whitehead & Russell 25], as they attempted to reduce ``mathematical'' ideas to ``logical'' ideas. We shall not consider the philosophical points here, but we note that Frege gave us the predicate calculus in Begriffssschrift and that Russell and Whitehead gave us Principia Mathematica, a formal system of mathematics based on type theory.
can be seen as expressing the philosophical ideas of Brouwer and Bishop in a language closely related to the type theory of Russell. Types prescribe constructions; some of these constructions are recognized as the meaning of propositions.