Iterated forcing with side conditions and high forcing axioms

这个项目是关于数学独立性的研究。数学是建立在某种固定的“基础理论”中的。更具体地说，在高等数学的实践中，人们经常需要指定一个基础理论，在这个基础理论中，人们打算发展一些感兴趣的数学理论。这个基础理论，也被称为基础理论，是用某种固定的形式语言形式化的，由一系列公理组成，这些公理是用固定的形式语言对数学世界的合理（不言自明）陈述。人们在基础理论中所得到的数学定理，仅仅是可以从基础理论的公理中，使用某些定义明确的逻辑规则，经过许多步骤推导出来的陈述。最标准的数学基础理论被称为ZFC（Zermelo Fraenkel set theory with the axiom of Choice），但有时人们会考虑通过添加所谓的“大基数公理”来加强ZFC。这是一系列公理，它们以ZFC为模，自然地建立了一个越来越强的理论层次。一个值得注意的事实是，在数学中自然出现的每一个理论都可以用一个由此产生的基础理论来解释。另一个值得注意的事实是，这些基本理论T中没有一个决定所有的数学陈述。这意味着存在这样的陈述S，即S及其否定都不能在T内被证明（等价地，这意味着人们不能从假设T的公理和S，或者从假设T的公理和S的否定中导出任何矛盾）。这种现象被称为独立性。该项目的最终目标是在独立现象的背景下详细研究无限数学对象的组合性质。更具体地说，该项目主要侧重于开发具体的“强迫”技术，旨在证明某些此类性质与ZFC一致，可能会用大基数公理增强;换句话说，在标准数学中，相关的物体具有这些组合性质（这当然只是证明从给定的基础理论出发，说某个性质对所有相关对象成立的陈述的独立性的任务的一半;任务的另一半是证明没有对象具有所讨论的属性的陈述的一致性）。在我们的上下文中，这种一致性的证明在实践中是通过建立一个通常公理的特定模型来进行的，在这个模型中，这些性质成立，作为宇宙的一个精心选择的“强迫扩展”而获得。这种强制扩张是数学论域的某种扩张，它是通过以一种精确定义的方式向其添加一个新的对象而获得的。另一种实现这一点的方法是通过直接从一些“强制公理”推导出感兴趣的组合性质，这些“强制公理”之前已经被证明相对于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.