Constructive Set Theory: Forcing, Large Sets, and Mathematics

构造集理论的一般主题起源于JohnMyhill的努力，他试图发现一个简单的形式主义，将bishop的构造数学与经典Zermelo-Fraenkel集合理论（带有选择公理）联系起来，与经典cantorian数学联系起来。建构性Zermelo-Fraenkel集合理论（CZF）为毕晓普风格的建构性数学的发展提供了标准的集合理论框架。建构性集合论的一个特点是，它在马丁-洛夫的直觉型理论中有一个经典的解释，直觉型理论被认为是最可接受的基本思想框架，它使数学的建构性方法变得精确。这种解释采用了Curry-Howard的命题作为类型的概念，即构造集合论的公理被解释为可证明命题。在过去的50年里，经典Cantorian集合论的研究人员一直在研究一些核心问题。本研究的目的是为建构性集合论寻找类似的中心问题。粗略地说，这些问题解决了集合理论原理的独立性（通过可实现性概念和强迫overKripke模型），大集合公理的作用，以及在这样一个框架内的数学形式化。强迫方法在科恩关于选择公理和连续统假设的著名的独立性结果中占有突出地位。同样，将采用与直觉主义背景相关的强制方法以及可实现性结构来解决基于CZF的独立性问题。在过去的40年里，大基数理论一直主导着经典集合论的研究。在直觉集合论的背景下，大基数公理必须被大集合公理所取代。提出的研究的一个中心部分将涉及研究在初等嵌入方面的大的概念。希望这个项目也能揭示大基数在设计强序数表示系统方面的作用，该系统在证明理论领域被称为序数分析。建构性数学与其传统的对应物——古典数学的区别在于，它坚持认为数学中存在定理的证明尊重建构性存在：一个存在的主张必须提供构造它的一个实例的方法。构建数学的系统方法，即直觉主义的基础，是在布劳威尔对20世纪初数学基础危机的回应中奠定的。如今，在计算机科学中，基于类型论或curry - howard同构的构造形式系统在程序开发和语言设计中越来越广泛。程序和构造证明的概念有着深刻的联系。通过这种连接，证明被用来支持可靠软件系统的开发。所谓的Zermelo-Fraenkel集合论的公理为形式化经典数学提供了公认的框架，而构造性集合论（简称CST）是从构造性观点发展数学的通用框架。这个项目的动机是希望回答关于CST的核心问题，这些问题已经塑造了半个多世纪以来经典cantoran集合论的研究活动。这项工作有望大大提高我们对建构性集合理论模型的理解，从而扩大建构主义的领域。

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.