Proof Theory: Finite Data from Infinite Mathematics

证明论：无限数学中的有限数据

• 批准号: 1600263
• 负责人: Henry Towsner
• 金额: $ 15.41万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2020-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1600263&HistoricalAwards=false
• 关键词: Proof; Theory; Finite; Data; Infinite

Many mathematical questions can be solved in multiple ways, each with its own advantages. Short, conceptual proofs can avoid complicated calculations, but sometimes cannot provide the detailed quantitative information those calculations would reveal. A recent insight is that, sometimes, mathematics can have it both ways. By studying the structure of mathematical proof itself, techniques from the field known as proof theory make it possible to take abstract proofs and to extract detailed calculations from them. Used in the opposite direction, these techniques can take certain kinds of lengthy calculations and replace them with short, abstract arguments which can then be generalized to prove new results. The focus of this project is to both further extend these techniques to new areas, particularly recently discovered applications in statistics, as well as continue the application of known techniques to new problems, especially in areas where probability and randomness play a central role.In this project, Towsner will build on previous applications of ultraproducts to studying the way mathematical objects can be separated into structured and random parts. An explicit quantitative approach to such dichotomies has long been central to extremal graph theory, but recent work has shown that these can also be viewed in measure-theoretic terms by using ultraproducts to mediate between the finitary and infinitary perspectives, leading to new results in the area. Towsner will study this connection systematically, both developing new tools in the infinitary setting and using the proof-theoretic functional interpretation to translate these tools back to the classical setting, extracting explicit calculations from these infinitary arguments.

许多数学问题可以用多种方法解决，每种方法都有自己的优点。简短的概念证明可以避免复杂的计算，但有时不能提供这些计算所揭示的详细的定量信息。最近的一个洞察是，有时，数学可以两全其美。通过研究数学证明本身的结构，来自被称为证明论的领域的技术使得获取抽象的证明并从中提取详细的计算成为可能。在相反的方向上，这些技术可以进行某些类型的冗长计算，并用简短、抽象的论点来取代它们，然后可以推广这些论点来证明新的结果。这个项目的重点是将这些技术进一步扩展到新的领域，特别是最近在统计学中发现的应用，以及继续将已知技术应用于新的问题，特别是在概率和随机性发挥核心作用的领域。在这个项目中，Towsner将建立在超积的先前应用的基础上，研究数学对象如何被分为结构部分和随机部分。这种二分性的显式定量方法长期以来一直是极值图论的核心，但最近的工作表明，通过使用超积在有限和无限视角之间进行调解，这些二分性也可以用测度论的形式来看待，从而在该领域产生了新的结果。Towsner将系统地研究这种联系，既在无限背景下开发新的工具，又使用证明论函数解释将这些工具翻译回经典背景，从这些无限论证中提取显式计算。