Workshop Ramsey Theory and Computability


Monday July 9 – Friday July 13, 2018

Rome Notre Dame Global Gateway



All talks are 50 minutes unless noted.



Monday, July 9, 2018

[Chair: Carlucci)


3:30pm       Paul Shafer, University of Leeds, UK

                              Reverse mathematics, a Ramsey theorem for graphs, and complete linear orders, Slides.


4:30pm       Coffee Break


5:00pm       Silvia Steila, University of Bern, Switzerland

                              SCT through the reverse mathematical looking glasses (Joint work with Emanuele Frittaion, Florian Pelupessy and Keita Yokoyama.), Slides.


Tuesday, July 10, 2018

[Chair: Patey)


3:00pm       Lu Liu, Central South University, China

                              Finitary combinatorics in computability theory,  Slides.


4:00pm       Coffee Break


4:30pm       Marcia Groszek, Dartmouth College, USA

                              Coloring Principles beyond ACA, Slides.

                              *25 minutes


5:00pm       Keita Yokoyama, Japan Advanced Institute of Science and Technology

                                                Ramsey's theorem and sizes of proofs, Slides.


Wednesday, July 11, 2018

[Chair: Cholak)


9:30am       Nicola Galesi, Università di Roma - Sapienza, Italy

                              Proof complexity of k-clique principles, Slides.


10:30am     Coffee Break


11:00am     CANCELLED Jake Pardo, Appalachian State, USA

                              Reverse mathematics and colorings of hypergraphs

                              *25 minutes


11:00am  (new time) Jeff Hirst, Appalachian State University, USA

                              A weak coloring principle, Slides.


12:00pm     Lunch


2:30pm       Lorenzo Carlucci, Università di Roma - Sapienza, Italy

                              On the strength of some families of natural restrictions of Hindman's Theorem, Slides.


3:30pm       Coffee Break


4:00pm       Richard Shore, Cornell University, USA

                              Producing Elementary Proofs from Ultrafilter Proofs of Combinatorial Theorems: The View from Reverse Mathematics.


5:00pm       Mauro Di Nasso, Università di Pisa, Italy

                                                Nonstandard methods and ultrafilters in Ramsey Theory, Slides.


6:00pm       Wine and Cheese Reception


Thursday, July 12, 2018

[Chair: Dzhafarov)


9:30am       Wei Li, National University of Singapore

Ramsey's Theorem for Trees, Slides.


10:30am     Coffee Break


11:00am     Thilo Weinert, University of Vienna, Austria

Choiceless Ramsey theory for linear orders, Slides.

                              *25 minutes


11:30am     Chi Tat Chong, National University of Singapore

                                                Separating the tree Ramsey theorem for pairs, Slides.


Friday, July 13, 2018

[Chair: Hirschfelt)


9:30am       Arno Pauly, Swansea University, UK

                              Separation techniques for products of Weihrauch degrees, Slides and Handout.


10:30pm     Coffee Break


11:00am     Henry Towsner, University of Pennsylvania, USA

                              The complexity of the set of tautologies of a theory, Slides.


12:00pm     Conference Ends


Invited talks

Lorenzo Carlucci, On the strength of some families of natural restrictions of Hindman's Theorem

Abstract: The strength of Hindman's Finite Sums/Finite Unions Theorem is a long-standing open problem in Reverse Mathematics. We present some results on families of natural restrictions of Hindman's Theorem that admit both non-trivial lower bounds and upper bounds below the ACA_0^+ upper bound known to hold for the full theorem. For example we show that the restriction of Hindman's Finite Unions Theorem to unions of exactly three terms is equivalent to ACA_0, and that the restriction to unions of exactly two terms - which easily follows from RT^2_2 - combinatorially implies IPT^2_2.  We also discuss bounds on other families of restrictions of Hindman's Theorem featuring arbitrarily long sums of adjacent elements, exactly large sums and sums of terms chosen according to some fixed pattern - e.g., an arithmetical progression.

Chi Tat Chong, Separating the tree Ramsey theorem for pairs

Abstract: The tree Ramsey theorem for pairs, denoted TT^2_2, states that if the pairs of compatible nodes on the full binary tree are divided into two groups (I.e. colored in  two colors), then there is a subtree  isomorphic to the full binary tree all of whose pairs of compatible nodes belong to the same group. There is a corresponding notion of stability for trees, which is stated as: if the nodes on the full  binary tree are colored by a 0'-recursive scheme in two colors, then there is a  subtree isomorphic to the full binary tree all of whose nodes have the same color. In this talk we describe a nonstandard model that satisfies stable TT^2_2 but not TT^2_2.

Mauro Di Nasso, Nonstandard methods and ultrafilters in Ramsey Theory.

Abstract: In Ramsey Theory, ultrafilters often play an instrumental role. By using nonstandard models of the integers, one can replace those third-order objects (ultrafilters are families of subsets) by simple points. In this talk we present a nonstandard technique that is grounded on the above observation, and show its use in proving some new results in Ramsey Theory of Diophantine equations.

