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

Albert Atserias, Moritz Müller

We prove that the bounded arithmetic theory $S_2^1$ is consistent with EXP $⊈$ P/poly. More generally, we show that certain separations of $V_2^1$ from a theory $T$ imp…