Abstract
We prove that the conjecture NEXP \not\subseteq P/poly is
true in a model of the relatively strong theory of bounded arithmetic
V02. Concretely, there is a model of V02 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 in a strong theory of bounded
arithmetic -- previous consistencies were conditioned on unproved
conjectures, or for fixed-polynomial lower bounds. The theory V02
includes Buss' hierarchy T2, where the theory S12 for polynomial-time
reasoning sits at its first level, and includes Jerabek's theories
APC1 and APC2 for a approximate counting reasoning. In particular, it
is known that a significant part of contemporary complexity theory can
be formalized in V02. We view this as supporting the claim that the
consistency of the conjecture NEXP \not\subseteq P/poly in V02 is the
strongest available evidence that it is actually true.
Based on joint work with Sam Buss (UCSD) and Moritz Mueller (U.Passau).