On the Consistency of Circuit Lower Bounds for Non-Deterministic Time

Abstract

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory V${}_2^0$ is consistent with the conjecture that NEXP $⊈$ P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. The same techniques establish the same results with NEXP replaced by the class of problems that are decidable in non-deterministic barely superpolynomial time such as NTIME$(n^{O(\log \log \log n)})$. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.

An extended abstract of part of this work appeared in the Proceedings of the 55th ACM Symposium on Theory of Computation (STOC 2023). This is a small revision of the earlier long version that includes some minor corrections, a revised introduction, and some additional observations