Proof Theoretic Aspects of Ergodic Ramsey Theory

这个项目涉及证明理论中方法的发展，特别是被称为证明挖掘的领域，以及它们在拉姆齐理论中的应用。Ramsey理论中的许多定理都可以用超积、非标准分析、拓扑动力学和遍历理论等无限方法来证明。证据挖掘从这些无限的论证中提取有限的信息。建议的研究将应用证明挖掘的方法来调查：1)没有被无限证明明显的数值的显式界限，2)“量化”(通常用可数序数)给定结构的超限的无穷Ramsey理论语句的近似，以及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.