Mathematical Sciences: A Model-Theoretic Approach to Proof Theory

虽然Zermelo-Fraenkel集合理论为数学的形式化提供了一个广泛而灵活的框架，但最近的证明理论研究表明，大量的日常数学论证与二阶算法的弱得多的子系统更密切相关。在这个项目中，Avigad将使用模型理论技术来探索这些理论的有限组合结果。这包括发现类似帕里斯-哈林顿定理的拉姆齐理论的独立性，以及发展一种组合的、模型理论的方法来进行序数分析。数学逻辑的目的是创建描述数学实践的各个方面的形式化模型，并应用数学技术来分析这些模型。自本世纪初以来，两种相互矛盾和对立的数学观点一直在不安地共存。从经典的观点来看，数学是“关于”无限的，产生了强大而引人注目的抽象。从建设性的观点来看，数学必须总是有一些具体的、计算的意义，它的适用性由此而来。该项目旨在通过对无限假设及其有限组合结果的正式探索，更好地理解数学实践中这两个方面之间的相互作用。

While Zermelo-Fraenkel set theory provides a broad and flexible framework for the formalization of mathematics, recent proof-theoretic research has shown that a good deal of day-to-day mathematical argumentation correlates more closely with much weaker subsystems of second-order arithmetic. In this project Avigad will use model-theoretic techniques to explore the finitary combinatorial consequences of these theories. This includes finding Ramsey-theoretic independences akin to the Paris-Harrington theorem, and developing a combinatorial, model-theoretic approach to ordinal analysis. The aim of mathematical logic is to create formal models that describe various aspects of mathematical practice, and apply mathematical techniques to the analysis of these models. Since the beginning of this century, two conflicting and antagonistic views of mathematics have shared an uneasy coexistence. From a classical point of view, mathematics is "about" the infinite, yielding powerful and compelling abstractions. From a constructive point of view, mathematics must always have some concrete, computational meaning, from which it derives its applicability. This project aims to obtain a better understanding of the interplay between these two aspects of mathematical practice, through the formal exploration of infinitary assumptions and their finite, combinatorial consequences.