Constructive set theory: Models, independence results and mathematics

数学发展的历史可以部分地被看作是对更通用和更灵活的数据结构的探索。首先是整数，然后是有理数、真实的数和复数，函数的一般概念，最后是任意集合。布尔巴基承担了艰巨的任务，生产一个``充分公理化presentationof数学的整体，并表示`.所有的数学理论都可以看作是广义集合论的推广。.范畴论的出现在某种程度上改变了刚才描述的观点。范畴理论家的态度是，经典集合论的集合范畴SET只是一个可以作为数学论述的一般宇宙的范畴，但还有许多其他的范畴，称为toposes，它们看起来和行为都像SET。拓扑理论的主要来源之一是代数几何，特别是对层的研究。人们可以把拓扑（topos）（例如拓扑空间上的层范畴）看作是广义的集合论域或论域，而经典集合论域仅仅是一个特例。也许理解主题最重要的一步在于认识到每个主题都有自己的逻辑演算。事实证明，这种演算可能与经典逻辑不同，一般来说，持有拓扑的逻辑原则是构造逻辑（也称为直觉主义逻辑）的逻辑原则。由于每一个topos都提供了自己的集合概念，所以基于构造逻辑的集合论自然地出现在topos理论中。因此，集合论中的构造性证明程序具有将数学推理的有效性扩展到最广泛的可能context.While集合论被认为是严谨的，并且已经赢得了提供一个完整的数学形式化系统的地位，它以非计算性和非构造性而闻名。这在某种程度上对经典集合论是正确的，但集合本质上并不具有非构造性和非计算性。构造集合论（和数学）区别于它的传统对手，古典集合论，坚持存在定理的证明在数学尊重建设性的存在：一个存在的主张必须提供构造它的一个实例的方法。构造数学的系统方法的基础，被称为直觉主义，是在布劳威尔对世纪初数学基础危机的反应中奠定的。如今，在计算机科学中，基于类型论或Curry-Howard同构的构造性形式系统在程序开发和语言设计中变得越来越普遍。在Curry-Howard范式中，命题被视为类型，命题的构造性证明被视为它们各自类型的居民，从而以代数的方式将程序和构造性证明的概念联系起来。建构主义集合论（CST）是建构主义、集合论、证明论、类型论、拓扑理论和计算机科学之间相互作用的主要场所。它提供了一套理论框架的发展建设性的数学和一个精炼的框架内的区别概念，这是不明显的，在经典的上下文中，成为revealed.There是核心问题，指导研究人员在经典Cantorian集理论在过去的50年。这个项目的目标是追求建设性集合论的中心问题，其中一些已经长期存在的开放问题。

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.