From Gödel incompleteness to the consistency of circuit lower bounds
For researchers in computational complexity and proof theory, this work provides a consistency result linking Gödel incompleteness to circuit lower bounds, though it is incremental in building on Takeuti's earlier separation.
The paper proves that the bounded arithmetic theory S^1_2 is consistent with EXP not being contained in P/poly, using a variant of Gödel's consistency statement. It also establishes analogous results for PSPACE not in P/poly, contingent on unknown theory separations.
We prove that the bounded arithmetic theory $S^1_2$ is consistent with EXP $\not\subseteq$ P/poly. More generally, we show that certain separations of $V^1_2$ from a theory $T$ imply the consistency of $T$ with EXP $\not\subseteq$ P/poly. For $T=S^1_2$, Takeuti (1988) established such a separation using a variant of Gödel's consistency statement. Analogous results hold for PSPACE $\not\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.