Explicit Proofs from Compactness and Saturation

现代数学令人惊讶的一个方面是，在不提供显式的计算方法的情况下，经常可以证明计算是可能的。这个研究项目的重点是发生这种情况的情况，因为论证是间接的，证明了一个关于有限数的事实，通过各种无限的概念迂回。在这些情况下，通常可以提供一种翻译，将关于无限数的陈述重新解释为关于显式计算的更复杂的陈述。这个项目的目标是为这种情况开发“元定理”——结果允许我们系统地将无限证明转化为有限的、明确的证明——并通过将它们应用于模型理论中的例子来测试这些方法。该项目将通过研究生和本科生参与研究课题来支持他们的培训。这个项目考虑了抽象逻辑思想的各种情况，特别是饱和、紧致、强迫和不可数基数，被用来证明具体的定理。证明论的一个教训是，我们常常期望这样的证明为更具体的证明指明道路；这个项目的目标就是找到这样具体的证据。该项目侧重于模型理论的结果，包括稳定性理论的组合部分及其与图和超图拟随机的联系，以及量词消除的饱和嵌入测试。证明理论的泛函解释是核心工具；将开发特定于领域的适应性以使该方法切实可行。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.