Consistency of NEXP Not in P/poly in a Strong Theory
5Albert Atserias (Technical University of Catalonia (UPC))
https://simons.berkeley.edu/talks/albert-atserias-technical-university-catalonia-upc-2023-03-21-0
Proof Complexity and Meta-Mathematics
We prove that the conjecture NEXP \not\subseteq P/poly is true in a model of the relatively strong theory of bounded arithmetic V^0_2. Concretely, there is a model of V^0_2 in which the canonical NEXP-complete problem cannot be solved by polynomial-size circuits. To our knowledge, this is the first unconditional consistency result for superpolynomial circuit lower bounds relative to a strong theory of bounded arithmetic -- previous consistencies were only conditioned on unproved conjectures, or for fixed-polynomial lower bounds. The theory V^0_2 includes Buss' hierarchy T_2, of which the theory S^1_2 for polynomial-time reasoning and Jerabek's theories APC1 and APC2 for a approximate counting reasoning sit at its lower levels. In particular, it is known that a significant part of contemporary complexity theory can be formalized in V^0_2. We view this as supporting the claim that the consistency of the conjecture NEXP \not\subseteq P/poly with V^0_2 is the strongest available evidence that it is actually true.
Based on joint work with Sam Buss (UCSD) and Moritz Mueller (U.Passau).