Constructive set theory: Models, independence results and mathematics

The history of the development of mathematics can in part be seen as a search for more general and flexible datastructures. First one had the integers, then the rational, real and complex numbers, the general concept of function, and eventually arbitrary sets. Bourbaki undertook the formidable task of producing a ``fully axiomatised presentationof mathematics in entirety and has said ``... all mathematics theories may be regarded as extensions of the generaltheory of sets ... . The emergence of category theory has somewhat changed the perspective just described. The category-theorists attitude is that the category of sets of classical set theory, SET, is just one category that can serve as a general universe of mathematical discourse but that there are many other categories, called toposes, thatlook and behave like SET. One of the primary sources of topos theory is algebraic geometry, in particular the studyof sheaves. One may think of a topos (e.g. the category of sheaves over a topological space) as a generalized set-theoretic universe or universe of discourse, with the classical set universe being merely a special case. Perhapsthe most important step in understanding toposes consists in realizing that each topos carries its own logical calculus. It turns out that this calculus may differ from classical logic, and in general the logical principles that holdin a topos are those of constructive logic (also known as intuitionistic logic). Since each topos provides its own notion of set, set theory based on constructive logic emerges naturally in topos theory. As a result, constructive proof procedures in set theory have the effect of extending validity of mathematical reasoning to the widest possiblecontext.While set theory is identified with rigour and has earned the status of providing a full scale system for formalizing mathematics it has a reputation for being non-computational and nonconstructive. This is to some extent true for classical set theory but there is nothing intrinsically non-constructive and non-computational about sets. Constructive set theory (and mathematics) distinguishes itself from its traditional counterpart, classical set theory,by insisting that proofs of existential theorems in mathematics respect constructive existence: that an existentialclaim must afford means for constructing an instance of it. The foundations of a systematic approach to constructivemathematics, known as intuitionism, were laid in Brouwer's response to the foundational crisis in mathematics at the beginning of the 20th century. Nowadays, in computer science, constructive formal systems based on type theory, or on the Curry-Howard isomorphism have become increasingly widespread for program development and language design. Within the Curry-Howard paradigm, propositions are viewed as types and constructive proofs of propositions are viewed as inhabitants of their respective types, thereby connecting the concepts of programme and constructive proof in an algebraic way. Constructive set theory, CST, constitutes a major site of interaction between constructivism, set theory, proof theory, type theory, topos theory and computer science. It provides a set theoretical framework for the development of constructive mathematics and a refining framework within which distinctions between notions, which are not apparent in the classical context, become revealed.There are central questions that have guided researchers in classical Cantorian set theory over the last 50 years. The objective of this project is to pursue central questions for constructive set theory, some of which have been long-standing open problems.