Complexity Theory in Feasible Mathematics

This is a research project in proof complexity, a research area situated at the interface of mathematical logic and computational complexity theory. Proof complexity in general investigates the question of how difficult it is to prove mathematical theorems. In propositional logic this mainly concerns estimations on the lengths of proofs in propositional proof systems, and in first-order logic, the characterization of the deductive power of first-order mathematical theories. For strong propositional proof systems, specifically the so-called Frege and Extended Frege systems, only trivial lower bounds on proof lengths are known. Further, there is a lack of mathematical methods to establish independence of universal first-order sentences from weak theories of arithmetic. In both cases it seems to be even difficult to come up with plausible candidates of tautologies or sentences that might turn out to be hard to prove. Both questions are closely related due to a simulation of weak arithmetics by propositional proof systems. For example, Extended Frege simulates an arithmetical theory that formalizes arguments based on polynomial time computable concepts and functions. This and related theories can be seen as formalizations of feasible mathematics. The mentioned gaps of knowledge are related to our current inability to prove some of the fundamental hypotheses of computational complexity theory. A prominent conjecture states that these hypotheses themselves might be independent from weak arithmetics. An example is the hypothesis that the famous NP-complete satisfiability problem requires circuits of superpolynomial size. This hypothesis being unprovable in the abovementioned theory would mean that any proof of it must use concepts and functions of high computational complexity. On the propositional side the hypothesis is expressed by a sequence of tautologies. These exemplify an important family of tautologies, namely those obtained from so-called proof complexity generators. In some cases independence from weak arithmetics can be derived from the fact that provability would imply the existence of witnessing functions of low computational complexity, and this in turn might contradict other complexity theoretic hypotheses. Unfortunately, this approach seems to fail for the hypothesis considered above. An idea of this project is that one can make good use of such a failure. In fact, the existence of witnessing functions can be used to produce other, a priori even harder tautologies expressing he same hypothesis. Roughly speaking, this is due to the fact that witnessing functions eliminate quantifiers, and hence simplify formulas. Generally speaking, this project aims to enhance our current sparse understanding of the mentioned proof complexity generators and the relation between computational hardness hypotheses and independence of open questions from complexity theory from weak arithmetics, that is, feasible mathematics.

Understanding the power of computation is one of the biggest challenges in science and society. Computational complexity theory has been dedicated to the investigation of this generic goal but central questions of the field like the famous P versus NP problem remain notoriously elusive. The present project approached these questions from the perspective of mathematical logic. More specifically, from the perspective of bounded arithmetic which formalizes various levels of feasible reasoning. The main results of the project include 1. feasibly constructive proofs of some of the most canonical limitations of various restricted computational models, and 2. a co-development of a new approach for obtaining limitations of strong, unrestricted computational models, and, in particular, a contribution to a new approach to the P versus NP problem, which avoids previously existing barriers. We hope that this contribution to our understanding of the power of computation will eventually help us to design more efficient algorithms affecting everyday life.