This project deals with the development of methods in proof theory, particularly the area known as proof mining, and their application to Ramsey theory. Many theorems in Ramsey theory can be proven using infinitary methods, in the form of ultraproducts, nonstandard analysis, topological dynamics, and ergodic theory. Proof mining extracts finite information from these infinite arguments. The proposed research will apply the methods of proof mining in order to investigate: 1) explicit bounds on numerical quantities which are not made apparent by infinite proofs, 2) approximations of infinitary Ramsey theoretic statements which "quantify" (typically, with a countable ordinal) how transfinite a given construction is, and 3) new finitary analogs of infinitary methods. Where necessary, the proposed research will also expand the repertoire of proof mining tools by investigating how to interpret higher order notions, particularly the topological structure of the ultrafilters, in finitary terms.
Questions in mathematics about concrete, finite properties of the integers often turn out to have answers that make use of abstract, infinite notions. The goal of the area of proof theory known as "proof mining" is to develop tools for explaining this phenomenon. Often, we discover that there are finite methods which can replace the infinite ones, at the price of making the argument much more difficult to understand. Some of these arguments are so unwieldy that it is difficult to imagine that they could be discovered directly. By "unwinding" the infinite argument into finite arguments, however, we often discover new information. For example, infinite proofs often prove that a number with some property exists while providing no information about which number it is; the corresponding finite argument, however, typically gives an upper bound on the size of that number.
This project investigated the connection between relatively concrete---in particular, finite---mathematical questions and very abstract, infinitary techniques. As part of this project, an abstract framework for working with such arguments was introduced, making it possible to bring the techniques to a number of areas where they had not previously been used, including finite model theory (where a new, much shorter proof was given of a classic result showing that directed graphs are more complicated than undirected graphs), randomness (a new, very general characterization of quasirandomness was given, making it possible to treat several previously investigated ideas in a single framework), and probability (a infinite technique corresponding to finite Markov chains was introduced). Additionally, the project investigated "reverse mathematics": the investigation of how computationally complicated known results are. A new technique for "separating" results---showing that one is more complicated than another---was developed, resolving two open problems in the area. An additional result showed that many of the infinitary techniques described above are actually computationally "free": any proof using these infinitary techniques can be transformed into a proof which does not use them without increasing the computational complexity beyond a certain level. This project also supported a new program at the University of Pennsylvania to introduce first-year students to collaborative and conceptual aspects of advanced mathematics that don't appear in the standard first-year curriculum.
