Workshop Description:
The study of the limits of computability and provability is one of the fundamental areas of computer science. This study is articulated in many research fields, such as, prominently, proof theory, reverse mathematics, propositional proof complexity, and bounded arithmetic. Classical Combinatorics - especially Ramsey theory - is a major source of theorems and proof-techniques for all these areas.
Proof theory and reverse mathematics aim at characterizing the strength of theorems of ordinary mathematics in terms of provability in formal systems of arithmetic and analysis. Standard techniques in this area are recursion- and proof-theoretic methods. Despite the huge amount of results already obtained, the strength of various fundamental principles is still unknown. A famous challenge is e.g., the classification of the infinitary Ramsey theorem for pairs and two colors.
Propositional proof complexity studies the lengths of proofs in propositional proof systems. This problem is motivated by fundamental open questions in complexity theory, such as NP vs co-NP. Techniques for establishing lower bounds for proof length include tools from circuit complexity, communication complexity, cryptography and derandomization. Finding new techniques for proving stronger lower bounds is one of the major challenges in the field.
Infinite combinatorics studies properties of sets that depend on their size (rather than on their definability or on their complexity). Large cardinals, partition properties and cardinal arithmetic are the central objects of study here. The role of infinite Ramsey theory in providing a bridge between these areas and other areas of mathematics (e.g., analysis and topology) is prominent in recent research.
The workshop aims at giving an occasion to the communities working on independence results for theories of arithmetic, in reverse mathematics, in combinatorics of Ramsey theory, in proof complexity and in bounded arithmetic to be exposed to one another's recent results, methods, and goals.
The areas in question have large intersections, both in the methods of proof as in the principles of interest. One common endeavour is to establish lower and upper bounds of combinatorial principles.
For example, an unprovability (resp. provability) proof for a theory of arithmetic can be casted in terms of proving lower bounds (resp. upper bounds) against a scale of fast-growing functions that extends the functions usually considered in classical combinatorics. Proof-theoretical methods have proved to be relevant for combinatorics as witnessed, e.g., by Avigad and Townser's recent results in ergodic Ramsey theory, by Kohlenbach's progress on Ramsey's theorem for pairs and the infinitary pigeonhole principle, and Weiermann's results on phase transitions for independent combinatorial principles.
The lenght of proofs of propositional translations of classical combinatorial principles (e.g., pigeonhole principle and Ramsey theorem) is of central interest for proof complexity. Moreover, hardness results for propositional proof-systems and unprovability results in certain first order theories of arithmetic are strictly related: a first order theory T can be associated to a propositional proof system P in such a way that statements easily provable in T can be translated into propositional formulas easily provable in P. Many of the tools used in bounded arithmetic have their origins in the proof theory of arithmetic (e.g., Buss' witnessing method, Beckmann's dynamic ordinals, Pudlak's games etc.).
Infinite Ramsey theory is a major ingredient of current research in infinite combinatorics. In particular, it is a source of methods that have found successful and striking applications in topology and in functional analysis, in the work of Rosenthal, Bourgain-Fremlin-Talagrand and more recently of Todorcevic and Gowers, with the solution of major open problems in Banach space theory.
Ramsey theory thus constitutes a common theme for all the mentioned areas. The major aim of the workshop is to stimulate the interaction between researchers in the mentioned areas, to enhance the transfer of methods of proof from one area to the other, and to set the ground for developing a unifying view on the logico-combinatorial study of combinatorial principles, such as Ramsey-type statements.