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.
