Iterated forcing with side conditions and high forcing axioms

这个项目是关于数学独立性的研究。数学被框定在某种固定的“基础理论”中。更具体地说，在高等数学的实践中，人们经常需要指定一个基础理论，在这个基础理论中，人们打算发展一些感兴趣的数学理论。这个基础理论，也被称为基础理论，是用某种固定的形式语言形式化的，由一系列公理组成，这些公理是用固定的形式语言关于数学宇宙的合理(不言而喻)的陈述。人们在基础理论范围内得到的数学定理，就是可以使用某些明确定义的逻辑规则，在有限的许多步骤中从基础理论的公理中推导出来的陈述。最标准的数学基础理论是ZFC(带有选择公理的Zermelo Fraenkel集合论)，但有时人们会考虑通过添加所谓的“大基数公理”来得到ZFC的加强。这些是一系列公理，自然而然地以ZFC为模，构建了一个由越来越强大的理论组成的层次结构。一个值得注意的事实是，在数学中自然产生的每一个理论都可以在由此产生的基本理论之一中得到解释。另一个值得注意的事实是，这些基本理论T中没有一个决定了所有的数学陈述。这意味着，有S的说法，在T内既不能证明S，也不能证明它的否定(相当于，这意味着与S一起假设T的公理，或者与S的否定一起假设T的公理，不能产生任何矛盾)。这种现象被称为独立。这个项目的最终目标是在独立现象的背景下详细研究无限数学对象的组合性质。更具体地说，该项目主要致力于开发特定的“强迫”技术，目的是证明某些性质与零点控制一致，并可能用大型基数公理来增强；换句话说，证明在标准数学中，假设相关对象具有这些组合性质不会产生矛盾(这当然只是证明声明的独立性的任务的一半，该声明声称某一性质对所有相关对象成立；另一半任务是证明关于没有对象具有所讨论的属性的声明的一致性)。在我们的背景下，这种一致性的证明在实践中是通过建立一个通常公理的特定模型来进行的，在该模型中，这些性质是成立的，获得的是经过精心选择的宇宙的“强迫扩展”。这种强制扩展是通过以精确、明确定义的方式向其添加新对象而获得的数学宇宙的某种扩展。实现这一点的另一种方法是通过直接从某些“强制公理”推导出感兴趣的组合性质，该公理先前已被证明相对于ZFC(连同大的基数公理)是一致的，同样是通过一些强制扩展的方法。这些强制公理通常是通常公理的非常强大的自然扩展，从某种意义上说，它们往往提供了关于无限的丰富理论；通常的公理太弱，不能决定这样的理论。这类研究在数学之外的适用性可能来自与理论计算机科学和人工智能的联系，例如在模拟无限过程的背景下。

This project pertains to the study of independence in mathematics. Mathematics is framed within some fixed 'foundational theory'. More concretely, in the practice of advanced mathematics one often needs to specify a foundational theory within which one intends to develop some mathematical theory of interest. This foundational theory, also called basis theory, is formalised in some fixed formal language and consists of a list of axioms, which are reasonable (self-evident) statements, in the fixed formal language, about the mathematical universe. The mathematical theorems one obtains working within the basis theory are simply the statements that can be derived, in finitely many steps, from the axioms of the basis theory using certain well-defined rules of logic. The most standard foundational theory for mathematics is known as ZFC (Zermelo Fraenkel set theory with the axiom of Choice), but sometimes people consider strengthenings of ZFC obtained by adding to it so-called 'large cardinal axioms'. These are a family of axioms that naturally build, modulo ZFC, a hierarchy of stronger and stronger theories. It is a remarkable fact that every theory occurring naturally in mathematics can be interpreted in one of the resulting foundational theories. Another remarkable fact is that none of these foundational theories T decides all mathematical statements. This means that there are statements S such that neither S nor its negation can be proved within T (equivalently, this means that one cannot derive any contradiction from assuming the axioms of T together with S, or from assuming the axioms of T together with the negation of S). This phenomenon is known as independence. The ultimate goal of this project is the detailed study of combinatorial properties of infinite mathematical objects in the context of the independence phenomenon. More concretely, the project focuses mainly on the development of specific 'forcing' techniques aimed at proving that certain such properties are consistent with ZFC, possibly enhanced with large cardinal axioms; in other words, proving that no contradiction can be derived from assuming, within standard mathematics, that the relevant objects have these combinatorial properties (this is of course only one half of the task of proving the independence, from a given basis theory, of the statement saying that a certain property holds for all relevant objects; the other half of the task is to prove the consistency of the statement saying that no object has the property under discussion). In our context, the proof of some such consistency is carried out in practice by building a particular model of the usual axioms in which the properties hold, obtained as a carefully chosen 'forcing extension' of the universe. This forcing extension is a certain extension of the mathematical universe obtained by adding, in a precise well-defined way, a new object to it. Another way to accomplish this is by deriving the combinatorial property of interest directly from some 'forcing axiom', which has previously been shown to be consistent relative to ZFC (together with large cardinal axioms), again by means of some forcing extension. These forcing axioms are typically very powerful natural extensions of the usual axioms, in the sense that they tend to provide a rich theory of the infinite; the usual axioms are too weak to decide such a theory. The applicability of this type of research outside of mathematics might come from connections to theoretical computer science and artificial intelligence, for example in the context of modelling infinite processes.