Nicola Galesi, Proof complexity of k-clique principles  

Abstract: The k-clique principle states that a given graph contains a clique of size k.  When it is applied on a graph not containing a k-clique the principle can be encoded into a family of  propositional contradictions. We explore the question whether to refute the k-clique principle (over different families of graphs and different refutational proof systems) it is required  a proof length proportional to the time of a brute force algorithm or one can do significantly better. We will present some recent lower bounds results for these families of formulas based on random graphs and for the Resolution system and the importance of these questions in proof complexity.

Jeff Hirst, A weak coloring principle

Abstract: Given any finite coloring of the natural numbers, there must be a tail in which every color that is present appears at least twice. Working in RCA_0, it is easy to prove this principle from induction on \Sigma^0_2 formulas.  With more effort, it can also be proved from stable Ramsey's theorem for pairs and two colors.  Our interest in the principle arises from an equivalent statement about conflict free colorings of a particular hypergraph.  This is joint work with Caleb Davis, Jake Pardo, and Tim Ransom.

Wei Li, Ramsey's Theorem For Trees.

Abstract:  TT1 is the principle that every finite coloring of the full binary tree has a homogeneous subtree isomorphic to the full binary tree. We give a sketch of the proof that TT1 is Pi1-1 conservative over B\Sigma_2+P\Sigma_1. Therefore, TT1 does not imply I\Sigma_2. This is joint work with C.T. Chong, Wei Wang and Yue Yang.

Lu Liu, Finitary combinatorics in computability theory.

Abstract: Most of newly arising computability theory (reverse math, algorithmic randomness theory or even computable model theory) has close connection with combinatorics, and in many cases, finite combinatorics. In this talk we give two such examples. The first example shows that a relativized version of a naturally arising reverse math question is equivalent to a (purely) combinatorial question. The second example shows how to obtain a partial result of computable dimension 2 construction (on locally finite connected graph) by analyzing a combinatorial game. The second example is a joint work with Denis Hirschfeldt.

Arno Pauly, Separation techniques for products of Weihrauch degrees

Abstract: Many separations between Weihrauch degrees can be proven using established methods such as omega-models from reverse mathematics, the Borel-hierarchy from descriptive set theory or non-uniform considerations involving Turing degrees. These methods however cannot show results like f x f being strictly above f. Here, we survey some techniques suitable for such separations.

Paul Shafer, Reverse mathematics, a Ramsey theorem for graphs, and complete linear orders

Abstract: This talk consists of two parts (that we do not claim are particularly related).

In the first part, we consider the following theorem of Rival and Sands (1980):  every infinite graph G contains an infinite subset H such that every vertex of G is adjacent to either zero, one, or infinitely many vertices of H.  This is an interesting hybrid statement.  The H in the Rival-Sands theorem is not as structured as a homogeneous set in the sense of RT^2_2.  However, unlike with RT^2_2, the H in the Rival-Sands theorem provides some information about the vertices of G \setminus H.  We show that the Rival-Sands theorem is equivalent to ACA_0.  This work is joint with Marta Fiori Carones, Alberto Marcone, and Giovanni Soldà.

In the second part, we show that the statement ``for every linear order L, if L is complete, then the order topology on L is compact'' is equivalent to WKL_0.  This answers a question of François Dorais.


Richard Shore, Producing Elementary Proofs from Ultrafilter Proofs of Combinatorial Theorems: The View from Reverse Mathematics.

Abstract: An increasingly common phenomena in combinatorics is the use of higher order notions, objects and principles to prove combinatorial facts about the natural numbers N (or some other countable set) and its subsets. One particularly fruitful such notion has been that of (nonprincipal) ultrafilters on N and it has been applied extensively in proving Ramsey type theorems. We present a method that incorporates a systematic analysis of the classical proofs that exploit algebraic structures on classes of ultrafilters. It produces elementary proofs at relatively low levels of the reverse mathematical/recursion theoretic hierarchies Our results typically show that the theorems are reverse mathematically equivalent to Iterated HIndman's Theorem and that the homogenous sets produced are recursive in the $\omega\cdot m$th Turing jump of the given coloring. (Here both $m$ and the index of the reduction are fixed for all instances of the particular theorem.) Examples include Gowers' Fin_k Theorem and the Infinite Hales-Jewett Theorem.

In this talk we will give an outline of our methods centered on one of the applications from the viewpoint of reverse mathematics. We work in a third order system that is conservative over the corresponding second order one. Our plan is, given a countable second order model of Iterated Hindman's Theorem, we expand it to a structure for the third order theory without changing the first or second order parts. We then show that this third order structure contains objects which satisfy the properties defining idempotent or minimal idempotent ultrafilters. Thus the existence of such objects is conservative over IHT. We then show that the third order theory with axioms asserting the existence of such ultrafilters is strong enough to prove the Ramsey type theorems considered. Thus they are, in fact, all provable from IHT. They all imply Hindman's theorem and have iterated versions which are reverse mathematically equivalent to IHT

