An axiomatization of a mathematical theory consists of a system of basic notions as well as a set of axioms about these notions. The mathematical theory is then the set of theorems which can be derived from the axioms. Obviously, one needs a certain logic providing the tools of reasoning in the derivation of these theorems from the axioms. As pointed out by A. Heyting [1963, p. 5], in the early stages of the axiomatic viewpoint, logic was used in an unanalyzed form. In a later stage, in the study of the foundations of mathematics beginning early in the twentieth century, it was realized that a major part of mathematics has to exploit the full power of classical (Boolean) logic [Hatcher, 1982], the strongest in the family of existing logics. For example, group theory is based on first-order logic, and point-set topology is built on a fragment of second-order logic. However, some mathematicians, including the big names of L. E. J. Brouwer, H. Poincare, L. Kronecker and H. Weyl, have taken a constructive position which is in more or less explicit opposition to certain forms of mathematical reasoning used by the majority of the mathematical community. Some of them even endeavoured to establish so-called constructive mathematics, i.e. the part of mathematics that can be rebuilt on constructivist principles. The logic employed in the development of constructive mathematics is intuitionistic logic [Troelstra and van Dalen, 1988], which is genuinely weaker than classical logic.