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

Albert Atserias; Moritz Müller

paper

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

arXiv:2604.25251

Abstract

We prove that the bounded arithmetic theory $S_{2}^{1}$ is consistent with EXP $\neq \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 $\neq \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 $\neq \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.