Objectives:
We study weak logical systems, guided by the question: what is the weakest natural theory in which we can prove a mathematical statement? This question is often fundamentally complexity theoretic in nature, as proofs in such weak systems can be associated with feasible computations. We will study this and related topics in a range of settings, including bounded arithmetic, model theory, algebraic complexity, bounded set theory, and nonclassical logics.
Programme type: FP7 ERC Advanced Grant
Objectives:
This project aims at making progress in the study of basic open problems in computational complexity, such as the P versus NP problem. There are several approaches to these difficult problems, one of which is proof complexity. In proof complexity we not only study the lengths of proofs in various proof systems, but also first order theories associated with complexity classes, collectively called bounded arithmetic. Proving separations between proof systems or theories in bounded arithmetic, however, seems as difficult as separating the corresponding complexity classes.
Our group has been working in proof complexity for more than two decades and has played an important role in the development of the field. The novelty of this project is its focus on the role of the following two concepts in proof complexity: incompleteness and pseudorandomness. The incompleteness phenomenon is well understood in the context of stronger arithmetical theories, but little is known in bounded arithmetic. As it may be extremely difficult to solve the problems about incompleteness in the polynomial time domain, one of the approaches we will try is proposing axioms that will decide these questions. Similarly, pseudorandomness has been intensively researched in computational complexity, but its role in proof complexity still needs more research.