Proof Theoretic Aspects of Ergodic Ramsey Theory

这个项目涉及证明理论方法的发展，特别是被称为证明挖掘的领域，以及它们在拉姆齐理论中的应用。 拉姆齐理论中的许多定理可以用无穷方法证明，如超积、非标准分析、拓扑动力学和遍历理论。 证明挖掘从这些无限的参数中提取有限的信息。 拟议的研究将应用证明挖掘的方法，以调查：1）显式边界的数值量，这是不明显的无限证明，2）近似的无穷拉姆齐理论陈述“量化”（通常，与可数序数）如何超限一个给定的建设，和3）新的有限类似的无穷方法。 在必要的情况下，拟议中的研究还将通过调查如何解释高阶概念，特别是超滤子的拓扑结构，来扩展证明挖掘工具的剧目。数学中关于整数的具体有限性质的问题通常会使用抽象的无限概念来回答。 被称为“证明挖掘”的证明理论领域的目标是开发解释这种现象的工具。 我们经常发现，有有限方法可以代替无限方法，代价是使论证更难理解。 其中一些论点是如此笨拙，以至于很难想象它们可以被直接发现。 然而，通过将无限论证“展开”为有限论证，我们常常会发现新的信息。 例如，无限证明通常证明一个具有某种性质的数存在，但不提供关于它是哪个数的信息;然而，相应的有限论证通常给出该数大小的上限。

This project deals with the development of methods in proof theory, particularly the area known as proof mining, and their application to Ramsey theory. Many theorems in Ramsey theory can be proven using infinitary methods, in the form of ultraproducts, nonstandard analysis, topological dynamics, and ergodic theory. Proof mining extracts finite information from these infinite arguments. The proposed research will apply the methods of proof mining in order to investigate: 1) explicit bounds on numerical quantities which are not made apparent by infinite proofs, 2) approximations of infinitary Ramsey theoretic statements which "quantify" (typically, with a countable ordinal) how transfinite a given construction is, and 3) new finitary analogs of infinitary methods. Where necessary, the proposed research will also expand the repertoire of proof mining tools by investigating how to interpret higher order notions, particularly the topological structure of the ultrafilters, in finitary terms.Questions in mathematics about concrete, finite properties of the integers often turn out to have answers that make use of abstract, infinite notions. The goal of the area of proof theory known as "proof mining" is to develop tools for explaining this phenomenon. Often, we discover that there are finite methods which can replace the infinite ones, at the price of making the argument much more difficult to understand. Some of these arguments are so unwieldy that it is difficult to imagine that they could be discovered directly. By "unwinding" the infinite argument into finite arguments, however, we often discover new information. For example, infinite proofs often prove that a number with some property exists while providing no information about which number it is; the corresponding finite argument, however, typically gives an upper bound on the size of that number.