Constructive Set Theory: Forcing, Large Sets, and Mathematics

摘要奖：DMS-0301162首席研究员：Michael Rathjen建设性集合论的一般主题起源于JohnMyHill努力发现与毕晓普的建设性数学有关的简单形式主义，因为经典的Zermelo-Fraenkel集合论(具有选择公理)与经典的坎托利数学有关。构造性Zermelo-Fraenkel集合论(CZF)为Errett Bishop风格的构造性数学的发展提供了标准的集合论框架。构造性集合论的特点之一是它在马丁-洛夫的直觉主义类型理论中具有规范的解释，被认为是使数学的建构性方法精确化的最可接受的基本概念框架。解释采用了Curry-Howard‘命题作为类型’的思想，即构造性集合论的公理被解释为可证明的命题。在过去的50年里，有一些核心问题一直指导着经典的坎托利集合论的研究人员。这项研究的目的是为构造性集合论追寻类似的中心问题。粗略地说，这些问题涉及集合论原理的独立性(通过可实现性概念和强迫超越克里普克模型)，大集合公理的作用，以及在这样的框架内数学的形式化。强迫方法在科恩关于选择公理和连续统假设的著名的独立性结果中是突出的特征。同样，在CZF的基础上，将采用与直觉语境相关的强制方法以及可实现性结构来解决依赖问题。在过去的40年里，大基数理论一直主导着经典集合论的研究。在直觉主义集合论的背景下，大的基数公理必须被大的集合论所取代。这项拟议研究的一个中心部分将关注于从基本嵌入的角度来研究大的概念。希望这个项目还能阐明大基数在设计被称为顺序分析的证明论领域的强顺序表示系统中的作用。构造数学通过坚持数学中存在定理的证明尊重构造存在：存在主张必须提供构造它的实例的手段，而区别于它的传统对应的古典数学。在布劳威尔对20世纪初数学基础危机的回应中，奠定了一种称为直觉主义的系统的建构主义数学方法的基础。如今，在计算机科学中，基于类型理论或Curry-Howard同构的构造性形式系统在程序开发和语言设计中已经变得越来越普遍。程序和构造性证明这两个概念有着深刻的联系。通过这种连接验证被用来支持可靠软件系统的开发。所谓的Zermelo-Fraenkel集合论的公理为形式化经典数学提供了公认的框架，而构造性集合论(简称CST)是从建构性的观点发展数学的普遍框架。这个项目的动机是希望回答关于CST的核心问题，这些问题塑造了半个多世纪以来古典广域集合论的研究活动。这项工作有望极大地加深我们对建构主义集合论模型的理解，从而扩大建构主义的领域。

AbstractAward: DMS-0301162Principal Investigator: Michael RathjenThe general topic of Constructive Set Theory originated in JohnMyhill's endeavour to discover a simple formalism that relates toBishop's constructive mathematics as classical Zermelo-Fraenkel SetTheory (with the axiom of choice) relates to classical Cantorianmathematics. Constructive Zermelo-Fraenkel Set Theory (CZF) provides astandard set theoretical framework for the development of constructivemathematics in the style of Errett Bishop. One of the hallmarks ofconstructive set theory is that it possesses a canonicalinterpretation in Martin-Lof's intuitionistic type theory which isconsidered to be the most acceptable foundational framework of ideasthat make precise the constructive approach to mathematics. Theinterpretation employs the Curry-Howard `propositions as types' ideain that the axioms of constructive set theory get interpreted asprovable propositions. There are central questions that have guidedresearchers in classical Cantorian set theory over the last 50years. The objective of the research to be undertaken is to pursuesimilarly central questions for constructive set theory. Roughlyspeaking, these are questions addressing the independence ofset-theoretic principles (via realizability notions and forcing overKripke models), the role of large set axioms, and the formalization ofmathematics within such a framework. The method of forcing featuredprominently in Cohen's famous independence results regarding the axiomof choice and the continuum hypothesis. In a similar vein, forcingmethods germane to the intuitionistic context, as well asrealizability structures, will be employed to tackle problems ofindependence on the basis of CZF. The theory of large cardinals hasdominated research in classical set theory for the last 40 years. Inthe context of intuitionistic set theories large cardinal axioms haveto be replaced by large set axioms. A central part of the proposedresearch will be concerned with studying notions of largeness couchedin terms of elementary embeddings. It is hoped that this project willalso shed light on the role of large cardinals in devising strongordinal representation systems in the area of proof theory calledordinal analysis.Constructive mathematics distinguishes itself from its traditionalcounterpart, classical mathematics, by insisting that proofs ofexistential theorems in mathematics respect constructive existence:that an existential claim must afford means for constructing aninstance of it. The foundations of a systematic approach toconstructive mathematics, known as intuitionism, were laid inBrouwer's response to the foundational crisis in mathematics at thebeginning of the 20th century. Nowadays, in computer science,constructive formal systems based on type theory, or on theCurry-Howard isomorphism have become increasingly widespread forprogram development and language design. The concepts of program andconstructive proof are connected in a deep way. Via this connectionproofs are used to support the development of reliable softwaresystems. The axioms of so-called Zermelo-Fraenkel Set Theory providean accepted framework for formalizing classical mathematics whereasConstructive Set Theory (briefly CST) is a universal framework fordeveloping mathematics from a constructive viewpoint. This project ismotivated by the desire to answer central questions regarding CST,questions that have shaped the research activity in classicalCantorian set theory for more than half a century. The work isexpected to substantially enhance our understanding of models ofconstructive set theory and thereby enlarge the realm ofconstructivism.