Applications of Large Cardinals to Constructive Set Theory

这个项目的主要目的是研究ZFC(带选择的Zermelo-Fraenkel集合论)标准公理变体下的数学宇宙的结构。特别是，宇宙在ZF和直觉集合论IZF(直觉Zermelo-Fraenkel集合论)和CZF(构造性Zermelo-Fraenkel集合论)下的行为有多大的不同。为了做到这一点，这项工作将分为两部分。第一个是探索在没有选择的经典背景下大基数公理的性质，以及当选择被放弃时，ZFC中某些大基数定义之间的等价性在多大程度上被破坏。第二个涉及直觉主义理论，将涉及研究大集的概念。这些集合的性质类似于冯·诺依曼层次结构的初始部分，最高可达一个大基数。当人们在没有选择的情况下从事理论工作时，遇到的许多问题之一是难以产生这些理论的模型。例如，假设存在ZFC的模型，Lowenheim-Skolem定理给出了一个任意基数的模型。然而，我们知道“基数为K的语言中的每个无限模型都有一个基数为K的基本子模型”这句话等同于长度为K的选择。因此，当在弱选择或根本没有选择的情况下工作时，很难产生“小”模型。另一个我们不知道是否需要选择的结果是证明了在ZFC中没有宇宙本身的非平凡的初等嵌入。直觉主义背景下的大集最早是在1984年由H.Friedman和A.Scedrov在一篇论文中正式引入的。本文的目的是引入不可达集、Mahlo集和集的概念，它们是将宇宙初等嵌入到IZF的传递类模型$M$中的临界点。然后，作者进一步证明了IZF加上一些大集的存在与它的经典对应是等价的。P.Aczel和M.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