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.