Meta-Mathematics of Complexity Theory

Despite significant efforts from computer scientists and mathematicians, the P vs. NP problem and other fundamental questions about the complexity of computations seem to remain out of reach for existing techniques. The difficulty of making progress on such problems has motivated a number of researchers to investigate the logical foundations of computational complexity. Over the last few decades, several works at the intersection of logic and complexity theory showed that certain fragments of Peano Arithmetic collectively known as Bounded Arithmetic can formalize a large fraction of results from algorithms and complexity (e.g., the PCP Theorem and complexity lower bounds against restricted classes of Boolean circuits). It is natural to consider if the same theories can settle longstanding problems about the inherent difficulty of computations.

In the first part of this talk, we survey a few recent results on the unprovability of statements of interest to complexity theory in theories of Bounded Arithmetic and highlight some open problems. In the second part of the talk, we will cover new results on the reverse mathematics of complexity lower bounds, a research direction which seeks to determine which axioms are necessary to prove certain results. We explore reversals in the setting of bounded arithmetic, with Cook's theory PV₁ as the base theory, and show that several natural lower bound statements about communication complexity, error correcting codes, and Turing machines are equivalent to widely investigated combinatorial principles such as the weak pigeonhole principle for polynomial-time functions and its variants. As a consequence, complexity lower bounds can be formally seen as fundamental mathematical axioms with far-reaching implications. Time permitting, we will also present several implications of these results:

- Under a plausible cryptographic assumption, the classical single-tape Turing machine Ω(n²)-time lower bound for Palindrome is unprovable in Jerábek’s theory APC₁.
- While APC₁ proves one-way communication lower bounds for Set Disjointness, it does not prove one-way communication lower bounds for Equality, under a plausible cryptographic assumption.
- An amplification phenomenon connected to the (un)provability of some lower bounds, under which a quantitatively weak n^(1 + ε) lower bound is provable if and only if a stronger (and often tight) n^c lower bound is provable.
- Feasibly definable randomized algorithms can be feasibly defined deterministically (APC₁ is ∀Σ₁ˡ-conservative over PV₁) if and only if one-way communication complexity lower bound for Set Disjointness are provable in PV₁.