Constructive Systems: Models and Applications

The central dierence between working in constructive rather than classical mathematics is the meaning of existence. It came explicitly to the fore when Zermelo could not exhibit the well-ordering of the reals he claimed to have proved existed. Brouwer, the originator of intuitionism, rejected proofs by contradiction of the existence of objects because they do not supply the object they purportedly established. He held that no sensible meaning could be attached to the phrase "there exists " other than "we can nd". The history of the development of mathematics can in part be seen as a search for more general and exible data structures. First one had the integers, then the rational, real and complex numbers, the general concept of function, and eventually arbitrary sets. Set theory is identied with rigor and has earned the status of providing a full scale system for formalizing mathematics. On the other hand, set theory has a reputation for being non-computational and nonconstructive. This is certainly true for classical set theory but there is nothing intrinsically nonconstructive about sets. In computer science, constructive formal systems based on type theory or on the Curry-Howard isomorphism have shown their utility for program development and extraction of algorithms from proofs