Constructive Criticisms of Complexity: Unifying Proofs and Algorithms

For decades, fundamental questions in complexity theory have remained wide open. A classic counting argument by Shannon shows that most Boolean functions on n bits require circuits of size 2^n/n, yet we lack even superlinear circuit lower bounds for explicit functions. This raises a natural question: can we make these counting arguments constructive?

 

In this talk, we explore constructivity through the lens of mathematical logic. Weak fragments of Peano Arithmetic, known as theories of Bounded Arithmetic, characterize "efficient" reasoning and exhibit a constructive property—proofs of existence correspond to efficient search algorithms. In particular, Buss's seminal work introduced the theories S^i_2, which capture reasoning at the i-th level of the polynomial hierarchy. We focus on S^1_2, a theory powerful enough to formalize much of modern complexity theory, from the Cook-Levin theorem to the PCP theorem.

 

Our main results establish that:

(1) Proving known, non-constructive lower bounds within S^1_2 would yield breakthrough lower bounds.

(2) Under a reasonable conjecture in logic, certain circuit lower bounds are unprovable in S^1_2.

 

These findings build on and unify previous work on constructive complexity, which traditionally employs the algorithmic notion of efficient refuters rather than bounded arithmetic. Additionally, our work provides the first conditional separation between S^1_2 and APC, a theory corresponding to ZPP reasoning.

 

This talk is based on joint work with Marco Carmosino.