From G\"odel incompleteness to the consistency of circuit lower bounds

TL;DR

This paper establishes the consistency of certain complexity class separations with bounded arithmetic theories, linking G"odel's incompleteness to circuit lower bounds and exploring the implications for proof hardness.

Contribution

It proves the consistency of EXP and PSPACE lower bounds with bounded arithmetic theories, extending G"odel's incompleteness ideas to computational complexity.

Findings

Proves $S^1_2$ is consistent with EXP $ ot\subseteq$ P/poly.

Shows that certain theory separations imply the consistency of complexity lower bounds.

Provides magnification results for the hardness of proving lower bounds almost everywhere.

Abstract

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\"odel'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.