From Gödel incompleteness to the consistency of circuit lower bounds

We prove that the bounded arithmetic theory $S_2^1$ is consistent with EXP $\subseteq ̸$ P/poly. More generally, we show that certain separations of $V_2^1$ from a theory $T$ imply the consistency of $T$ with EXP $\subseteq ̸$ P/poly. For $T=S_2^1$, Takeuti (1988) established such a separation using a variant of Gödel’s consistency statement. Analogous results hold for PSPACE $\subseteq ̸$ P/poly but the required separations of theories are yet unknown. Finally, we give magnification results for the hardness of proving almost-everywhere versions of these lower bounds.