Explicit Proofs from Compactness and Saturation

现代数学的一个令人惊讶的方面是，通常可以证明，在不提供执行计算的显式方法的情况下，计算某事是可能的。这个研究项目集中在这种情况下发生的情况，因为论证是间接的，通过绕过各种无穷大的概念来证明关于有限数的事实。在这些情况下，通常可以提供一种翻译，在这种翻译中，我们将关于无穷大的语句重新解释为关于显式计算的更复杂的语句。这个项目的目标是为发生这种情况的情况开发“元定理”-结果允许我们系统地将无限证明转换为有限的、显式的证明-并通过将它们应用于模型理论中的例子来测试这些方法。该项目将通过参与研究主题来支持研究生和本科生的培训。该项目考虑了各种情况，其中抽象的逻辑概念，特别是饱和、紧凑、强迫和不可数基数，被用来证明具体的定理。证明理论的教训之一是，我们经常期望这样的证明指向更具体的证明；这个项目的目标是找到这样的具体证明。该项目专注于模型理论的结果，包括稳定性理论的组合部分及其与图和超图准随机性的链接，以及用于量词消除的饱和嵌入测试。证明理论功能解释是一个中心工具；将开发特定领域的改编以使方法实用。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

One of the surprising aspects of modern mathematics is that it is often possible to prove that it is possible to calculate something without providing an explicit way to perform the calculation. This research project is focused on cases where this happens because the argument is indirect, proving a fact about finite numbers using a detour through various notions of infinity. In these cases, it is often possible to provide a translation in which we reinterpret statements about infinite numbers as more complicated statements about explicit computations. The goal of this project is to develop "meta-theorems" for cases where this happens - results allowing us to systematically translate infinitary proofs into finite, explicit proofs - and to test these methods by applying them to examples in model theory. The project will support the training of graduate and undergraduate students through their involvement with the research topics.This project considers an assortment of situations where abstract logical ideas, particularly saturation, compactness, forcing, and uncountable cardinals, are used to prove concrete theorems. One of the lessons of proof theory is that we often expect such proofs to point the way towards proofs that are more concrete; the goal of this project is to find such concrete proofs. The project focuses on results in model theory, including the combinatorial part of stability theory and its links to graph and hypergraph quasirandomness, and saturated embedding tests for quantifier elimination. The proof-theoretic functional interpretation is a central tool; domain-specific adaptations will be developed to make the approach practical.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.