Applications of Large Cardinals to Constructive Set Theory

该项目的主要目的是研究ZFC（Zermelo-Fraenkel set theory with choice）标准公理变体下的数学宇宙结构。特别是，如何不同的宇宙行为下ZF一方面和直觉集理论IZF（直觉Zermelo-Fraenkel集理论）和CZF（建设性Zermelo-Fraenkel集理论）的另一方面。为了做到这一点，工作将分为两部分。第一个是探讨大基数公理的性质在经典的设置没有选择和有多少的等价性之间的某些定义的大基数在ZFC打破时，选择下降。第二，这涉及到直觉理论，将涉及研究大集合的概念。这些集合的性质类似于冯·诺依曼体系的初始部分，直到一个大基数。当人们在没有选择的情况下研究一个理论时，遇到的许多问题之一是难以产生这些理论的模型。例如，假设存在ZFC的模型，Lowenheim-Skolem定理给出了任何基数的模型。然而，众所周知，陈述“基数为K的语言中的每一个无限模型都有基数为K的初等子模型”等价于长度K的选择。因此，在选择不足或根本没有选择的情况下，很难产生"小”模型。另一个我们不知道是否需要选择的结果是证明了在ZFC中不存在宇宙到自身的非平凡基本嵌入。直觉主义语境中的大集在1984年由H. Friedman和A.谢德罗夫本文的目的是引入不可达集，Mahlo集和集的概念，是一个基本嵌入的宇宙到一些传递类模型M$的IZF的临界点。然后，作者继续表明，IZF加上一些大集的存在是equiconsistent其经典的对应。一个更实质性的研究大型枢机主教已进行了P。Rathjen和包含在他们的草案的一本书的建设性集理论。这项工作是介绍了一个经常集的想法，这是一个不可访问的定义集的一个组成部分。虽然这两种理论都是直觉主义的，但CZF中的不可达集与IZF中的不可达集有着本质的区别.这是因为，在IZF中，作者只想要IZF模型的集合（因此实际上更接近于词基数的定义），而在CZF中，作者想要一个集合，它恰好具有经典情况下不可接近基数的那些属性。建设性的提法也允许第二个定义，它意味着一个集是不可访问的，给一个简单的标准的性质，该集必须满足，而不是单独断言，该集满足每一个公理的理论。最深入的讨论大集在建设性的设置是在阿尔伯特齐格勒的论文，“集在建设性的集理论”。这项工作给出了一个严格的制定建设性的变种，许多较低的公理在大基数层次。这最终在一个广泛的审查两个重要方面的研究大集合;可实现性和基本嵌入。特别是，从这篇论文的结果显示如何不同的大集合的行为从他们的经典同行。此外，与经典情况不同，假设有更多的大集合满足某些性质并不一定会增加理论的一致性强度。例如，在一个示例中，如果存在一个不可访问是一致的，那么存在它们的适当类也是一致的。在未来几年里，本论文将研究的问题有：1。如何大枢机主教不同没有选择。例如，许多等价公式会发生什么变化？

The main aim of this project is to study the structure of the mathematical universe under variants of the standard axioms of ZFC (Zermelo-Fraenkel set theory with choice). In particular, how different the universe behaves under ZF on the one hand and the intuitionistic set theories IZF (Intuitionistic Zermelo-Fraenkel set theory) and CZF (Constructive Zermelo-Fraenkel set theory) on the other hand. In order to do this, the work will be split into two parts. The first is to explore the nature of large cardinal axioms in the classical setting without choice and how much the equivalences between certain definitions of large cardinals in ZFC break down when choice is dropped. The second, which concerns intuitionistic theories, will involve studying the notion of large sets. These are sets with properties analogous to the initial segment of the von Neumann hierarchy up to a large cardinal.One of the many problems one encounters when working in a theory without choice is the difficulty in producing models of these theory. For example, assuming that there is a model of ZFC, the Lowenheim-Skolem Theorem gives a model of any cardinality. However it is known that that the statement ``Every infinite model in a language of cardinality K has an elementary submodel of cardinality K" is equivalent to choice of length K. Therefore, when working with weak choice or no choice at all, it can be difficult to produce ``small" models. Another result where we don't know whether choice is needed or not is the proof that in ZFC there is no non-trivial elementary embedding of the universe into itself.Large sets in the intuitionistic context were first formally introduced in 1984 in a paper by H. Friedman and A. Scedrov. The purpose of this paper was to introduce the notions of inaccessible sets, Mahlo sets and sets that were the critical point of an elementary embedding of the universe into some transitive class model $M$ of IZF. The authors then go on to show that IZF plus the existence of some large set is equiconsistent to its classical counterpart. A more substantial study of large cardinals has been undertaken by P. Aczel and M. Rathjen and is contained within their draft of a book on Constructive Set Theory. This work is introduces the idea of a regular set which is an integral part of the definition of an inaccessible set. While both intuitionistic theories, inaccessible sets in CZF and fundamentally different from those in IZF. This is because, while in IZF the authors just wanted sets that were models of IZF (so were in fact closer to the definition of wordly cardinals), within CZF the authors wanted a set that had precisely those properties of in the classical case for inaccessible cardinals. The constructive formulation also allows for a second definition of what it means for a set to be inaccessible, giving a simple criterion of properties that the set must satisfy rather than solely asserting that the set satisfies every axiom of the theory.The most in depth discussion of large sets in a constructive setting is given in Albert Ziegler's thesis, ``Sets in Constructive Set Theory". This work gives a rigorous formulation of constructive variants of many of the lower axioms in the large cardinal hierarchy. This culminates in an extensive review of two important aspects of the study of large sets; realisability and elementary embeddings. In particular, the results from this thesis show how differently large sets behave from their classical counterparts. Also, unlike in the classical case, the assumption that there are more large sets satisfying some property does not necessarily increasing the consistency strength of the theory. E.g., if it is consistent that there is one inaccessible then it is consistent that there are a proper class of them. Some of the many questions which will occupy the research for the thesisover the coming years are:1. How do large cardinals differ without choice. E.g. what happens to the many equivalent formu