Principal Investigator: Michael Rathjen
The general topic of Constructive Set Theory originated in John Myhill's endeavour to discover a simple formalism that relates to Bishop's constructive mathematics as classical Zermelo-Fraenkel Set Theory (with the axiom of choice) relates to classical Cantorian mathematics. Constructive Zermelo-Fraenkel Set Theory (CZF) provides a standard set theoretical framework for the development of constructive mathematics in the style of Errett Bishop. One of the hallmarks of constructive set theory is that it possesses a canonical interpretation in Martin-Lof's intuitionistic type theory which is considered to be the most acceptable foundational framework of ideas that make precise the constructive approach to mathematics. The interpretation employs the Curry-Howard `propositions as types' idea in that the axioms of constructive set theory get interpreted as provable propositions. There are central questions that have guided researchers in classical Cantorian set theory over the last 50 years. The objective of the research to be undertaken is to pursue similarly central questions for constructive set theory. Roughly speaking, these are questions addressing the independence of set-theoretic principles (via realizability notions and forcing over Kripke models), the role of large set axioms, and the formalization of mathematics within such a framework. The method of forcing featured prominently in Cohen's famous independence results regarding the axiom of choice and the continuum hypothesis. In a similar vein, forcing methods germane to the intuitionistic context, as well as realizability structures, will be employed to tackle problems of independence on the basis of CZF. The theory of large cardinals has dominated research in classical set theory for the last 40 years. In the context of intuitionistic set theories large cardinal axioms have to be replaced by large set axioms. A central part of the proposed research will be concerned with studying notions of largeness couched in terms of elementary embeddings. It is hoped that this project will also shed light on the role of large cardinals in devising strong ordinal representation systems in the area of proof theory called ordinal analysis.
Constructive mathematics distinguishes itself from its traditional counterpart, classical mathematics, by insisting that proofs of existential theorems in mathematics respect constructive existence: that an existential claim must afford means for constructing an instance of it. The foundations of a systematic approach to constructive mathematics, 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. The concepts of program and constructive proof are connected in a deep way. Via this connection proofs are used to support the development of reliable software systems. The axioms of so-called Zermelo-Fraenkel Set Theory provide an accepted framework for formalizing classical mathematics whereas Constructive Set Theory (briefly CST) is a universal framework for developing mathematics from a constructive viewpoint. This project is motivated by the desire to answer central questions regarding CST, questions that have shaped the research activity in classical Cantorian set theory for more than half a century. The work is expected to substantially enhance our understanding of models of constructive set theory and thereby enlarge the realm of constructivism.
