The Project

The first direction concerns the so-called arithmetic Ramsey Theory, namely the partition regularity of combinatorial configurations on the integers, a topic that has attracted the interest of the mathematical community in the past few years. We will focus on specific problems regarding polynomial and exponential configurations, on the natural numbers as well as on abstract structures.

The second direction regards the logico-computational strength of Hindman's Finite Sums Theorem. This theorem features a deep interplay of logical, computational and combinatorial methods. In particular, we plan to study the strength (in the sense of reverse and computable mathematics) of some restrictions and of some finite versions of HT, and the role of the apartness condition.

The third direction concerns densities and Keisler measures. These are finitely additive measures on algebras of definable sets. Loeb samples will be our main tool. Firstly we will compare properties of Loeb samples to known properties of Keisler measures and then study applications to combinatorics, including extensions of the famous B+C property of sets of positive density.

The fourth direction concerns quasi-orders and applications; this is an area full of open problems with ramifications to a wide range of areas, including reverse mathematics, Ramsey theory, model checking. We plan to study graph minors, α-better quasi orders and better quasi order preservation properties.

The fifth direction concerns the propositional proof complexity of combinatorial statements. It is centered on studying the computational limits to finite provability, analysing the complexity of proving combinatorial statements in different logical proof systems. Proof complexity is our guiding line. This is a core research area at the border between logic, combinatorics and complexity mainly aimed at solving whether NP is equal P. Its main question is proving that every proof system fails on proving efficiently at least a family of theorems and is grounded on techniques drawn from logic, combinatorics and complexity theory. We will explore the complexity of proof systems and theorem-proving procedures focusing on classifying them according to their provability strength and on developing new logico-combinatorial methods to obtain new lower bounds for limits of provability.