Constructive Set Theory: Forcing, Large Sets, and Mathematics

构造性集合论：强迫、大集合和数学

• 批准号: 0301162
• 负责人: Michael Rathjen
• 金额: $ 14.13万
• 依托单位: Ohio State University Research Foundation -DO NOT USE
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-06-01 至 2007-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0301162&HistoricalAwards=false
• 关键词: Constructive; Set; Theory; Forcing; Large

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.

AbstractAward：DMS-0301162首席研究员：迈克尔Rathjen一般主题的建设性集理论起源于约翰Myhill的努力，以发现一个简单的形式主义，涉及到主教的建设性数学作为经典的泽梅洛-弗伦克尔集理论（与公理的选择）涉及到经典Cantorian数学。构造性Zermelo-Fraenkel集合论（CZF）为ErrettBishop式的构造数学的发展提供了一个标准的集合理论框架。构造性集合论的标志之一是它在Martin-Lof的直觉类型理论中拥有一个经典的解释，该理论被认为是最可接受的基本思想框架，使数学的构造性方法变得精确。该解释采用了Curry-Howard的“命题作为类型”的思想，即构造性集合论的公理被解释为可证命题。 在过去的50年里，有一些中心问题一直在指导着经典Cantorian集合论的研究者。要进行的研究的目的是追求类似的建设性集合论的中心问题。粗略地说，这些问题涉及集合论原理的独立性（通过可实现性概念和强迫Kripke模型），大集合公理的作用，以及在这样一个框架内的数学形式化。强迫的方法在科恩关于选择公理和连续统假设的著名的独立性结果中占有突出的地位。类似地，与直觉语境密切相关的强迫方法以及可实现结构将被用来解决基于CZF的独立性问题。在过去的40年里，大基数理论一直主导着经典集合论的研究。在直觉主义集合论的背景下，大基数公理必须被大集合公理所取代。所提出的研究的一个中心部分将关注于研究用基本嵌入表达的大概念。我们希望这个项目也能阐明大基数在被称为序分析的证明理论领域中设计强序表示系统的作用。构造数学与其传统的对应物古典数学的区别在于，它坚持数学中存在定理的证明尊重构造性的存在：存在性主张必须提供构造其实例的方法。构造性数学的系统方法的基础，称为直觉主义，是布劳威尔对世纪初数学基础危机的回应。 目前，在计算机科学中，基于类型论或Curry-Howard同构的构造性形式系统在程序开发和语言设计中越来越广泛。程序和构造性证明的概念有着深刻的联系。通过这种连接，证明被用来支持可靠的软件系统的开发。 所谓的Zermelo-Fraenkel集合论的公理为经典数学的形式化提供了一个公认的框架，而构造性集合论（Constructive Set Theory，简称CST）则是从构造性的观点发展数学的一个普遍框架。 这个项目的动机是希望回答关于CST的中心问题，这些问题已经塑造了半个多世纪的经典Cantorian集合论的研究活动。这项工作有望大大提高我们对建构集合论模型的理解，从而扩大建构主义的领域。