Proof Theoretic Aspects of Ergodic Ramsey Theory

遍历拉姆齐理论的证明理论方面

• 批准号: 1340666
• 负责人: Henry Towsner
• 金额: $ 3.51万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-08-23 至 2014-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1340666&HistoricalAwards=false
• 关键词: Proof; Theoretic; Aspects; Ergodic; Ramsey

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.

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