Constructive set theory: Models, independence results and mathematics

Lead Research Organisation: University of Leeds
Department Name: Pure 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.


10 25 50

publication icon
Chen R (2012) Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory in Archive for Mathematical Logic

publication icon
Crosilla L (2012) A generalized cut characterization of the fullness axiom in CZF in Logic Journal of IGPL

publication icon
Friedman S (2013) Slow consistency in Annals of Pure and Applied Logic

publication icon
Leigh G (2014) The Friedman-Sheard programme in intuitionistic logic in The Journal of Symbolic Logic

publication icon
Rathjen M (2012) Epistemology versus Ontology

publication icon
Rathjen M (2015) Gentzen's Centenary

publication icon
Rathjen M (2014) Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience in Annals of Pure and Applied Logic

publication icon
Rathjen M (2014) Relativized ordinal analysis: The case of Power Kripke-Platek set theory in Annals of Pure and Applied Logic

Description Development of techniques which show that several intuitionistic set theories with Collection axioms have the existence property.
Determining the strength of some forms of the calculus of construction.
Exploitation Route They can be used to extract computational information
from proofs in intuitionistic set theories.
Sectors Creative Economy,Education

Description The centre of this research were results about the existence property in intuitionistic set theories with collection, solving a riddle that was posed thirty years ago. To achieve this, important technical progress on ordinal analysis of theories with power set and exponentiation was essential.
First Year Of Impact 2012
Sector Other
Impact Types Cultural