Computability theory arose out of the development by Turing and others of a mathematically precise definition of the notion of algorithm. One of the most fruitful developments in this field has been the study of the algorithmic content of mathematics. At the same time, concerns about the foundations of mathematics have led to the analysis of different formal systems for mathematical reasoning, and the study of the relative power of such systems. The computability-theoretic approach has turned out to play a key role in this project. Combinatorics is an area of mathematics whose methods and results underlie a great deal of mathematical reasoning, so the study of its algorithmic content and of the systems required to formalize its methods is particularly important. Computable combinatorics has a long history, but has seen a recent surge of interest highlighting the fact that computability-theoretically natural notions tend to be combinatorially natural, and vice-versa. This project aims to strengthen the connections between computability theory and combinatorics by increasing our understanding of the algorithmic content of combinatorial principles, through a concerted group effort to use what we have learned in recent years to systematize the area further, work toward solving a number of its outstanding questions, and explore its outward-facing aspects.
This project will address major open problems such as determining whether Hindman’s Theorem holds arithmetically, and whether it is equivalent to its restriction to sums of length at most two; determining the first-order part of Ramsey’s Theorem for pairs, and clarifying the computability-theoretic relationship between this principle and its stable version; and determining the exact proof-theoretic strength of Laver’s Theorem. More importantly, it will focus on the development of lines of research particularly relevant to the growing interest in connections between computability theory and combinatorics, including the study of questions of methodological interest to combinatorialists, for instance ones involving Hindman’s Theorem and the use of ultrafilters in combinatorics; the development of new proofs of combinatorial theorems inspired by questions regarding the computational content of these theorems, along the lines of Montalban’s new proof of Laver’s Theorem; the analysis and comparison of different general methods, such as the use of ultrafilters, topological dynamics, and probabilistic methods; the development of notions of comparison between theorems that, while still computability-theoretic in spirit, are closer to being direct reflections of combinatorial differences; the understanding of splittings of combinatorial principles into computationally and combinatorially simpler parts; the study of the usefulness of combinatorially-defined objects as computational oracles; and the study of the first-order consequences of the existence of combinatorially-defined second-order objects. This project is thus aimed at developing the study of the connections between computability theory and combinatorics along a large number of related directions, making use of the computability-theoretic, proof-theoretic, and combinatorial expertise of its PIs, senior personnel, and key collaborators.