This is joint work with Antonio Montalban.

Silvia Steila, SCT through the reverse mathematical looking glasses (Joint work with Emanuele Frittaion, Florian Pelupessy and Keita Yokoyama.)

Abstract: In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (we call MSCT) for first order functional programs, a sufficient condition for termination. They proved the SCT criterion: a program is size-change terminating (i.e. MSCT) if and only if it satisfies a certain property (we call ISCT) which can be statically verified from the recursive definition of the program.

From Lee, Jones and Ben-Amram’s paper we can outline the following three-steps argument to prove the termination of a first order functional program P:  Verify that P is ISCT; Apply the SCT criterion to prove that P is MSCT;  Derive the termination of P from the fact that "every MSCT program terminates". Since the Ackermann function is ISCT provably in RCA0, a natural question arises: in which theory can we carry out the above argument?  Specifically, in which theory can we prove the SCT criterion? Similarly, in which theory can we prove that every MSCT program terminates?  In this talk we focus on the reverse mathematical analysis of such statements.

Henry Towner, The complexity of the set of tautologies of a theory

Abstract: A complete axiomatizable theory has additional tautologies beyond those of first-order logic. That is, there are additional formulas A(X) of first-order logic with a predicate X such that, for any formula phi, the theory proves A(phi).

We investigate the complexity of the set of these tautologies. We identify some properties of a theory which show that the set of tautologies is computable, but show that for many important theories, the set of tautologies is as complicated as it can be (co-c.e. complete).

(Joint work with Denis Hirschfeldt and Scott Weinstein.)

Keita Yokoyama, Ramsey's theorem and sizes of proofs

Abstract: In the recent study of reverse mathematics, it is known that Ramsey's theorem for pairs and two colors (RT^2_2) is Pi^0_3-conservative over both of RCA_0 and RCA_0*. In this talk, we will refine these conservation results from the view point of sizes/lengths of proofs. We will reformulate the conservation proofs with forcing indicators and show that RT^2_2 gives no speed-up for Pi^0_3-consequences over RCA_0, while it gives super-exponential speed-up over RCA_0*. This is a joint work with Leszek Kolodziejczyk and Tin Lok Wong.

Special Session Talks

Marcia Groszek, Coloring Principles Beyond ACA

Abstract: The reverse mathematics of Ramsey-type theorems often follows the model of Ramsey's Theorem, in which the full theorem essentially has the strength of arithmetic comprehension, and restricted versions occupy places lower in the hierarchy.  This talk looks at structures, and families of structures, for which a Ramsey property for pairs, or for singletons, has greater reverse-mathematical strength.

Jake Pardo, Reverse mathematics and colorings of hypergraphs. CANCELLED.

Abstract: Given the classical reverse mathematical interest in graphs and their colorings, it is only reasonable to consider hypergraphs in the same way.  Our work considers different representations for hypergraphs as well as different types of vertex colorings for hypergraphs that inspire new questions beyond what would be asked regarding graphs.  We present several equivalence theorems to subsystems of second order arithmetic.  This is joint work with Caleb Davis, Jeff Hirst, and Tim Ransom.

Thilo Weinert, Choiceless Ramsey theory for linear orders

Abstract: Ramsey-Type problems have been considered both in finite and infinite combinatorics. In infinite combinatorics most attention has been payed to partition relations between cardinals assuming the Axiom of Choice and almost all research dealt with ordinals (We think of cardinals as initial ordinals here). A notable exception is a paper by Erdős, Milner and Rado from 1971. There the authors prove, among other things the following theorem.


Assume the Axiom of Choice. Then for all order-types t there is a colouring of the triples of t in black and white such that every quadruple contains a white triple and every copy of the integers contains a black one.

This is similar to the folklore result (using AC) that for every order-type t there is a colouring of the pairs of t in black and white such that every infinite descending sequence contains a white pair and every infinite ascending sequence contains a white one. These two results put things into perspective. It is known that one can have very strong partition properties in models of ZF violating AC, consider for example Mathias's result that it is consistent with ZF that all sets of reals have the Ramsey property or Martin's discovery that AD implies that a colouring of the uncountable sets of countable ordinals with two colours admits an uncountable sets all of whose uncountable subsets get the same colour.

We focus on linear orders of lexicographically ordered sequences of zeroes and ones of an ordinal length and prove positive and negative partition relations, an example of the latter is the following Theorem of ZF:

For every initial ordinal kappa and every ordinal alpha of cardinality at most kappa there is a colouring of the quadruples of the linear order given by the lexicographically ordered sequences of zeroes and ones of length alpha in black and white such that every sextuple contains a black quadruple and each of the following order-types contains a white one:


\kappa^* + \kappa \\

2 + \kappa^* \\

\kappa 2 \\



We achieve a complete answer as to which partition relations for 2-colourings of points, pairs, triples or quadruples of the continuum are consistent with ZF. For larger linear orders however there are many questions left unanswered.

This is joint work with Philipp Lücke and Philipp Schlicht